Institut für Theoretische Informatik, Algorithmik II

SAT Solving in der Praxis

  • Typ: Vorlesung
  • Semester: SS 2020
  • Ort:

    Geb. 50.34, R. 131

  • Zeit:

    Montag 11.30-13.00 Uhr
    Donnerstag 14.00 -15.30 Uhr
     

  • Dozent:

    Prof. Dr. Carsten Sinz
    Markus Iser
     

  • SWS: 3
  • LVNr.: 2400105

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.