3

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

提前致谢

4

1 回答 1

3

第二种编码不等同于第一种，因此行为不同。第二种编码不包括约束(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)，默认情况下它将选择可以处理此问题的正确求解器。所以是的，从本质上讲，这与选择求解器有关，这部分取决于底层术语的种类。

相关问答：将非线性 Real 与线性 Int 相结合

于 2015-09-08T17:24:05.397 回答