SAT Solving

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

U. Schöning, J. Toran: Das Erfüllbarkeitsproblem SAT. Lehmanns Media, 2012.