为什么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 现在能够解决这个实例（它是 unsat）。

为什么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 确实有另一个求解器，但它的理论组合非常有限，即，您不能将它用于混合布尔、位向量、数组等问题，而只能用于算术问题。通过将(check-sat) 命令替换为(check-sat-using qfnra-nlsat) 很容易测试。