Формализация достижимости в 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, но теперь проблема в том, что, если я не-комментарий/добавить сек .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) 

она по-прежнему возвращает меня х = 0 и у = 3, где, как это не выполнимо решение, то первое выполнима решение должно быть х = 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

Я попытаюсь объяснить, почему это переходы с седа на 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 (х, у), являются ложными.

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, мы можем заменить все экземпляры L (-, -) в s5, чтобы получить:

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) 

Это противоречит р (х, у) == 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)))) 

Существует несвязанного х верхнего уровня и у в «р (х, у)», версия, связанный с помощью «EXISTS ([х, у], ...)» (которые не имеют любой экземпляр) и версии, связанные с si1 через si5. Может быть, вы можете следить за этим, но мне сложно.

Answer 2

я смог обновить свои формализации следующим образом, теперь я получаю выполнимые решения, но до сих пор я не могу найти различные значения для промежуточных узлов: I, J, г

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 и г как si_1 гарантирует, что Ь (х, х) будет ложным:

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

Что нужно изменить, чтобы я мог получать различные значения i, j, z, и они не должны быть одинаковыми ...