SMT

SMT = mathend000# 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 mathend000#

• allgemeines Lösungsverfahren:

  Erweiterung des DPLL-Algorithmus: DPLL(T)

Literatur: Kroening/Strichman, Kap. 12