Logik in der Informatik
Prof. Dr. Martin Grohe

Institut für Informatik

Seminar SAT-Solver in Theorie und Praxis

Aktuelles  Einführung  Zeit&Raum  Literatur  Vorträge

Aktuelles

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

Ab sofort (Montag, 21.06.04) findet das Seminar im Raum 4.410 (RUD 25) statt.

Einführung

Das aussagenlogische Erfüllbarkeitsproblem (SAT) ist ein algorithmisches Problem von zentraler Bedeutung für die Informatik. Theoretisch ist es wichtig, weil es das "generische" NP-vollständige Problem ist, auf das sich zahlreiche andere Probleme leicht reduzieren lassen. Praktisch ist es wichtig, weil sich Programme zur Lösung von SAT (sog. SAT-Solver) vielseitig als Werkzeuge in verschiedenen Anwendungsbereichen einsetzen lassen, etwa in der automatischen Verifikation und in der künstlichen Intelligenz.

Obwohl SAT NP-vollständig und damit theoretisch "schwer" ist, lassen sich mit modernen SAT-Solvern in der Praxis mittlerweile sehr große Formeln (mit mehreren Millionen Variablen) auf Erfüllbarkeit testen. Es liegt also eine gewisse Diskrepanz zwischen den theoretischen Vorhersagen und der Praxis vor, deren Untersuchung ein wichtiges Thema der aktuellen Forschung ist.

Themen des Seminars sind die algorithmischen und komplexitätstheoretischen Grundlagen von SAT, die in praktischen SAT-Solvern eingesetzten Verfahren sowie Anwendungen von SAT-Solvern.

Zeit und Raum

Montags 15-17 im Johann von Neumann Haus (Rudower Chaussee 25), Raum 4.112

Literatur

Wir haben versucht, zu möglichst vielen Artikeln, einen Link zu einer elektronischen Version anzugeben. Sollte kein solcher Link bekannt sein, so kann die Literatur am Lehrstuhl  eingesehen und kopiert werden.

Weitere interessante Quellen lassen sich mittels CiteSeer und SATLive finden.
 
[Ach01]
Dimitris Achlioptas. A Survey of Lower Bounds for Random 3-SAT via Differential Equations. Theoeretical Computer Science 265 (2001), S. 159-185. Erhältlich hier als Postscript.
[BCCSZ03]
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman und Yunshan Zhu. Bounded Model Checking. Advances in Computers, 2003.
[CBRZ01]
Edmund Clarke, Armin Biere, Richard Raimi und Yunshan Zhu. Bounded Model Checking Using Satisfiability Solving. Formal Methods of System Design, 2001. Erhältlich hier als PDF.
[Dub01]
Olivier Dubois. Upper bounds of the satisfiability threshold. Theoretical Computer Science 265 (2001), S. 187-197. Erhältlich hier als PDF.
[GN02]
Evgueni Goldberg und Yakov Novikov. BerkMin: a Fast and Robust Sat-Solver. Design, Automation and Test in Europe, S. 142-149. Erhältlich hier als PDF.
[IT03]
Kazuo Iwama und Suguru Tamaki. Improved Upper Bounds for 3-SAT. Electronic Colloquium on Computational Complexity, Report Nr. 53, 2003. Erhältlich hier als PDF:
[Joh03]
Dr. Jan Johannsen. Algorithmen für das SAT-Problem. Skript zur gleichnamigen Vorlesung. Erhältlich hier als Postscript (neben einigen weiteren interessanten Links)
[McM03]
K.L. McMillan. Interpolation and SAT-based model checking. Proceedings of CAU'03, 2003. Erhältlich hier als Postscript.
[M-SS99]
Joao P. Marques-Silva, Karem A. Skallah. GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Treansactions on Computers, Vol. 48, No. 5. 1999. Erhältlich hier als PDF.
[MMZZM01]
Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang und Sharad Malik. Chaff: Engineering an Efficient SAT Solver. Proceedings of the 38th Design Automation Conference. 2001. Erhältlich hier als PDF.
[PPSZ02]
Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, Francis Zane. An Improved Exponential-time Algorithm for k-SAT. 2002. Proceedings of the 39th Annual Symposium on Foundations of Computer Science. 2002. Erhältlich hier als PDF.
[Sch99]
Uwe Schöning. A Probabilistic Algorithm for k-SAT and Constraint Satisfaction Problems. Proceedings of the 40th Annual Symposium on Foundations of Computer Science. 2002. Erhältlich hier als PDF.
[SKC95]
Bart Selman, Henry Kautz und Bram Cohen. Local Search Strategies for Satisfiability Testing. DIMACS Series in Discrete Mathematics and Theoretical Computer Science 26, S. 521-536. 1996. Erhältlich hier als Postscript.
[SW00]
Eli Ben-Sasson und Avi Wigderson. Short Proofs are Narrow - Resolution Made Simple. Journal of the ACM Vol. 48, Nr. 2, S. 149-169. 2001. Erhältlich hier als Postscript.
[ZM02]
Lintao Zhang. Sharad Malik. The Quest for Efficient Boolean Satisfiability Solvers. Proceedings of the 8th International Conference on Computer Aided Deduction. 2002. Erhältlich hier als PDF.

Vortragsthemen und -termine

Datum
Thema
Referent/Referentin
Literaturhinweise
10.05.04
DPLL-Algorithmen
Janis Bardins
[Joh03]
17.05.04
GRASP und Chaff
Kevin Bierhoff
[Joh03], [M-SS99], [MMZZM01], [ZM02]
24.05.04
SAT-Solver in der Verifikation
Christian Gierds
[BCCSZ03], [CBRZ01], [McM03]
14.06.04
Untere Schranken für resolutionsbasierte Algorithmen
Dzifa Ametowobla
[SW00]
21.06.04
Zufällige Formeln
Florian Kühnert
[Dub01], [Ach01]
28.06.04
Randomisierte lokale Suche
Bettina Hepp
[Sch99],  [SKC95]
5.07.04
Die Algorithmen von Paturi, Pudlkak, Saks, Zane und von Iwama, Tamaki
Marc Thurley
[PPSZ02], [IT03]

Last modified: Mon Jun 21 10:30:00 CEST 2004
Martin Grohe