在 Python 中使用 SAT 求解找到通过图中顶点的路径答案

【问题标题】：Finding a path through vertices in a graph with SAT Solving in Python在 Python 中使用 SAT 求解找到通过图中顶点的路径
【发布时间】：2020-10-15 10:14:26
【问题描述】：

基本上我要做的是在图表上找到从 v1 到 v2 的路径，但有些节点是彩色的，我们无法访问它们。

我了解约束，但我真正遇到问题的部分是了解如何将可能的移动添加到约束中。

如果我以这种方式设置布尔值

nodes = [Int('"n%i_%i" % (i, j)) for i in range(len(G))]

moves = []
for i in range(len(G)):
     moves += ?

条件是节点彼此相邻，因此 i = i 和 j = j +1（或 i = i +1 和 j = j）并且允许访问节点，因此 path=True，这是图表的一个特征。所以例如 G[i][j] == True。

我会使用类似 (or(And(节点彼此相邻), (G[i][j] == True))) 以及如何表示节点彼此相邻？

谢谢！！

【问题讨论】：

您是否尝试在邻接矩阵表示中实现路径查找？ “彩色”节点具体是什么意思？或者您是否尝试从 (0,0) 开始遍历二维网格并仅向下和向右移动？
感谢您的评论。如此彩色意味着我们无法访问它们，并且节点确实具有像 2d 网格一样的坐标，但我们不一定从 (0,0) 开始。是的，我们只是在向右和向下移动。

标签： python graph z3 sat

【解决方案1】：

由于我不明白您对彩色节点的意思，这里将是一个初步的解决方案：

谓词

首先，我们定义一些谓词以及它们对我们的直观含义：

p(X, Y, n)表示我们在时间点n访问坐标X，Y的节点，时间点从0开始，一直到G的长度。

go(right, n)表示我们在时间点n向右走。

go(down, n)表示我们在时间点n下降。

编码

初始状态

最初，我们知道p(Start_X, Start_Y, 0) 是真的。因此，我们添加单元子句[p(Start_X, Start_Y, 0)]

运动

在每个时间点，我们都必须移动。因此，对于每个时间点 t，添加子句 [go(right, t), go(down, t)] 和 [not go(right, t), not go(down, t)] 这也称为恰好一次约束，即我们可以向右或向下移动。

现在，我们需要关联 p 谓词和 go 谓词：如果 p(X, Y, T) 为真，并且 go(right, T)，则 p(X+1, Y, T+1) 为真。因此，添加子句[not p(X, Y, T), not go(right, T), p(X+1, Y, T+1)]。

您可以以类似的方式对“向下”动作进行编码。

最终状态

现在，我们必须确保最终到达节点 v2。请注意，仅添加 p(v2_x, v2_y, t) 在某个时间点为真是不够的。相反，我们必须确保排除违反此条件的模型：由于我们只能向下或向右移动，我们知道我们无法访问低于 v2 或向右的节点。因此，我们添加[not p(X, Y, t)] 形式的单元子句，其中 t 是与 v1 和 v2 的距离。

辅助

现在，可以从您的模型中读取解决方案，但您的模型可能看起来有点奇怪，因为多个 p 谓词在同一时间点为真。一般来说，这并没有什么坏处，但如果你这样说可以排除： [not p(X1, Y1, t), not p(X2, Y2, t)] 对于每个 t 和不同的坐标。

【讨论】：