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

Question

Z3 的算术求解器是基于 DPLL(T) 和 Simplex(在 this paper 中描述)开发的。并且我不明白Z3在产生冲突解释时是如何进行回溯的。我举个例子:

线性算术公式为:

(2x1+x2≤200 或 3x1+x2≤250) AND (2x1+x2+x3≤200 或 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