Z3 给出方程求解的不满意结果

Question

给定每个变量的一组可能值和两个方程式，我编写了以下代码来获取确切的变量值。但是 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"

Answer 1

[...] clearly it can be seen there exists a valid solution.

其实没有。

让我们稍微修改一下问题，将 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)

如果我们枚举所有可能的解决方案，其中 none 个验证 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]

Z3 给出方程求解的不满意结果

Z3 giving unsat result for equation Solving

python

z3

smt

sat-solvers