Bemerkungen

Das aussagenlogische Erfüllbarkeitsproblem (SAT-Problem) spielt in Theorie und Praxis eine herausragende Rolle. Es ist das erste als NP-vollständig erkannte Problem, und auch heute noch Ausgangspunkt vieler komplexitätstheoretischer Untersuchungen. Darüber hinaus hat sich SAT-Solving inzwischen als eines der wichtigsten grundlegenden Verfahren in der Verifikation von Hard- und Software etabliert und wird zur Lösung schwerer kombinatorischer Probleme auch in der industriellen Praxis verwendet.

Dieses Modul soll Studierenden die theoretischen und praktischen Aspekte des SAT-Solving vermitteln. Behandelt werden:

1. Grundlagen, historische Entwicklung
2. Codierungen, z.B. cardinality constraints
3. Phasenübergänge bei Zufallsproblemen
4. Lokale Suche (GSAT, WalkSAT, …, ProbSAT)
5. Resolution, Davis-Putnam-Algorithmus, DPLL-Algorithmus, Look-Ahead-Algorithmus
6. Effiziente Implementierungen, Datenstrukturen
7. Heuristiken im DPLL-Algorithmus
8. CDCL-Algorithmus, Klausellernen, Implikationsgraphen
9. Restarts und Heuristiken im CDCL-Algorithmus
10. Preprocessing, Inprocessing
11. Generierung von Beweisen und deren Prüfung
12. Paralleles SAT Solving (Guiding Paths, Portfolios, Cube-and-Conquer)
13. Verwandte Probleme: MaxSAT, MUS, #SAT, QBF
14. Fortgeschrittene Anwendungen: Bounded Model Checking, Planen, satisfiability-modulo-theories

2 SWS Vorlesung + 1 SWS Übungen

(Vor- und Nachbereitungszeiten: 4h/Woche für Vorlesung plus 2h/Woche für Übungen; Klausurvorbereitung: 15h)

Gesamtaufwand: (2 SWS + 1 SWS + 4 SWS + 2 SWS) x 15h + 15h Klausurvorbereitung = 9x15h + 15h = 150h = 5 ECTS

Lernziele:

• Studierende sind in der Lage, kombinatorische Probleme zu beurteilen, deren Schwere einzuschätzen und mittels Computern zu lösen.
• Studierende lernen, wie kombinatorische Probleme mittels SAT Solving effizient gelöst werden können.
• Studierende können die praktische Komplexität von Entscheidungs- und Optimierungsproblemen beurteilen, Probleme als SAT-Probleme kodieren und effiziente Lösungsverfahren für kombinatorische Probleme implementieren.