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 12-14 Uhr   in O27 - 2202

Mittwoch 12-14 Uhr in O27 - 2201

Der erste Vorlesungstermin ist am Mittwoch, 14.10.2015.

Weitere Informationen

LSF-Eintrag