表示在图 G 中存在一个函数 `path(x, y)`

如何解决表示在图 G 中存在一个函数 `path(x, y)`

我正在尝试通过 Z3Py 中的边通过顶点的连通性来形式化图中存在的路径的属性。

我在 z3py 中有以下定义：

from z3 import *

# Set of vertices present in the graph
V = EmptySet()
V = SetAdd(V,0)
V = SetAdd(V,1)
V = SetAdd(V,2)

Edge = DataType('Edge')
Edge.declare('edge',('first',IntSort()),('second',IntSort()))
Edge = Edge.create()

def makeEdge(i,j):
  return Edge.edge(i,j)

# Set of directional edges in the graph
E = EmptySet()
E = SetAdd(E,makeEdge(0,1))
E = SetAdd(E,makeEdge(1,2))

根据上述定义，我们可以说图 G 有 2 个集合：V 和 E，它们是 G 中存在的顶点和边的集合。

我现在定义成员资格谓词并将它们固定到求解器中

x = Int('x')
y = Int('y')

Isvertex = Function('Isvertex',IntSort(),BoolSort())
IsEdge = Function('IsEdge',BoolSort())

vertex_axiom = ForAll([x],IsMember(x,V) == Isvertex(x))
edge_axiom = ForAll([x,y],IsMember(makeEdge(x,y),E) == IsEdge(x,y))

s = Solver()
s.add(vertex_axiom)
s.add(edge_axiom)

当调用 sat 时，上面的返回 s.check()。使用随机值作为函数 Isvertex 和 IsEdge 的输入进行测试，仅当在集合 V 和 E 中按预期找到该值时才返回 true。

现在我尝试定义一个谓词函数 IsPath(x,z) wrt to G 其中 IsPath(x,z) 应该返回 true 当且仅当顶点 x 和 {{ 之间存在路径1}}。

z

使用第一个代码片段中定义的图形将其修复到求解器中：

z = Int('z')
IsPath = Function('IsPath',BoolSort())

# base case
path_axiom1 = ForAll([x,z],Implies(IsEdge(x,z),IsPath(x,z))

# recurrence case
'''
A path exists between x,z if and only if there is a vertex y such that
x,y is an edge in G and y,z is a path
'''
path_axiom2 = ForAll([x,Exists([y],And(And(Isvertex(y),IsEdge(x,y)),IsPath(y,z) == IsPath(x,z))))

返回 s.add(path_axiom1) s.add(path_axiom2) print(s.check()) ，这是有道理的，因为路径不存在 unsat 对顶点。

如何更好地优化我的表达式以仅引用符合路径公式的顶点并将其添加到我的求解器中？

谢谢。