问题描述
基本上，我想做的是在图形上找到从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。
我会使用类似（或（And（节点彼此相邻），（G [i] [j] == True））的东西吗？ 以及如何表达节点彼此相邻？
谢谢！
解决方法
由于我不了解您对彩色节点的含义，因此这是一个初步的解决方案：
谓词
首先，我们定义一些谓词以及它们对我们的直观含义：
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,0)]
运动
在每个时间点，我们都必须移动。因此，对于每个时间点t，添加子句
[go(right,t),go(down,t)]和[not go(right,not go(down,t)]
这也称为恰好一次约束，即我们可以向右或向下移动。
现在，我们需要关联p谓词和go谓词：
如果p（X，Y，T）是true，而go（right，T）是true，则p（X + 1，Y，T + 1）是true。
因此，添加子句[not p(X,T),not go(right,p(X+1,T+1)]。
您可以通过类似的方式对“下沉”动作进行编码。
最终状态
现在，我们必须确保最终到达节点v2。
请注意，仅在某个时间点添加p(v2_x,v2_y,t)是正确的。
相反，我们必须确保排除违反此条件的模型：
因为我们只能上下移动，所以我们知道我们无法访问v2之下或右边的节点。
因此，我们添加格式为[not p(X,t)]的单位从句，其中t是与v1和v2的距离。
辅助
现在，可以从模型中读取解决方案，但是就多个p谓词在同一时间点为真而言，您的模型可能看起来有些奇怪。
通常，这不会造成伤害，但是如果您这样说，可以将其排除：
[not p(X1,Y1,not p(X2,Y2,t)]用于每个t和不同的坐标。