SAT-Solving

Lehrveranstaltung mit SWS 2/2/0 (Vorlesung/Übung/Praktikum) in SS 2015

Dozent

Steffen Hölldobler
Norbert Manthey

Tutor

Peter Steinke

Umfang (SWS)

2/2/0

Module

Leistungskontrolle

Mündliche Prüfung

Information
Termine und Unterlagen

Vorlesung: Montag, 4. DS Übung: Montag, 5. DS

Die Vorlesung beginnt immer 13:15 und endet dafür 14:45 Uhr

Das Erfüllbarkeitsproblem (SAT) der Aussagenlogik ist ein fundamentales Entscheidungsproblem der Informatik, und das repräsentative Problem der Komplexitätsklasse NP. Neben vielen akademischen Anwendungen, die sich auf SAT reduzieren lassen, gibt es auch industriell relevante Probleme, die gelöst werden können. Einige Beispiele sind das Lösen von Sudokus, das Lösen von Hamiltonion Path und Hamiltonian Cycle Problemen, aber auch die Verifikation von Hardware und Software. Selbst Attacken auf Crypthographie-Verfahren sind mit SAT möglich.

In den letzten zwei Jahrzehnten wurden SAT Solver -- Algorithmen die das Efüllbarkeitsproblem lösen -- wesentlich verbessert, und gehen weit über den DPLL Algorithmus der 1960er hinaus. Die Vorlesung präsentiert zum einen die theoretischen Grundlagen, auf denen SAT Solver aufbauen und führt Lösungsalgorithmen abstrakt ein und diskutiert Eigenschaften, die ausgenutzt werden können, um effiziente SAT Solver zu erhalten.

Auf der anderen Seite werden interna von SAT Solvern beleuchtet, und verwandte Anwendungen aufgezeigt. So kann mit MaxSAT -- der Optimierungsvariante des Erfüllbarkeitsproblems -- eine beste Lösung gefunden werden, oder durch mehrfaches Aufrufen eines Solvers eine kleinste unerfüllbare Teilformel gefunden werden. Die Varianten des Lösens werden ebenso diskutiert, wie das parallele Lösen des SAT Problems. Dabei wird auch auf die effiziente Implementierung geachtet.

In den Übungen werden sowohl theoretische als auch praktische Aufgabenstellungen gegeben. Es sollen sowohl Lösungsalgrithmen implementiert, als auch Probleme auf das SAT Problem reduziert werden.

Veranstaltungskalender abonnieren (icalendar)

Vorlesung	SAT Introduction	DS5, 13. April 2015 in APB E005	Datei
Übung	Exercise 1	DS5, 20. April 2015 in APB E005	Datei
Vorlesung	SAT Problems	DS5, 20. April 2015 in APB E005	Datei
Übung	Exercise 2	DS5, 27. April 2015 in APB E005	Datei
Vorlesung	Systematic Search	DS4, 4. Mai 2015 in APB E005	Datei
Übung	Exercise 3	DS5, 4. Mai 2015 in APB E005	Datei
Übung	Exercise 4	DS5, 1. Juni 2015 in APB E005	Datei
Vorlesung	Stochastic Local Search	DS4, 8. Juni 2015 in APB E005	Datei
Übung	Exercise 5	DS5, 8. Juni 2015 in APB E005	Datei
Vorlesung	SAT Algorithms	DS4, 15. Juni 2015 in APB E005	Datei
Vorlesung	SAT - Programming	DS4, 22. Juni 2015 in APB E005	Datei
Vorlesung	Konflikt Analyse	DS4, 29. Juni 2015 in APB E005	Datei
Übung	CNF Benchmark	DS5, 29. Juni 2015 in APB E005	Datei
Vorlesung	Simplification	DS4, 6. Juli 2015 in APB E005	Datei
Vorlesung	Parallel SAT Solving	DS4, 13. Juli 2015 in APB E005	Datei

Kalender