DPLL(T), Prinzip

Ansatz: für jedes Atom A = P(t₁,…, t_k)
eine neue boolesche Unbekannte p_A↔A.

naives Vorgehen:

• für jede Lösung des SAT-Problem für diese Variablen p_*:
• feststellen, ob die dadurch beschriebene Konjunktion von Atomen in der Theorie T erfüllbar ist

Realisierung mit DPLL(T):

• decide, T-solve (Konjunktion von T-Atomen)
• Konflikte (logische und T-Konfl.): backtrack
• logische Propagationen, Lernen
• T-Propagation (T-Deduktion)