z3py 中 .check() 的不正确行为

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) 表示：检查所有 other 约束是否可满足，假设 F 是。特别是，它 而不是 断言 F。（如果您稍后 asserts/checks 进一步操作，这一点很重要。）

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

Aside 您可以获得 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)

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

z3py 中 .check() 的不正确行为

Incorrect behaviour of .check() in z3py

z3

z3py