SAT Solving

Aktuelles

• Das Seminar findet am 11.-12. März 2013 jeweils ab 10 Uhr c.t. im Seminarraum 061, Oettingenstr. 67 statt.
  

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.308ⁿ) für 3-SAT und O(1.469ⁿ) für 4-SAT.

Andererseits gibt es für die klassischen Backtracking Algorithmen (DPLL) sehr gute Heuristiken und Implementierungen, die selbst sehr große Testinputs in akzeptabler Zeit bewältigen. Diese sog. SAT Solver  zeigen inzwischen so gute Performanz, dass sie für realistische Anwendungen zur Lösung kombinatorischer Optimierungsprobleme eingesetzt werden.

Im Seminar sollen diese Algorithmen, Techniken und Anwendungen sowie Ansätze zum Beweis unterer Schranken an die Laufzeit kennengelernt werden.

Vortragsthemen

Vollständige Algorithmen

• DPLL-Algorithmen, Anna Mira Steiger
  
• Der Algorithmus von Monien und Speckenmeyer, Stefan Faßrainer
  
• Der Algorithmus von Zhang, Raffaella Germano
  

Implementierung

• Implementierung von DPLL, André Reichstaller
  
• CDCL Solver, Otto Voggenreiter
  

Einfache Spezialfällle

• Formeln in 2-CNF, Patrick Zemanyk
  
• Horn-Formeln, Tobias Rosenberger
  
• Formeln mit 2 Variablenvorkommen, Thomas Ledwon
  

Probabilistische Algorithmen

• Der Algorithmus von Schöning, Philipp Martinek
  
• Der Algorithmus von Paturi, Pudlák und Zane, Riccardo Valentini
• Der Algorithmus von Paturi. Pudlák, Saks und Zane und dessen Analyse von Hertli, Stephan Barth
  

Anwendungen

• Bounded Model Checking, Mathias Hüsing
  
• Superoptimierung, Bernhard Fabry
  

Organisation

• Umfang: 2 Semesterwochenstunden
• Betreuung: Dr. Jan Johannsen
• Zum Seminar ist für Studierende in den Bachelorstudiengängen Informatik und Medieninformatik eine Bewerbung über die zentrale Seminaranmeldung bis zum 7. 10. 2012 nötig. Studierende in anderen Studiengängen können sich per Email beim Betreuer bewerben.

Anforderungen

• Vortrag: 30 Minuten + 10 Minuten Diskussion
• Anwesenheit während der Seminarsitzungen
• Ausarbeitung zum Thema von 7000-14000 Zeichen
• Bei Master- und Diplomstudenten werden die Anforderungen mit dem Betreuer abgesprochen.

Zeit und Ort

Das Seminar findet als Blockseminar am 11.-12. März 2013 um 10 Uhr c.t. bis ca. 18 Uhr im Seminarraum 061, Oettingenstr. 67 statt.

Weitere Informationen

Bestandene Prüfung in Formale Sprachen und Komplexität, Theoretische Informatik oder Logik und Diskrete Strukturen ist wünschenswert, Teile der Inhalte werden vorausgesetzt.