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.

Vorlesungszeiten

Montag 12:00 - 14:00 Uhr in O27/2201

Mittwoch 12:00 - 14:00 Uhr O27/2201