Z3：非线性算术的奇怪行为

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)

但神奇的是，现在我得到了“sat”。我不确定 Z3 在非线性算术方面如何选择策略，但问题是否可能来自 Z3 为第一个公式选择了对第二个公式无用的策略？

提前致谢

Answer 1

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

对于这个问题，本质上是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