z3py 中可达性的形式化

Question

我正在尝试将可达性属性形式化，以便如果存在长度为 4 的路径（这意味着如果有 3 个中间节点通过它连接 2 个所需节点），我可以找到一个令人满意的解决方案。 注意：我将它限制为只能找到长度为 4 的路径。以下是我所做的：

from z3 import*
# link between two nodes
L= Function('L', IntSort(), IntSort(),BoolSort())

# path between two nodes
p=Function('p', IntSort(), IntSort(), BoolSort())

u=Int('u')
x=Int('x')
y=Int('y')
z=Int('z')
i=Int('i')
j=Int('j')

s=Solver()

s.add(x>=0, x<=5, y>=0,y<=5, u>=0,u<=5,i>=0,i<=5, j>=0,j<=5,z>=0,z<=5)

# no self link or path
si1= ForAll(i,  And (L(i,i)==False,p(i,i)==False))

si2=ForAll([x,y], p(x,y)==p(y,x))

# To fix source and destination
si3= ForAll([u,x,y], And(L(u,x)==False, L(y,u)==False) ) 

# To fix the length of path
si4=ForAll([x,y], Exists([i,j,z] , And( L(x,i)==True, L(i,j)==True,L(j,z)==True,L(z,y)==True) )   )

si5=ForAll([x,y,z], Implies (And (p(x,y)==True, L(x,z)==False,L(y,z)==False), L(x,y)==True))

#s.add(L(1,2)==True,L(2,3)==True, L(3,4)==True,L(4,5)==True)

s.add( Implies (p(x,y)==True, Exists([x,y], And(si1==True,si2==True,si3==True,si4==True,si5==True))) )

#s.add(p(x,y)==True)

result=s.check()
model = s.model()

print result, model ,model[p].else_value()

它返回我 SAT，但现在的问题是，如果我取消评论/添加 s.add(p(x,y)==True) 它让我不满意，而是应该给我一个 SAT 结果。因为在 x 和 y 之间存在一条路径。即使我手动提及（这是一种幼稚的方法）

s.add(L(1,2)==True,L(2,3)==True, L(3,4)==True,L(4,5)==True)

它仍然返回 x=0 和 y=3，因为这不是一个可满足的解决方案，所以第一个可满足的解决方案应该是 x=0 和 y=4

si4=ForAll([x,y], Exists([i,j,z] , And( L(x,i)==True, L(i,j)==True,L(j,z)==True,L(z,y)==True) )   )

我哪里错了？

Answer 1

我将尝试解释为什么会从 sat 转换为 unsat，但忽略如何编码可达性。简而言之，问题在于 si3 和 si5 意味着 p(x,y) 对于所有 x 和 y 都是错误的。当您取消注释/断言“p(x,y)==True”时，这会同时断言 si3 和 si5 并导致矛盾。

更详细地说，让我们断言“p(x,y)==True”。 s1 到 s5 必须是这样的情况：

s.add( Implies (p(x,y)==True, Exists([x,y], And(si1==True,si2==True,si3==True,si4==True,si5==True))) )
; |- Exists([x,y], And(si1==True,si2==True,si3==True,si4==True,si5==True))
; |- And(si1==True,si2==True,si3==True,si4==True,si5==True) as the existential bindings for x and y are not instantiated in any subformula.

我们可以分解 si3 来推断它等价于所有 L(x,y) 都是假的。

si3= ForAll([u,x,y], And(L(u,x)==False, L(y,u)==False) ) 
; moving the forall across the and we get
And (ForAll([u,x,y], L(u,x)==False), ForAll([u,x,y], L(y,u)==False) ) 
; dropping unused variables
And(ForAll([u,x], L(u,x)==False), ForAll([u,y], L(y,u)==False) ) 
; which are the same statement up to variable renaming. So
ForAll([x,y], L(x,y)==False)

使用s3，我们可以替换s5中所有L(-,-)的实例，得到：

s5=ForAll([x,y,z], Implies (And (p(x,y)==True, L(x,z)==False,L(y,z)==False), L(x,y)==True))
; replacing L(-,-) with False and reducing False==False and False==True gives:
ForAll([x,y,z], Implies (And (p(x,y)==True, True, True), False))
; which is equivalent to
ForAll([x,y], p(x,y)==False)

这与 p(x,y)==True 相矛盾。 （注意这是 x 和 y 的不同绑定，而不是量词中的绑定。）

一个令人满意的模型是“u = x = y = z = i = j = 0”和“p(0,0)=False”。一旦“p(x,y)”为假，可以忽略 s1 到 s5 以满足公式。 （我在这里说“模型”有点松散，但希望直觉很清楚。）

作为一般建议，我建议重命名由量词绑定的变量以消除歧义。下面一行中存在 3 个不同的“x”和“y”副本。

s.add( Implies (p(x,y)==True, Exists([x,y], And(si1==True,si2==True,si3==True,si4==True,si5==True))) )

“p(x,y)”中有顶层未绑定的x和y，由“Exists([x,y],...)”绑定的版本（没有任何实例） ，以及绑定在 si1 到 si5 中的版本。也许你可以跟踪这一点，但我觉得很难。

Answer 2

我能够按如下方式更新我的形式化，现在我得到了一个令人满意的解决方案，但我仍然无法找到中间节点的不同值：i,j,z

from z3 import*

L= Function('L', IntSort(), IntSort(),BoolSort())
p=Function('p', IntSort(), IntSort(), BoolSort())

u=Int('u')
x=Int('x')
y=Int('y')
z=Int('z')
i=Int('i')
j=Int('j')

s=Solver()

s.add(And(x>=0, x<=5, y>=0,y<=5, u>=0,u<=5,i>=0,i<=5, j>=0,j<=5,z>=0,z<=5))

#si_1
s.add(ForAll(x,  And( L(x,x)==False,p(x,x)==False )))

#si_2
s.add(ForAll([x,y], And(L(x,y)==L(y,x), p(x,y)==p(y,x))))


#si_3
s.add(ForAll([x,y], Implies(p(x,y)==True,  Exists([i,j,z], And( L(x,i)==True, L(i,j)==True,L(j,z)==True,L(z,y)==True)))))


#si_4
s.add(ForAll([x,y,z], Implies (And (p(x,y)==True, L(x,z)==False,L(y,z)==False), L(x,y)==True) ))


s.add(p(x,y)==True)




result=s.check()
model = s.model()

print result, model

根据约束 si_3：

    s.add(ForAll([x,y], Implies(p(x,y)==True,  Exists([i,j,z], And( L(x,i)==True, L(i,j)==True,L(j,z)==True,L(z,y)==True)))))

我应该得到 i、j 和 z 的不同值，因为 si_1 确保 L(x,x) 为假：

s.add(ForAll(x,  And( L(x,x)==False,p(x,x)==False )))

我应该改变什么，这样我才能得到不同的 i、j、z 值并且它们不应该相同......