DPLL(T)算法采用Z3(线性算法)

Question

基于DPLL(T)和单纯形(本文描述)开发了Z3的算法求解器。我不明白当产生冲突解释时，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