DPLL(T), Beispiel

T = LRA (linear real arithmetic)

durch Tseitin-Transformation als CNF darstellen (zusätzliche boolesche Variablen)

DPLL(T) benutzt

• T-Solver für Konjunktion von vollst. belegten Klauseln

  (z. B. Simplexverfahren)

• T-Propagation

  (z. B. x$\le$y $\wedge$ y$\le$z $\Rightarrow$ x$\le$z)

• T-Lerner

  bei Nichterfüllbarkeit liefert T-Solver eine ,,Begründung`` (kleine nicht erfüllbare Teilmenge)