命名断言是否应该影响Z3中检查的可满足性

Question

我们遇到了Z3返回sat的约束，但如果我们随后添加某个命名断言，那么Z3将返回unknown。一个例子是：

(declare-fun a () Real)
(declare-fun b () Bool)
(assert (and (<= 0.1 a) (<= a 10.0)))
(assert (= b (= 1.0 (/ 1.0 a))))
(check-sat)

Z3报告说，这正如预期的那样是令人满意的。我们还可以断言b是true或false，这两个都是可满足的。然而，如果我们对b的值使用命名断言，那么根据该值，可满足性检查的结果可以变成unknown。值为true时，Z3仍然返回sat:

(set-option :produce-unsat-cores true)
(declare-fun a () Real)
(declare-fun b () Bool)
(assert (and (<= 0.1 a) (<= a 10.0)))
(assert (= b (= 1.0 (/ 1.0 a))))
(assert (! (= b true) :named c))
(check-sat)

使用值false，Z3返回unknown:

(set-option :produce-unsat-cores true)
(declare-fun a () Real)
(declare-fun b () Bool)
(assert (and (<= 0.1 a) (<= a 10.0)))
(assert (= b (= 1.0 (/ 1.0 a))))
(assert (! (= b false) :named c))
(check-sat)

检查unknown结果的原因(使用(get-info :reason-unknown)(返回(incomplete (theory arithmetic))。

Answer 1

在后一种情况下，z3似乎只是选择了错误的策略。将您的check-sat呼叫替换为：

(check-sat-using qfnra-nlsat)

z3在这两种情况下都显示sat。

为什么z3最终选择了不同的策略是一个很难回答的问题；我建议在他们的github网站上以票证的形式提交；他们可能错过了一个启发。

附带说明：我通过使用-v:10运行这两种情况并浏览详细的输出发现了这一点。这是一个不错的方式来看看z3在足够短的基准测试中做了什么。