Z3中使用的DPLL(T)算法（线性算术）

Question

Z3的算术求解器是基于DPLL(T)和Simplex（在this paper中描述）开发的。当生成冲突解释时，我不理解Z3如何执行回溯。以下是一个例子：线性算术公式为：(2x1+x2≤200 OR 3x1+x2≤250) AND (2x1+x2+x3≤200 OR 4x1+2x2+x3≤400) AND x1≥50 AND x2≥50 AND x3≥60。在依次断言2x1+x2≤200、2x1+x2+x3≤200、x1≥50、x2≥50和x3≥60之后，它产生了一个冲突解释集{2x1+x2+x3≤200, x1≥50, x2≥50, x3≥60}。我的问题是，当生成这个冲突集时，回溯是如何执行的？

- ClePIR

Answer 1

理解该算法的主要论文是：

 A Fast Linear-Arithmetic Solver for DPLL(T)
 Bruno Dutertre,  Leonardo de Moura 

下载: .pdf

- Nikolaj Bjorner