SMT =
Erfüllbarkeitsproblem
für beliebige boolesche Kombinationen
von atomaren Formeln aus einer Theorie
Beispiel:
x≥3∨x + y≤4↔x > y
Erweiterung des DPLL-Algorithmus: DPLL(T)
Literatur: Kroening/Strichman, Kap. 12
2014-03-31