Pro-Seminar Decision Diagrams Summer Semester 2022
Das Pro-Seminar wird auf Deutsch abgehandelt und hat als Thema Daten-Strukturen und Algorithmen für Entscheidungsdiagramme (Decision Diagrams).
Organisiation
-
Vorbesprechung: : Dienstag, 26.4., 17:30 h, in Raum 00-026 in Geb. 051
-
Vorträge: : jeweils dienstags, 12.7., 19.7., 26.7., 17:30 h, in Raum 00-026 in Geb. 051
Beschreibung
Entscheidungsdiagramme in Form von Binären Entscheidungsdiagrammen waren Ende des letzten Jahrhunderts sehr beliebt und trugen tatsächlich dazu bei, das Interesse an formaler Verifikation und formalen Methoden im Allgemeinen wiederzubeleben, da sie einer der Hauptgründe für den Erfolg des Model Checking waren, insbesondere im Zusammenhang mit der Hardware-Verifikation. Entscheidungsdiagramme neigen jedoch dazu, viel Speicherplatz zu verbrauchen, so dass ihre Verwendung teilweise problematisch ist. Zu Beginn dieses Jahrhunderts wurden sie größtenteils durch SAT-basierte Ansätze ersetzt, die robuster und effizienter zu sein versprechen, obwohl Entscheidungsdiagramme prinzipiell mächtiger sind, wenn es beispielsweise um Quantifizierung oder um das Zählen erfüllender Belegungen geht.
In diesem Proseminar greifen wir neue Entwicklungen zu Entscheidungsdiagrammen auf, die in einigen Nischenbereichen immer noch als die Methode der Wahl gelten. Außerdem hat Donald Knuth 2010 einen großen Abschnitt über Entscheidungsdiagramme in seiner Buchreihe The Art of Computer Programming geschrieben. In jüngster Zeit gibt es ein gewisses Interesse an der Verwendung von Entscheidungsdiagrammen für die Optimierung in der Operations Research Community. Wir sind auch daran interessiert, Entscheidungsdiagramme für SAT und verwandte Probleme wieder aufzugreifen.