Vorlesung im Hauptstudium (SS 2005):

Algorithmen für das SAT-Problem

Inhaltsverzeichnis dieser Seite

Organisatorisches

Aktuelles:

Die Vorlesung findet ab Dienstag den 7.6.2005 wieder statt und vertretungsweise von Klaus Aehlig gehalten. Die Übungen finden bis auf weiteres nicht statt.

Vorlesung:

Dr. Jan Johannsen, 4-stündig

Zeit und Ort: Di 12:00 - 13:30, Mi 10:15-11:45, Raum 17, Oettingenstraße 67

Beginn: 12. April 2005

Übung:

Dr. Jan Johannsen, 2-stündig

Zeit und Ort der Übung: Do 16:30 - 18:00, Raum 17, Oettingenstraße 67

Beginn: 21. April 2005

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 Mitarbeit in Übungsgruppen

Inhalt

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(2ⁿ) für die brute-force Suche. Der derzeit beste (probabilistische) Algorithmus erreicht eine Laufzeit von O(1.324ⁿ) für 3-SAT und O(1.474ⁿ) für 4-SAT.

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, speziell aus der Hardware-Verifikation (Model Checking), aber auch aus den Bereichen Planungsprobleme und Codeoptimierung präsentiert werden.

Gliederung

• Grundlagen
  • Aussagenlogik: Syntax und Semantik
  • Das SAT Problem und seine Komplexität
  • Einfache Fälle: Horn-SAT, 2-SAT und SAT(2)
• DLL-Algorithmen
  • Backtracking
  • Reduktionen
  • Algorithmus von Monien-Speckenmeyer
  • Analysemethode von Kullmann
  • Algorithmus von Zhang
• Effiziente Implementierung von DLL-Algorithmen
  • Datenstrukturen
  • Effiziente unit propagation
  • Verzweigungsheuristiken
  • Konfliktanalyse und Lernen
• Probabilistische Algorithmen
  • Hammingkugel-Algorithmus
  • Random Walk-Verfahren
  • Algorithmus von Paturi-Pudlák-Saks-Zane
• Anwendungen
  • Bounded Model Checking
• Beweiskomplexität
  • DLL und Resolution
  • Untere Schranken für Resolution
  • Effiziente Interpolation
  • Anwendung für Model Checking

Literatur

• Vorlesungsskript zur Vorlesung im WS 02/03, das für die aktuelle Vorlesung überarbeitet und ergänzt wird.
• 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

Material zur Vorlesung

Skript:

• Kapitel 1, Version vom 26.04.05
• Kapitel 2, Version vom 08.07.05
• Kapitel 4, Version vom 08.07.05
• Kapitel 6, Version vom 30.09.05

SAT Solver:

• Chaff (Lintao Zhang, Sharad Malik, Princeton)
• Limmat und Compsat (Armin Biere, Linz)
• Jerusat (Alexander Nadel, Tel Aviv)
• BerkMin (Eugene Goldberg, Berkeley und Yakov Novikov, Minsk)
• SATO (Hantao Zhang, Iowa)
• GRASP (J.P. Marques Silva, Lissabon)
• WalkSAT (Henry Kautz, Washington, Bart Selman, Cornell)

Benchmarks:

• SATLIB Benchmark Problems
• SAT-Ex SAT Experimentation website

Übungen

• Blatt 1 ( ps , pdf )
• Blatt 2 ( ps , pdf )
• Blatt 3 ( ps , pdf )
• Blatt 4 ( ps , pdf )
• Blatt 5 ( ps , pdf )
• Blatt 6 ( ps , pdf )