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.