Chair of Computer Architecture

University of Freiburg

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

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.

Weitere Information gib es auch hier und in ILIAS.