Vorlesungsinhalte

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 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

Organisatorisches

Die Übungen zur Vorlesung finden 14-tägig donnerstags von 14:00-15:30 Uhr im ATIS-SR 010 statt, erster Termin am 27.04.2017.

Vorlesungsfolien

Siehe Link oben rechts auf der Seite.

Literatur

A. Biere, M. Heule, H. Van Maaren, T. Walsh: Handbook of Satisfiability, IOS Press, 2009.
D. Knuth: The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability, 2015.