我试图通过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
有两个集合:V
和E
,它们是G
中存在的顶点和边的集合
我现在定义成员资格的谓词,并将它们固定到解算器中
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)
当调用s.check()
时,上述函数返回sat
。使用随机值作为函数IsVertex
和IsEdge
的输入进行测试时,只有在集合V
和E
中找到预期的值时,才会返回true
现在,我尝试将谓词函数IsPath(x, z)
wrt定义为G
,其中IsPath(x, z)
应在且仅当顶点x
和z
之间存在路径时返回true
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
对顶点
如何更好地优化表达式,使其仅引用符合路径公式的顶点,并将其添加到解算器中
多谢各位
目前没有回答
相关问题 更多 >
编程相关推荐