【发布时间】：2016-09-06 16:23:56
【问题描述】：
我想构建一个 SMT 公式，该公式具有对整数线性算术和布尔变量的许多断言，以及对实数非线性算术和布尔变量的一些断言。整数和实数的断言只共享布尔变量。例如，考虑以下公式：
(declare-fun b () Bool)
(assert (= b true))
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (or (not b) (>= (+ x y) (- x (+ (* 2 z) 1)))))
(declare-fun r () Real)
(assert (or (not b) (= (+ (* r r) (* 3 r) (- 4)) 0)))
如果我用这个公式输入 z3，它会立即报告“未知”。但是如果我删除它的整数部分，我会立即得到解决方案，它满足变量“r”的约束。我认为这意味着非线性约束本身对求解器来说并不难。问题应该在于对整数的（线性）约束和对实数的（非线性）约束的混合。
所以我的问题如下。使用 z3（如果有的话）处理这种混合公式的正确方法是什么？我对 DPLL(T) 的理解是，它应该能够使用针对不同约束的不同理论求解器来处理此类公式。如果我错了，请纠正我。
【问题讨论】：
-
根据我的经验，Z3 中的非线性算术处理程序相当脆弱，能否正常工作取决于预处理过程是否成功。在许多情况下，您最好在自己身边执行线性化（例如，用区间化代替非线性算术）
-
谢谢！所以你认为这个问题与理论混合无关？
-
是的，我就是这么想的。
-
以上涉及的理论有两种合理的解释：混合实数和整数理论，或者实数理论和整数理论的并集。 AFAIK 所有 SMT 求解器都将其解释为混合实数和整数的理论。 QF 非线性混合整数和实理论包含希尔伯特的第 10 个问题。因此，其中涉及一种理论，它是不可判定的，它超出了 nlsat 算法所解决的范围。对于“我要申请 nlsat 吗？”，您很可能不在警卫范围内。并击中线性混合求解器。 （克里斯托夫，阿列克谢怎么能证实这一点？）
-
好的，谢谢！我知道非线性整数算术的不确定性。但我不是 SMT 方面的专家。所以我认为一个典型的 SMT 求解器应该能够以某种方式检测断言属于哪个理论，并为该断言使用相应的理论求解器（例如，在我的情况下，线性整数求解器用于第一个断言，非线性实数求解器用于第二个断言）。这是我对 DPLL(T) 工作原理的理解。但也许在实践中情况并非如此（或者我的理解完全错误），如果可能的话，SMT 求解器会尝试对所有断言使用一个理论求解器。