SAT Solving

Inhalt

Grundlagen

  • Aussagenlogik
  • Normalformen
  • kombinatorische Eigenschaften von (k-)SAT
  • Tseitin-Codierung
  • NP-Vollständigkeit von SAT

Kalkülbasierte Algorithmen

  • Resolution
  • Davis-Putnam (DP)

DPLL-Algorithmen

  • DPLL
  • Heuristiken wie Monien Speckenmeyer
  • Klausellernen

Lokale Suche

  • deterministische lokale Suche mit Überdeckungscodes
  • stochastische lokale Suche (SLS)
  • Heuristiken

Spezialfälle von SAT

  • 2-KNF
  • HORN
  • Renamable HORN

SAT Spezialthemen

  • SAT Schwellenwert (phase transition)
  • Lovasz Local Lemma

 

Literatur:

U. Schöning, J. Toran: Das Erfüllbarkeitsproblem SAT. Lehmanns Media, 2012.

 

 

Übungen

Es gibt weder Tutorien noch Übungen zu dieser Veranstaltung.

Vorlesungszeiten

Montag 14-16 Uhr in O27 - 2203

Donnerstag 12-14 Uhr in O27 - 2203

Tutorien

keine

Weitere Informationen

LSF-Eintrag