Z3 : strange behavior with non linear arithmetic

Question

我刚开始使用 Z3 (v4.4.0)，我想尝试其中一个教程示例:

(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)

(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)

如前所述，第二个示例因“未知”而失败，通过增加详细级别(到 3)，我想我明白了原因:简化过程出现了一些问题，然后该策略失败了。为了更好地了解问题(并缩短输出)，我决定删除代码的第一部分以仅测试失败的部分:

(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)

但神奇的是，现在我“坐下”了。我不确定 Z3 在涉及非线性算术时如何选择其策略，但问题可能出在 Z3 为第一个公式选择了对第二个公式无用的策略吗？

提前致谢

Answer 1

第二个编码不等同于第一个，因此行为不同。第二个编码不包括约束 (assert (> (* a a) 3))，因此 Z3 可以发现对于某些实数 b 的选择，b^3 + b*c = 3 是可满足的和c。然而，当它具有 a^2 > 3 对于某个整数 a 的约束时，它无法发现它是可满足的，即使这两个断言彼此独立。

对于这个问题，本质上是Z3在遇到实数与整数混合时，默认情况下不会使用非线性实数算术求解器(它是完整的)。以下是如何使用 qfnra-nlsat(rise4fun 链接:http://rise4fun.com/Z3/KDRP)强制执行此操作的示例:

(declare-const a Int)
;(assert (> (* a a) 3))
;(check-sat)
;(get-model)

(echo "Z3 will fail in the next example...")
(declare-const b Real)
(declare-const c Real)
(push)
(assert (and (> (* a a) 3) (= (+ (* b b b) (* b c)) 3.0)))
(check-sat)
(check-sat-using qfnra-nlsat) ; force using nonlinear solver for nonlinear real arithimetic (coerce integers to reals)
(get-model)
(pop)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)

同样，如果您只是将 (declare-const a Int) 更改为 (declare-const a Real)，它会默认选择能够处理的正确求解器这个。所以是的，从本质上讲，这与选择的求解器有关，这在一定程度上取决于基础术语的种类。

相关问答:Combining nonlinear Real with linear Int