Das aussagenlogische Erfüllbarkeitsproblem (SAT-Problem) spielt in Theorie (Komplexität, NP-Vollständigkeit) und Praxis (Hard- und Software-Verifikation, Konfiguration) eine herausragende Rolle.
Durch große Fortschritte in den letzten Jahren lassen sich heute eine Vielzahl praktischer kombinatorischer Probleme effizient mit SAT-Solvern bearbeiten.
- Grundlagen: Aussagenlogik
- SAT-Solving: Das DPLL-Verfahren
- Moderne Erweiterungen und Verbesserungen
- Implementierungstechniken
- Anwendungsbeispiele
- Übungen zu Theorie und Implementierung; Schreiben eines SAT-Solvers als Mini-Projekt
