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: wird in der Vorlesung ausgegeben

 

Übungen

Es gibt weder Tutorien noch Übungen zu dieser Veranstaltung.

Übungsleiter

keiner

Tutorien

keine