How to effectively implement binary decision diagrams (BDD)?

Question

The story of binary adoption schemes can be found here on BDD on wikipedia .

The easiest way is to build a BDT (binary decision tree) and then reduce it due to two rules:
- Merge any isomorphic subgraphs.
- Exclude any node in which two children are isomorphic.
But there is one serious problem: BDT can be really huge compared to BDD. Is there a way to build a BDD without first creating a BDT?

Answer 1

Use the Mk (make node) and Build (build BDD) algorithms from Andersen , pp. 16-17. I have not played with BDD after a while, but I believe that H or T should be a hash table. Use hash tables to keep them safe.

Answer 2

The way to build a BDD is a parse tree for an expression representing the logical function that you are trying to build.

Ie if you want BDD for (A + B). (C + D), first you parse (A + B). (C + D) to tree:

  .
   / \
  +++
 / \ / \
 Abcd

then create the BDD recursively - you need methods that can form the AND and OR of the two BDDS, and the base register (a single BDD variable).

This works just as well for logic (lookup as DAG parsing instead of tree).

These BDD notes explain how to implement AND and OR, as well as the hash tables necessary for efficient operation: http://bit.ly/cuClGe

Answer 3

Try reading Knut if you want to do it right.

https://www-cs-faculty.stanford.edu/~knuth/fasc1b.ps.gz

To be more precise, the "R" algorithm, the initial page 14 of this chapter of the book, is an accurate and complete answer to FP;

In general, Knut’s book chapters are very good reference material, so he happens to have written one on (RO) BDD, which is extremely lucky for anyone who is seriously trying to implement BDD.