SAT Solving

Eine Klausur wird für die SAT Solving Vorlesung nicht angeboten. Prüfungstermine bitte mit Frau Fromm abklären.

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
• Mixed-HORN
• Renamable HORN

SAT Spezialthemen

• SAT Schwellenwert (phase transition)
• Lovasz Local Lemma

Literatur:

• Script
• Begleit CD zur Vorlesung

Es gibt weder Tutorien noch Übungen zu dieser Veranstaltung.