z. B. Simplex, Fourier-Motzkin
bei Nichterfüllbarkeit liefert T-Solver eine „Begründung``
= (kleine) nicht erfüllbare Teilmenge (von Atomen {a1,…, ak}), dann Klausel ¬a1∨…∨¬ak lernen
neues (!) Atom x≤z entsteht durch Umformungen während Simplex oder Fourier-Motzkin
betrachte ¬x≤y∨¬y≤z∨x≤z als Konfliktklausel, damit CDCL