Vorlesung SAT-Solving und Constraint-Satisfaction Probleme

Aktuelles

An dieser Stelle finden Sie im Laufe der Vorlesung aktuelle Mitteilungen. Bitte sehen Sie regelmäßig nach, ob es Neues gibt.

Auf allgemeinen Wunsch beginnt die Vorlesung jetzt jeweils erst um 9.30 Uhr.

Einführung

Im Zentrum der Vorlesung steht das Erüllbarkeitsproblem der Aussagenlogik (kurz SAT-Problem), d.h. das Problem, zu einer gegebenen Formel der Aussagenlogik zu entscheiden, ob sie eine erfüllende Belegung besitzt. Wegen seiner Allgemeinheit lassen sich viele praktische Probleme auf das SAT-Problem reduzieren. So findet das Problem Anwendungen im Bereich der Planungsprobleme in der künstlichen Intelligenz, im Bereich des Model-Checkings und verschiedenen anderen Gebieten.
Obschon das Problem 1971 von Cook als NP-vollständig nachgewiesen wurde, sind in den letzten Jahren SAT-Solver entwickelt worden, die Formeln mit vielen tausend Variablen routinemäßig auf Erfüllbarkeit hin überprüfen können. Erst diese Algorithmen erlauben die Anwendung des SAT-Problems im industriellen Maßstab. Im Verlauf des Vorlesung werden wir verschiedene sehr unterschiedliche Verfahren und Methoden rund um das SAT-Problem kennen lernen. Zunächst werden die verschiedenen Ansätze zur Entwicklung von Algorithmen zur Lösung des Problems vorgestellt, insbesondere die auf dem DLL-Algorithmus aufbauenden Suchverfahren sowie randomisierte Algorithmen. Daneben werden wir auf die verschiedenen praktischen Anwendungen des Problems eingehen, z.B. im Bereich des Bounded-Model-Checking. Einen wichtigen Teil der Vorlesung werden aber auch Methoden einnehmen, mit denen untere Schranken für die Laufzeit von SAT-Algorithmen nachgewiesen werden können.

Inhaltverzeichnis

• Grundlagen
  • Aussagenlogik
  • Erste Anwendungen
  • Normalformen
  • Das Erfüllbarkeitsproblem der Aussagenlogik und seine Komplexität
  • Einfache Spezialfälle
  • Resolution und der Davis-Putnam-Algorithmus
• DLL-Algorithmen
• Der Algorithmus von Davis, Logemann und Loveland
• Der Algorithmus von Monien und Speckenmeyer
• Wenn viele Leute einen Algorithmus entwerfen
• Struktur und Implementierung DLL-basierter SAT-Löser
• Anwendungen des SAT-Problems
• Untere Schranken für die Laufzeit von Algorithmen
• Der Satz von Schäfer und effizient lösbare Spezialfälle
• Randomisierte Algorithmen

Logbuch

Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungen und gelegentlich ergänzende Bemerkungen.

Informationen zum Vorlesungsbetrieb

Zeiten und Raum

Dienstags 9-11 und Donnerstags 9-11 im Erwin Schrödinger Zentrum (Rudower Chaussee 26), Raum 1'308

 

Dozent

Prof. Dr. Stephan Kreutzer

Übungen

Ergänzend zu den Vorlesungen finden 2-stündige Übungen statt.

Zeit und Raum

Donnerstag 11-13 im Erwin Schrödinger Zentrum (Rudower Chaussee 26), Raum 1'308

 

Übungsleiter

Prof. Dr. Stephan Kreutzer

Übungsaufgaben

Es wird regelmäßig Übungsaufgaben geben, deren erfolgreiche Bearbeitung (mindestens 40% der Punkte) Voraussetzung für den Scheinerwerb und die Zulassung zur Prüfung ist.

• Blatt 1 (ausgeteilt am 25.10.2005; Abgabe: Dienstag, den 1.11.2005 zu Beginn der Vorlesung)
• Blatt 2 (ausgeteilt am 1.11.2005; Abgabe: Dienstag, den 8.11.2005 zu Beginn der Vorlesung)
• Blatt 3 (ausgeteilt am 8.11.2005; Abgabe: Dienstag, den 15.11.2005 zu Beginn der Vorlesung)
• Blatt 4 (ausgeteilt am 15.11.2005; Abgabe: bis spätestens Donnerstag, 24.11.2005 zu Beginn der Vorlesung)
  Die Aufgabe 3 des Blattes muß selbstverständlich erst zum Ende der Vorlesung Anfang Februar abgegeben werden. Genaueres wird während der kommenden Übungsstunden besprochen.
• Zu Kapitel 2.4 (Implementierung von SAT-Lösern) gibt es kein eigenes Übungsblatt, sondern die Zeit soll zur Implementierung Ihres SAT-Lösers genutzt werden.
• Blatt 5 (ausgeteilt am 29.11.2005; Abgabe: bis Donnerstag, den 8.12.2005 vor der Vorlesung)
• Blatt 6 (ausgeteilt am 13.12.2005; Abgabe: Dienstag, den 3.1.2006 vor der Vorlesung)
• Blatt 7 (ausgeteilt am 5.1.2006; Abgabe: Dienstag, den 17.1.2006 vor der Vorlesung)
• Blatt 8 (ausgeteilt am 17.1.2006; Abgabe: Dienstag, den 24.1.2006 vor der Vorlesung)
• Blatt 9 (ausgeteilt am 24.1.2006; Abgabe: Dienstag, den 31.1.2006 vor der Vorlesung)

Prüfung

Zu Beginn der Semesterferien finden mündliche Prüfungen statt. Für die Zulassung zur Prüfung müssen mindestens 40% der Punkte in den Übungaufgaben erworben werden.

Materialien

• Web-Seiten aktueller SAT-Löser:
  • BerkMin. Siehe hier . Beschrieben wird der SAT-Löser in BerkMin: a Fast and Robust Sat-Solver von Goldberg und Novikov, erschienen in DATE 2002.
  • Chaff: Der SAT-Löser chaff kann hier runtergeladen werden. Beschrieben wird chaff in dem Paper Chaff: Engineering an Efficient SAT Solver von Moskewicz, Madigan, Zhao, Zhang und Malik erschienen in den Proceedings der Design and Automation Conference 2001.
  • GRASP: Siehe hier. Beschrieben in GRASP: A Search Algorithm for Propositional Satisfiability von Marques-Silve und Sakallah, erschienen in IEEE Transactions on Computers, Vol 48 no. 5, 1999.
  • Benchmarks können Sie hier finden.
  • Weitere Informationen finden Sie auch auf der "SAT Experimentierseite".
  • Das DIMACS-Format für SAT-Formeln wird in einem Artikel beschrieben, den Sie hier finden können. Bitte verwenden Sie das vorgeschlagene cnf-Format für Ihren SAT-Löser. (Sie brauchen keine Kommentare zuzulassen.)

  Literatur

  Die Vorlesung orientiert sich nicht an einem konkreten Buch. Literaturangaben zu den einzelnen Teilen der Vorlesung wird jeweils in der Vorlesung bekannt gegeben. Hier ist eine immer wieder aktualisierte Liste mit Referenzen zu einzelnen Kapiteln der Vorlesung.
  • Skript zur Vorlesung Algorithmen für das SAT-Problem von Dr. Jan Johannsen, gehalten an der LMU München im Sommersemester 2005.
    Kapitel 1 des Skriptes enthält viel von dem Material, was in Kapitel 1 dieser Vorlesung behandelt worden ist.
  • Uwe Schöning, Algorithmik, Spektrum Verlag.
    Das Buch bietet eine Einführung in Algorithmen und enthält unter anderem ein Kapitel über SAT-Algorithmen. Einige der in der Vorlesung behandelten Algorithmen finden sich hier wieder, teilweise in anderer Form.
  • L.Zhang, S.Malik, The Quest for Efficient Boolean Satisfiability Solvers, CAV 2002, Springer Lecture Notes in Computer Science, Vol. 2404, Springer, 2002.
    Sehr schöner Übersichtsartikel über aktuelle SAT-Löser. Mehr Details finden Sie in den Arbeiten über die SAT-Löser GRASP, BerkMin, Chaff, die Sie in der Refenzliste der Zhang, Malik-Arbeit finden.