Z3 の算術ソルバーは、DPLL(T) とシンプレックス (この論文で説明) に基づいて開発されています。また、競合の説明が生成されたときに 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}ます。
私の質問は、この競合セットが生成されたときにバックトラックがどのように実行されるかです。