KursbeschreibungDas Erfüllbarkeitsproblem (satisfiability problem, SAT) ist ein zentrales Problem der theoretischen Informatik und fragt, ob zu einer gegebenen
aussagenlogischen Formel (üblicherweise in konjunktiver Normalform) ein Modell existiert, d. h. eine Belegung aller in der Formel auftauchenden Variablen mit "wahr" oder "falsch", so dass die gesamte Formel zu "wahr" evaluiert. Dieses Problem ist NP-vollständig und algorithmische Lösungen benötigen daher im schlimmsten Fall exponentielle Laufzeit (unter üblichen komplexitäts theoretischen Annahmen). Viele Probleme der Informatik (beispielsweise Verifikationsprobleme) und insbesondere der KI (beispielsweise Planungsprobleme) können als Erfüllbarkeitsproblem modelliert werden und profitieren damit von ¨effektiven Lösungsstrategien für das Erfüllbarkeitsproblem. ¨
In diesem Seminar werden sowohl die Grundlagen als auch erweiterte Techniken zur algorithmischen Lösung des Erfüllbarkeitsproblems behandelt. Die Themen des Seminars folgen dabei der Struktur des ¨ Handbook of Satisfiability1.
Bitte beachten Sie, dass die gesamte Veranstaltung (inklusive der Präsentationen und der Ausarbeitung) auf Englisch stattfinden wird.