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

Z3 : strange behavior with non linear arithmetic

我刚开始使用 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 为第一个公式选择了对第二个公式无用的策略吗?

提前致谢

第二种编码不等同于第一种,因此行为不同。第二种编码不包括约束 (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