DPLL(T), Beispiel

T = mathend000# 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≤y∧y≤z⇒x≤z mathend000#)

• T-Lerner

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