Aussagenlogik (SAT)
- Grundlagen: Formeln, BDDs, Resolution, DPLL, CDCL
- Anwendungen: SAT-Kodierungen für
kombinatorische Aufgaben, Bit-Blasting
für andere Constraint-Bereiche
Prädikatenlogik: Bereiche und -spezifische Verfahren:
- Zahlen: lineare Gleichungen,
lineare Ungleichungen, Polynome,
Presburger-Arithmetik
- uninterpretierte Funktionen, Arrays
Prädikatenlogik: allgemeine Verfahren:
- Kombinationen von Theorien (Nelson-Oppen)
- Kombination von Theorie und SAT (DPLL(T))
2014-03-31