Allgemeines

Veranstaltungsnummer  -
Veranstalter Jens Keppeler
Klassifikation Proseminar
Semester Sommersemester 2021
Ort und Zeit  Ort & Zeit siehe Moodle
Vorbesprechung n. a.
Querverbindungen Logik
Voraussetzungen wünschenswert DAP-2, MafI I + II, Logik

 

Inhalt

Ist eine gegebene aussagenlogische Formel erfüllbar? Mit dieser Frage beschäftigt sich das SAT-Problem, welches eines der zentralen Entscheidungsprobleme der theoretischen Informatik ist.
Da dieses Problem NP-vollständig ist (Satz von Cook und Levin), ist insbesondere unklar, ob es Algorithmen gibt, die das Problem in polynomieller Zeit lösen können.
Das SAT-Problem ist auch in der Praxis von großer Bedeutung, da es in vielen Bereichen der Informatik, beispielsweise in der Soft- und Hardwareverifikation, in der künstlichen Intelligenz und in verschiedenen Schedulingalgorithmen, Anwendungen hat.
Aus diesem Grund ist es von besonderem Interesse, möglichst effiziente Algorithmen (sog. SAT-Solver) zu konstruieren, die das SAT-Problem mit akzeptabler Laufzeit lösen.

In diesem Proseminar betrachten wir SAT-Solver sowohl aus der theoretischen als auch aus der algorithmischen Sichtweise.

 

Für die Teilnahme an dem Proseminar sind ein solider Umgang mit mathematischer Notation sowie algorithmische Grundkenntnisse, wie sie in DAP2 vermittelt werden, notwendig.

Die Vortragsthemen basieren auf Teilen der Buches Handbook of Satisfiability von Biere et. al. . Es können auch weitere Quellen infrage kommen.