SAT Solving und Anwendungen

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