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)

如前所述，第二个示例因 "unknown" 而失败，通过增加详细级别（到 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^2 > 3 对于某个整数 a 的约束时，它无法发现它是可满足的，即使这两个断言彼此独立。

对于这个问题，本质上是Z3在遇到实数与整数混合时，默认情况下不会使用非线性实数算术求解器（它是完整的）。这是一个如何使用 qfnra-nlsat (rise4fun link: 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)，它会默认选择能够处理此问题的正确求解器。所以是的，本质上这与选择的求解器有关，这在一定程度上取决于基本术语的种类。

相关Q/A：Combining nonlinear Real with linear Int

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

Z3 : strange behavior with non linear arithmetic

z3

solver

smt

sat