DPLL (T) algorithm used in Z3 (linear arithmetic)

Question

The Z3 arithmetic solver is developed based on DPLL (T) and Simplex (described in this article ). And I don't understand how Z3 performs backtrack when a conflicting explanation is generated. I will give an example:

Linear arithmetic formula:

(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

after the approval of 2x1+x2≤200, 2x1+x2+x3≤200, x1≥50, x2≥50and x3≥60consistently, he gives a description explaining the conflict {2x1+x2+x3≤200, x1≥50, x2≥50, x3≥60}.

My question is, how do I go back while creating this set of conflicts?

Answer 1

The main document for reading the algorithm:

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

Download: .pdf