|
Logik in der Informatik
Prof. Dr. Martin Grohe |
 Institut für Informatik |
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.
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.
Montags 15-17 im Johann von Neumann Haus (Rudower Chaussee 25), Raum 4.112
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.
| [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. |
| 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] |