Lehr- und Forschungseinheit für Theoretische Informatik,
Institut für Informatik
der Ludwig-Maximilians-Universität München
Vorlesung im Hauptstudium (WS 02/03):
Algorithmen für das SAT-Problem
- Vorlesung:
- Dr. Jan
Johannsen, 2-stündig
- Zeit und Ort: Mi 12 - 14, Raum 0.13, Oettingenstraße
67
- Beginn: 16. 10. 2002
- Übung:
-
Dr. Jan Johannsen, 2-stündig
- Zeit und Ort der Übung: Fr 12 - 14, Raum 252,
Theresienstraße 39
- Beginn: 29. 10. 2002
- Vorkenntnisse:
-
Grundbegriffe der Aussagenlogik
Effiziente Algorithmen
- Hörerkreis: :
- Studierende der Informatik im Hauptstudium
- Studierende mit Nebenfach Informatik
- Schein:
- Schein gilt für Diplomprüfung in
Haupt- und Nebenfach Informatik
- Scheinerwerb durch Kolloquium
zurück zum
Inhaltsverzeichnis dieser Seite
Das Erfüllbarkeitsproblem für die Aussagenlogik (SAT) ist das
kanonische NP-vollständige Problem, daher sind Algorithmen zu
seiner Lösung von wesentlicher Bedeutung für die
theoretische Informatik, ihre Entwicklung und Untersuchung bildet
einen ganzen eigenen Forschungszweig.
In letzter Zeit wurden auf diesem Gebiet große Fortschritte
erzielt, und zwar in sowohl theoretischer als auch praktischer
Natur. Auf der theoretischen Seite gibt es neue Algorithmen, für die sich
worst-case Schranken an die Laufzeit zeigen lassen, die besser
sind als die O(2n) für die brute-force Suche. Der
derzeit beste (probabilistische) Algorithmus erreicht für
3-SAT eine Laufzeit von O(1.3302n).
Andererseits gibt es für die klassischen Backtracking
Algorithmen (DLL) sehr gute Heuristiken und Implementierungen, die
selbst sehr große Testinputs in akzeptabler Zeit
bewältigen.
Diese zeigen inzwischen so gute Performanz, dass sie für
realistische Anwendungen zur Lösung kombinatorischer
Optimierungsprobleme eingesetzt werden. Neben Algorithmen aus
beiden Klassen sollen insbesondere auch solche Anwendungen,
z.B. für Planungsprobleme, Codeoptimierung und
Hardware-Verifikation, präsentiert werden.
- Grundlagen
- Aussagenlogik: Syntax und Semantik
- Das SAT Problem und seine Komplexität
- Einfache Fälle: 2-SAT und Horn-SAT
- DLL-Algorithmen
- Backtracking
- Reduktionen
- Algorithmus von Monien-Speckenmeyer
- Analysemethode von Kullmann
- Algorithmus von Zhang
- Effiziente Implementierung von DLL-Algorithmen
- Datenstrukturen
- Reduktionen
- Verzweigungsheuristiken
- Konfliktanalyse und Lernen
- Lokale Suche und Random Walks
- Hammingkugel-Algorithmus
- Random Walk-Verfahren
- Heuristische Verfahren
- Anwendungen
- Probabilistisches Verzweigen
- Algorithmus von Paturi-Pudlák-Saks-Zane
- Vorlesungsskript
- Aktuelle Übersichts- und Forschungsarbeiten, die in der Vorlesung
bekannt gegeben werden.
- Einiges Material ist in den folgenden Büchern zu finden, im
zweiten vor allem Grundlegendes.
- U. Schöning: Algorithmik, Spektrum Akademischer Verlag, 2001
- Kleine Büning / Lettman: Aussagenlogik: Deduktion und Algorithmen,
Teubner 1994
zurück zum
Inhaltsverzeichnis dieser Seite
SAT Solver:
- Chaff (Lintao Zhang, Sharad Malik, Princeton)
- SATO
(Hantao Zhang, Iowa)
- GRASP (J.P. Marques
Silva, Lissabon)
- WalkSAT (Henry Kautz, Washington, Bart Selman, Cornell)
Benchmarks: