DPLL(T)

Ansatz: für jedes Atom F = P(t₁,…, t_k) mathend000#
eine neue boolesche Unbekannte p_F↔F mathend000#, dann:

• SAT-Problem für diese Variablen p_* mathend000# lösen,
• feststellen, ob die dadurch beschriebene Konjunktion von Atomen in der Theorie T mathend000# erfüllbar ist

Ideen zur Realisierung/Verbesserung:

• naiv (SAT): belegen, testen, backtrack.
• DPLL (SAT): partiell belegen, t., b., propagieren (, lernen)
• DPLL(T) (SMT): Test in Theorie T mathend000#, Theorie-Propagation.