Logbuch zur Vorlesung SAT-Solving und Constraint-Satisfaction Probleme

Di, 18.10.2005: Organisatorisches, Überblick über den Inhalt der Vorlesung, grundlegende Definitionen, Anwendungsbeispiel, Negationsnormalform.
Do, 20.10.2005: Disjunktive und konjunktive Normalform, Umwandlung von Formeln in erfüllbarkeitsäquivalente KNF-Formeln, Komplexität von gSAT, SAT und 3-SAT, Definition von Horn-Formeln
Di, 25.10.2005: Das Problem Horn-SAT, Streichungsalgorithmus für Horn-SAT, einfache Spiele, Linearzeitalgorithmus zur Berechnung der Gewinnmengen in einfachen Spielen, konkrete C-Implementation des Algorithmus. Übungsblatt 1 ausgeteilt.
Do, 27.10.2005: Abschluß des Horn-SAT Beweises, Reduktion auf Spiele, 2-SAT und seine Komplexität.
Di, 1.11.2005: SAT(l), Resolution und der Davis-Putnam-Algorithmus, Kapitel 2: "DLL-Algorithmen" angefangen, allgemeines zu vollständigen vs. unvollständigen SAT-Algorithmen, Grundstruktur des Algorithmus von Davis, Logemann und Loveland, einfache Verbesserungen und Reduktionen, Unit Propagation und Pure Literals.
Do, 3.11.2005: Algorithmus von Monien und Speckenmeyer
Di, 8.11.2005: Der SAT-Algorithmus von Dantsin et al., Definition von Überdeckungscodes, lokale Suche in r-Kugeln, berechnen von Überdeckungscodes.
Do, 10.11.2005: Algorithmus von Dantsin et al., Abschluß von Kapitel 2.3
Di, 15.11.05: Kapitel 2.4 angefangen. Iterative Version des DLL-Algorithmus, Grundlagende Datenstrukturen und Verzweigungsheuristiken.
Do, 17.11.2005: Unit Propagation, Linearzeitalgorithmus für BCP sowie BCP mit Head/Tail-Listen. Amortisierte Komplexität des Verfahrens.
Do, 24.11.2005: BCP mit bewachten Literalen, Konfliktanalyse und das Lernen von Konfliktklauseln, Implikationsgraph und nicht-chronologisches Backtracking.
Di, 29.11.2005: Verzweigungsheuristik VSIDS, Abschluß des Kapitels über DLL-Algorithmen, Anwendung des SAT-Problems: Bounded Model Checking, Transitionssysteme, temporale Logik LTL, Grobstruktur des Bounded Model Checking.
Do, 1.12.2005: Bounded Model Checking, Übersetzung in die Aussagenlogik
Do, 8.12.2005: Abschluß des Kapitels über Anwendungen des SAT-Problems
Di, 13.12.2005: Kapitel 4: Beweiskomplexität, Einführung in Beweissysteme, reguläre und baumartige Resolution, Entscheidungsbäume
Do, 15.12.2005: Beweis des Zusammenhangs zwischen baumartiger Resolution und DLL-Läufen. Anfang des Kapitel 3.2. über untere Schranken für die Länge von Resolutionswiderlegungen.
Di, 3.1.2006: Beweis des Zusammenhangs zwischen Weite und Länge von Resolutionswiderlegungen. Definition von Tseitin-Formeln.
Do, 5.1.2006: Grundlegende Eigenschaften von Tseitin-Formeln, allgemeine Beweismethode zum Nachweis unterer Schranken für Resolutionswiderlegungen basierend auf dem Weite-Länge Zusammenhang.
Di, 17.1.2006: Nachweis von exponentiellen unteren Schranken für Resolutionswiderlegungen von Tseitin-Formeln.
Do, 19.1.2006: Abschluß des Beweises und Nachweis unterer Schranken für Schubfach-Formeln.
Di, 24.1.2006: Einführung des Cutting-Planes-Beweiskalküls. Beweis des Simulationslemmas.
Do, 26.1.2006: Abschluß des Kapitels über Cutting-Planes. Nachweis, daß PHP-Formeln mit kubischer Länge widerlegt werden können.

Arbeitsgruppe Logik in der Informatik