Modul
SAT Solving in der Praxis (erweitert) [M-INFO-105622]
Leistungspunkte
6Turnus
UnregelmäßigDauer
1 SemesterSprache
Deutsch/EnglischLevel
4Version
1Verantwortung
Einrichtung
- KIT-Fakultät für Informatik
Bestandteil von
Teilleistungen
Identifier | Name | LP |
---|---|---|
T-INFO-111254 | SAT Solving in der Praxis (erweitert) | 6 |
Erfolgskontrolle(n)
Siehe Teilleistung.
Qualifikationsziele
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.
Studierende erhalten einen Einblick in die modernsten Lösungverfahren für SAT und verwandte Probleme und deren Implementierungen in SAT Solvern.
Voraussetzungen
Siehe Teilleistung.
Inhalt
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:
- Grundlagen, historische Entwicklung
- Codierungen, z.B. cardinality constraints
- Phasenübergänge bei Zufallsproblemen
- Lokale Suche (GSAT, WalkSAT, ..., ProbSAT)
- Resolution, Davis-Putnam-Algorithmus, DPLL-Algorithmus, Look-Ahead-Algorithmus
- Effiziente Implementierungen, Datenstrukturen
- Heuristiken im DPLL-Algorithmus
- CDCL-Algorithmus, Klausellernen, Implikationsgraphen
- Restarts und Heuristiken im CDCL-Algorithmus
- Preprocessing, Inprocessing
- Generierung von Beweisen und deren Prüfung
- Paralleles SAT Solving (Guiding Paths, Portfolios, Cube-and-Conquer)
- Verwandte Probleme: MaxSAT, MUS, #SAT, QBF
- Fortgeschrittene Anwendungen: Bounded Model Checking, Planen, satisfiability-modulo-theories
Zusätzlich:
- Erfolgsstrategien der aktuell besten SAT Solver, z.B. Vivification, Rephasing, Conditional Chronological Backtracking, Gaussian Eliminiation / XOR Reasoning, etc.
- Instanz-spezifische Algorithmenselektion und -konfiguration
- Effizientes Erkennen von Gate-Kodierungen in CNF Formeln
- Model Counting (#SAT): Algorithmen und Anwendungen
Arbeitsaufwand
3 SWS Vorlesung + 1 SWS Übungen
(Vor- und Nachbereitungszeiten: 5h/Woche für Vorlesung plus 2h/Woche für Übungen; Klausurvorbereitung: 15h)
Gesamtaufwand: (3 SWS + 1 SWS + 5 SWS + 2 SWS) x 15h + 15h Klausurvorbereitung = 11x15h + 15h = 180h = 6 ECTS