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

Question

我试图通过 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))

有了上面的定义，我们可以说一个图有 2个G集合：它们是存在于.VEG

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

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

IsVertex = Function('IsVertex', IntSort(), BoolSort())
IsEdge = Function('IsEdge', IntSort(), IntSort(), 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时才返回 true 。VE

现在我尝试定义一个谓词函数IsPath(x, z)wrtG当IsPath(x, z)且仅当顶点之间存在路径时应该返回 truex和z.

z = Int('z')
IsPath = Function('IsPath', IntSort(), IntSort(), 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, z], 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有意义，因为路径不存在ForAll顶点对。

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

谢谢你。

标签： pythonz3smtz3py