z3 - 为什么 Z3 不能在不进行看似微不足道的修改的情况下解决这个实例？

Question

原问题是:

(declare-const a Real)
(declare-const b Bool)
(declare-const c Int)

(assert (distinct a 0.))

(assert (= b (distinct (* a a) 0.)))

(assert (= c (ite b 1 0)))

(assert (not (distinct c 0)))

(check-sat)

结果未知。

但最后两个约束合在一起，等同于(assert (= b false))，并且在手动执行此重写之后

(declare-const a Real)
(declare-const b Bool)
(declare-const c Int)

(assert (distinct a 0.))

(assert (= b (distinct (* a a) 0.)))

(assert (= b false))

;(assert (= c (ite b 1 0)))

;(assert (not (distinct c 0)))

(check-sat)

Z3 现在能够解决这个实例(它是不满意的)。

为什么Z3可以解决第二个问题，但不能解决第一个问题，即使第一个问题可以简化为第二个问题？

编辑:

在定位问题的过程中，我发现了一个很奇怪的地方。

Z3 解决了以下实例并返回“unsat”:

(declare-fun a() Real)
(declare-fun b() Bool)
(declare-fun c() Int)

(assert (distinct a 0.0))

(assert (= b (distinct (* a a) 0.0)))

(assert (= b false))

;(assert (= c 0))

(check-sat)

但如果我取消注释 (assert (= c 0))，求解器将返回“未知”，即使 c=0 与上述断言无关.

Answer 1

这里的问题是像 (* a a) 这样的表达式是非线性的，而 Z3 的默认非线性问题求解器会放弃，因为它认为它太难了。 Z3 确实有另一个求解器，但那个求解器的理论组合非常有限，也就是说，你不能将它用于混合 bool 、位向量、数组等问题，而只能用于算术问题。将 (check-sat) 命令替换为 (check-sat-using qfnra-nlsat) 即可轻松进行测试。