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}.
我的问题是,当生成此冲突集时,如何执行回溯？