Das Erfüllbarkeitsproblem für logische Formeln — lässt sich eine gegebene logische Formel erfüllen? — ist eines der fundamentalen algorithmischen Probleme. Grund hierfür ist, dass sich viele andere wichtige algorithmische Probleme auf verschiedene Varianten des Erfüllbarkeitsproblems reduzieren lassen.
In diesem Seminar im Theoriebereich der Informatik wollen wir uns mit dem Erfüllbarkeitsproblem aus verschiedenen Perspektiven und für verschiedene Logiken beschäftigen.
Der Schwerpunkt wird auf dem Erfüllbarkeitsproblem für aussagenlogische Formeln und dem Erfüllbarkeitsproblem für (eingeschränkte) prädikatenlogische Formeln liegen:
- Das Erfüllbarkeitsproblem für aussagenlogische Formeln (SAT) ist die Grundlage der Theorie der NP-schwierigen Probleme: Jedes Problem aus NP lässt sich auf SAT zurückführen, ist also höchstens so schwierig wie SAT. Fortschritte beim Lösen von SAT übertragen sich deshalb auch in der Praxis oft auf andere Probleme aus NP.
- Das Erfüllbarkeitsproblem für (eingeschränkte) prädikatenlogische Formeln ist unter anderem die Grundlage für das Schlussfolgern in wissensbasierten Systemen und für die formale Verifikation von Hardware und Software. Für allgemeine prädikatenlogische Formeln ist das Erfüllbarkeitsproblem nicht algorithmisch lösbar (formal: unentscheidbar). In der Praxis werden daher oft eingeschränkte Klassen prädikatenlogischer Formeln benutzt, für die sich das Problem noch algorithmisch lösen lässt.
Ziel des Seminars ist es, ein gutes Verständnis dafür zu entwickeln, mit welchen Varianten des Erfüllbarkeitsproblem sich algorithmisch gut umgehen lässt und für welche Art von Problemstellungen dies jeweils hilfreich ist.
Einstiegsliteratur für dieses Seminar ist:
- Kroening, D. & O. Strichman. Decision procedures. Springer-Verlag Berlin Heidelberg, 2016.
- Biere, A., Heule, M., & van Maaren, H. (Eds.). (2009). Handbook of satisfiability (Vol. 185). IOS press.
- Börger, E., Grädel, E., & Gurevich, Y. (2001). The classical decision problem. Springer Science & Business Media.
Voraussetzungen:
- Erfolgreicher Besuch der Veranstaltung "Theoretische Informatik"
- Wünschenswert: Besuch der Veranstaltung "Logik in der Informatik"
Zielgruppe:
- Studierende im Bereich Informatik, d.h. der Studiengänge Informatik, Angewandte Informatik und ITS.
- Es wird geeignete Vortragsthemen für Bachelor- und Masterstudierende geben.
- Die Teilnehmerzahl ist auf 15 Personen beschränkt.
Anmeldung:
Voranmeldung bis spätestens 30.09.2021 (über Anmeldung im Moodle-Kurs)
Die Vorbesprechung findet voraussichtlich Anfang Oktober statt.
- Die verbindliche Anmeldung erfolgt mit Annahme des Vortragsthemas.
- Kursleiter/in: Felix Tschirbs
- Kursleiter/in: Thomas Zeume