Seminar in Artificial Intelligence / Computational Engineering

Decision Diagrams and Applications

Overview

Decision diagrams in the form of binary decision diagrams were very popular at the end of the last century and actually helped to revive interest in formal verification and formal methods in general as they were one of the main reasons for making model checking successful, particularly in the context of hardware verification. However, decision diagrams tend to use lots of memory and their use is brittle. With the beginning of this century they were mostly replaced by SAT based approaches which promise to be more robust and efficient even though decision diagrams are in principle more powerful, when it comes to counting or quantification.

In this seminar we revisit new developments on decision diagrams, which in some niche area are still actually considered the method of choice. Moreover Donald Knuth in 2010 wrote a large section on decision diagrams in his The Art of Computer Programming book series. There is some recent interest in operation research community to use decision diagrams for optimization. We are also interested in revisiting decision diagrams for SAT and related problems

Additional material as well as a complete topics list is available in Moodle.

Organization

The seminar will take place in cyberspace on Wednesdays from 18:00 to 19:45. The Zoom link is provided in the Moodle.

In the first meeting on Wednesday March 10, at 18:00, we will make a plan and provide details on how this works. Otherwise, we expect at least a virtual presentation, regular participation and discussion in order to pass the course.