带前提的非线性实数算法的可解性 [英] Solvability of nonlinear real arithmetic with premises
问题描述
一个小例子表明，当 NRA 断言由与 (sat p1 ... pn) 检查相关的前提 pi 标记时，非线性实数算术 (NRA) 求解器会受到阻碍.
A small example indicates that the nonlinear real arithmetic (NRA) solvers are hindered when NRA assertions are labeled by premises pi in connection with (sat p1 ... pn) checks.
以下 SMT2 示例返回具有正确模型的 SAT:
The following SMT2 example returns SAT with the correct model:
(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)
以下语义等效的示例返回未知:
The following semantically equivalent example returns unknown:
(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)
此外，模型查询返回一个模型，这是不正确的！
Moreover, the model query returns a model, which is incorrect!
使用第一种风格对我来说不是一个选择，因为我对从 UNSAT 问题实例中获取 unsat-cores 特别感兴趣，并且我希望动态组合活动"前提.但是，通过将前提与and"连接起来，可以防止 unsat 核心产生.
Working with the first style is not an option for me since I am particularly interested in getting unsat-cores from UNSAT problem instances, and I wish to dynamically combine "active" premises. However, by connecting the premise with "and", unsat core production is prevented.
看起来第一个带有 (assert (and p1 p2 p3 p4)) 的示例在预处理步骤中以某种方式进行了简化，因此 NRA 求解器可以同时查看所有四个约束并能够解决它们.使用带有 (check-sat p1 p2 p3 p4) 的第二个示例似乎并非如此.
It looks like the first example with (assert (and p1 p2 p3 p4)) is somehow simplified in a preprocessing step, so that the NRA solver looks at all four constraints together and is able to solve them. This seems not to be the case using the second example with (check-sat p1 p2 p3 p4).
我错过了什么吗?谢谢！
Am I missing something? Thank you!
PS:我正在使用来自不稳定分支的 Z3 4.4.0 版(2015 年 3 月 26 日加载).
PS: I'm working with Z3 version 4.4.0 from the unstable branch (loaded 2015-03-26).
推荐答案
这种行为差异的原因是 Z3 在使用假设时运行不同的求解器.如果不需要假设、增量特征、证明或理论组合，它将运行一个新的求解器 (NLSAT)，而当至少需要这些特征中的一个时，它会回退到一个旧的、弱得多的求解器，该求解器会迅速放弃返回未知.您可以使用 -v:100 运行 Z3，它会报告
This difference in behavior is explained by the fact that Z3 runs a different solver when assumptions are used. If no assumptions, incremental features, proofs or theory combination are required, it will run a new solver (NLSAT), while when at least one of those features are required, it falls back to an older, much weaker solver which gives up quickly and returns unknown. You can run Z3 with -v:100 and it will report
(combined-solver "using solver 1")
...
(nlsat :num-exprs ...)
然而，无效模型确实是默认不应该输出的东西.
The invalid model however is indeed something that shouldn't be output by default.
这篇关于带前提的非线性实数算法的可解性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
