Z3 дает ненадлежащий результат для решения уравнения - PullRequest
Новая
       71

Z3 дает ненадлежащий результат для решения уравнения

4 голосов
/ 01 ноября 2019

Учитывая набор возможных значений для каждой переменной и двух уравнений, я написал приведенный ниже код, чтобы получить точные значения переменных. Но Z3 дает результаты Unsat.

Я создал 7 экземпляров и объединил их в один. И передал экземпляр решателю z3. Но получение неудовлетворительного результата в качестве ответа, но ясно видно, что существует правильное решение. Ниже код, который я написал: 

from z3 import *
import sys
import io
import math
import copy

X0 = Int('X0')
X1 = Int('X1')
X2 = Int('X2')
X3 = Int('X3')
X4 = Int('X4')
P0 = Int('P0')
P1 = Int('P1')
P2 = Int('P2')
P3 = Int('P3')
P4 = Int('P4')

I =  IntSort()
P = Array('P', I, I)

P0 = 10
P1 = 20
P2 = 30
P3 = 40
P4 = 50

s = Solver()

X0_ =[1,2,6]
X1_ =[2,6,7,8]
X2_ =[2,3,6,7]
X3_ =[2,4,8,9]
X4_ =[5,6,7,8,9]
X_Con1 = [(Or([X0 == i for i in X0_]))]
X_Con2 = [(Or([X1 == i for i in X1_]))]
X_Con3 = [(Or([X2 == i for i in X2_]))]
X_Con4 = [(Or([X3 == i for i in X3_]))]
X_Con5 = [(Or([X4 == i for i in X4_]))]
S_Con = [(X0 + X1 + X2 + X3 + X4 == 15)]
P_Con = [(P0*X0 + P1*X1 + P2*X2 + P3*X3 + P4*X4 == 520)]
Solve =   X_Con1 + X_Con2 + X_Con3 + X_Con4 + X_Con5 + S_Con + P_Con
s.add(Solve)
print(Solve)
if s.check() == sat:
    m = s.model()
    r = [m.evaluate(X0,X1,X2,X3,X4)]
    print(r)
else:
    print "unsat"

1 Ответ

3 голосов
/ 01 ноября 2019

[...] ясно видно, что существует верное решение.

На самом деле, нет.

Давайте немного изменим проблему изамените 520 новой свободной переменной с именем PFREE. 

from z3 import *
import sys
import io
import math
import copy

X0 = Int('X0')
X1 = Int('X1')
X2 = Int('X2')
X3 = Int('X3')
X4 = Int('X4')
P0 = Int('P0')
P1 = Int('P1')
P2 = Int('P2')
P3 = Int('P3')
P4 = Int('P4')

PFREE = Int('PFREE')

I =  IntSort()
P = Array('P', I, I)

P0 = 10
P1 = 20
P2 = 30
P3 = 40
P4 = 50

s = Solver()

X0_ =[1,2,6]
X1_ =[2,6,7,8]
X2_ =[2,3,6,7]
X3_ =[2,4,8,9]
X4_ =[5,6,7,8,9]
X_Con1 = [(Or([X0 == i for i in X0_]))]
X_Con2 = [(Or([X1 == i for i in X1_]))]
X_Con3 = [(Or([X2 == i for i in X2_]))]
X_Con4 = [(Or([X3 == i for i in X3_]))]
X_Con5 = [(Or([X4 == i for i in X4_]))]
S_Con = [(X0 + X1 + X2 + X3 + X4 == 15)]
P_Con = [(P0*X0 + P1*X1 + P2*X2 + P3*X3 + P4*X4 == PFREE)]
Solve =   X_Con1 + X_Con2 + X_Con3 + X_Con4 + X_Con5 + S_Con + P_Con
s.add(Solve)

while s.check() == sat:
    m = s.model()
    print(m)
    blocking_clause = Or([x != m.evaluate(x) for x in [X0, X1, X2, X3, X4]])
    s.add(blocking_clause)

Если мы перечислим все возможные решения, ни одно из этих проверок не подтвердит PFREE = 520: 

~$ python test.py 
[X0 = 2, X1 = 2, X2 = 2, X3 = 4, X4 = 5, PFREE = 530]
[X0 = 2, X1 = 2, X2 = 3, X3 = 2, X4 = 6, PFREE = 530]
[X0 = 1, X1 = 2, X2 = 3, X3 = 4, X4 = 5, PFREE = 550]
[X0 = 2, X1 = 2, X2 = 2, X3 = 2, X4 = 7, PFREE = 550]
[X0 = 1, X1 = 2, X2 = 2, X3 = 4, X4 = 6, PFREE = 570]
[X0 = 1, X1 = 2, X2 = 3, X3 = 2, X4 = 7, PFREE = 570]
[X0 = 1, X1 = 2, X2 = 2, X3 = 2, X4 = 8, PFREE = 590]
...