Seminar Satisfiability

NUMMER: 150562
KÜRZEL: SS
MODULBEAUFTRAGTE:R: Prof. Dr. Thomas Zeume
DOZENT:IN: Prof. Dr. Thomas Zeume
FAKULTÄT: Fakultät für Informatik
SPRACHE: Deutsch
SWS: 2
CREDITS: 3
WORKLOAD: 90 Stunden
ANGEBOTEN IM: jedes Wintersemester

PRÜFUNGEN

FORM: Seminarbeitrag, studienbegleitend
ANMELDUNG:
DATUM: 0000-00-00
BEGINN: 00:00:00
DAUER:
RAUM:

LERNFORM

Seminar

LERNZIELE

siehe Inhalt

INHALT

Das Erfüllbarkeitsproblem für logische Formeln — lasst 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 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

Keine

EMPFOHLENE VORKENNTNISSE

Keine