SMT = Satisfiability modulo Theory

• Aufgabenstellung:

  Erfüllbarkeitsproblem für beliebige boolesche Kombinationen von atomaren Formeln aus einer Theorie

  Beispiel: x≥3∨x + y≤4↔x > y

• Lösungsplan:
  • Umformung in erfüllbarkeitsäquivalente CNF (Tseitin)
  • Lösung durch Variante von DPLL (``DPLL modulo Theory'')

Literatur: Kroening/Strichman, Kap. 11