| NUMMER: | 211117 |
| KÜRZEL: | SS |
| MODULBEAUFTRAGTE:R: | Prof. Dr. Thomas Zeume |
| DOZENT:IN: | Dr. Nils Vortmeier |
| FAKULTÄT: | Fakultät für Informatik |
| SPRACHE: | Deutsch |
| SWS: | 2 |
| CREDITS: | 3 |
| ANGEBOTEN IM: | unregelmäßig |
VERANSTALTUNGSART
rechnerbasierte PräsentationTafelanschrieb
PRÜFUNGEN
| FORM: | Seminarbeitrag, studienbegleitend |
| TERMIN: | Siehe Prüfungsamt. |
LERNFORM
Seminar
LERNZIELE
siehe Inhalt
INHALT
Das Erfüllbarkeitsproblem für logische Formeln — lasst sich eine gegebene logischeFormel 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 schwierigen Probleme: Jedes Problem aus NP lässt sich auf SAT zurückfuhren, 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.
VORAUSSETZUNGEN CREDITS
Bestandener Seminarbeitrag
EMPFOHLENE VORKENNTNISSE
Keine