Home | english  | Impressum | Sitemap | KIT

SAT Solving in der Praxis

SAT Solving in der Praxis
Typ: Vorlesung Links:
Ort:

Seminarraum 236 (Geb. 50.34)

Zeit:

Mo 14:00-15:30

Beginn: 18.04.2016
Dozent:

T. Balyo, C. Sinz

SWS: 3 (2 Vorlesung, 1 Übung)
ECTS: 5
LVNr.: 2400085
Prüfung:

mündlich (Termine: 25.07.2016 und 19.09.2016)

Hinweis:

Die Vorlesung wird auf Englisch gehalten.

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

  • Montag, 18.04.2016: Vorbesprechung, Einführung ins Thema
  • Die Übungen zur Vorlesung finden 14-tägig donnerstags von 14:00-15:30 Uhr statt

Vorlesungsfolien

Noch keine veröffentlicht.

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.