z3 - SMT 中的混合理论

Question

我想构造一个 SMT 公式，其中包含对整数线性算术和 bool 变量的多个断言，以及对实数非线性算术和 bool 变量的一些断言。对整数和实数的断言仅共享 bool 变量。例如，请考虑以下公式:

(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) 的理解是，它应该能够针对不同的约束使用不同的理论求解器来处理此类公式。如果我错了，请纠正我。

Answer 1

正如 George 在评论中所说，Z3 中的非线性求解器相当脆弱，开箱即用的性能也不是很好。也就是说，在 stackoverflow 上有很多关于这个问题的问题和答案，例如，请参阅这些:

Z3 Performance with Non-Linear Arithmetic

How does Z3 handle non-linear integer arithmetic?

Z3 : strange behavior with non linear arithmetic

Non-linear arithmetic and uninterpreted functions

Z3 Theorem Prover: Pythagorean Theorem (Non-Linear Artithmetic)

Which techniques are used to handle Non-linear Integer Real problems in z3?

Satisfiablity checking in non-linear integer arithmetic by approximation