带前提的非线性实数算术的可解性

Question

一个小例子表明，当 NRA 断言被与 (sat p1 ... pn) 检查相关的前提 pi 标记时，非线性实数算术 (NRA) 求解器会受到阻碍。

以下 SMT2 示例 returns SAT 正确模型：

(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)

(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)

(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))

(assert (and p1 p2 p3 p4))
(check-sat)
(get-model)

以下语义等价的例子returns未知：

(declare-const p1 Bool)
(declare-const p2 Bool)
(declare-const p3 Bool)
(declare-const p4 Bool)

(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)

(assert (=> p1 (= x1 (/ 1.0 (* x2 x2)))))
(assert (=> p2 (not (= x2 0.0))))
(assert (=> p3 (= x3 (* 2.0 x1))))
(assert (=> p4 (= x3 5.0)))

(check-sat p1 p2 p3 p4)
(get-model)

此外，模型查询returns一个模型，这是不正确的！

使用第一种风格对我来说不是一个选择，因为我对从 UNSAT 问题实例中获取 unsat-cores 特别感兴趣，并且我希望动态组合 "active" 前提。但是，通过将前提与 "and" 联系起来，可以防止不饱和核心的产生。

看起来带有 (assert (and p1 p2 p3 p4)) 的第一个示例在预处理步骤中以某种方式得到了简化，因此 NRA 求解器会同时查看所有四个约束并能够求解它们。使用带有 (check-sat p1 p2 p3 p4) 的第二个示例似乎并非如此。

我错过了什么吗？谢谢！

PS：我正在使用来自不稳定分支（2015-03-26 加载）的 Z3 版本 4.4.0。

Answer 1

这种行为差异的原因是 Z3 运行在使用假设时是不同的求解器。如果不需要假设、增量特征、证明或理论组合，它将运行一个新的求解器 (NLSAT)，而当至少需要其中一个特征时，它会回退到一个较旧的、弱得多的求解器很快就放弃了，returns 未知。您可以使用 -v:100 运行 Z3，它会报告

(combined-solver "using solver 1")
...
(nlsat :num-exprs ...)

然而，无效模型确实是不应该默认输出的东西。

带前提的非线性实数算术的可解性

Solvability of nonlinear real arithmetic with premises

z3