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}。

我的问题是，当生成此冲突集时如何执行回溯？

Answer 1

为了理解算法而要阅读的主要论文是：

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

下载：.pdf