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

Question

Z3 的算术求解器是基于 DPLL(T) 和 Simplex（在本文中描述）开发的。而且我不明白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