.check()在z3py中的错误行为

Question

考虑一组约束F=[a+b>10，a*a+b+10<50]。

当我使用运行它时

s = Solver()
s.add(F)
s.check()

我得到了sat解决方案。

如果我用运行它

s = Solver()
s.check(F)

我得到了一个unknown解决方案。有人能解释为什么会发生这种情况吗？

Answer 1

让我们看看：

from z3 import *
a = Int('a')
b = Int('b')
F = [a + b > 10, a*a + b + 10 < 50]
s = Solver()
s.add(F)
print (s.check())
print (s.model())

此打印：

sat
[b = 15, a = -4]

我觉得不错。

让我们试试你的第二种变体：

from z3 import *
a = Int('a')
b = Int('b')
F = [a + b > 10, a*a + b + 10 < 50]
s = Solver()
print (s.check(F))
print (s.model())

此打印：

sat
[b = 7, a = 4]

我也觉得不错。

所以，我不知道你是怎么得到unknown的答案的。也许你有一个旧版本的z3；或者你的程序中有其他事情没有告诉我们。

然而，需要注意的是，s.add(F); s.check()和s.check(F)是不同的操作：

• s.add(F); s.check()表示：断言F中的约束；检查它们是否令人满意。

• s.check(F)的意思是：检查所有其他约束是否都是可满足的，假设F是。特别是，它确实不断言F。(如果您稍后进行进一步的断言/检查，这一点非常重要。(

因此，通常这两种不同的check使用方式用于不同的目的；并且可以得到不同的答案。但是，在没有其他断言的情况下，您将获得两者的解决方案，当然模型可能不同。

除此之外获得unknown的一个原因是存在非线性约束。你的a*a+b+10 < 50是非线性的，因为它本身有一个变量的乘积。您可以通过使用位向量而不是Int(如果适用(或使用非线性求解器来处理此问题；它仍然可以给你unknown，但可能会表现得更好。但只要看看你提出的问题，z3就可以很好地处理它

Answer 2

要了解s.check(F)中发生了什么，可以执行以下操作：

from z3 import *
import inspect
a = Int('a')
b = Int('b')
F = [a + b > 10, a*a + b + 10 < 50]
s = Solver()
print (s.check(F))
print (s.model())
source_check = inspect.getsource(s.check)  
print(source_check)

结果输出：

sat
[b = 10, a = 1]
def check(self, *assumptions):
"""Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
>>> x = Int('x')
>>> s = Solver()
>>> s.check()
sat
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> s.model().eval(x)
1
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown
"""
s = BoolSort(self.ctx)
assumptions = _get_args(assumptions)
num = len(assumptions)
_assumptions = (Ast * num)()
for i in range(num):
_assumptions[i] = s.cast(assumptions[i]).as_ast()
r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
return CheckSatResult(r)

这里和这里讨论了假设与断言的语义。但如果不得不承认的话，他们对我来说还不是很清楚。