Binary Decision Diagrams (BDDs)

Notes by Gene Cooperman, © 2009 (may be freely copied as long as this copyright notice remains)

A good starting point for learning about BDDs is the Wikipedia article. We are concerned only with Reduced Ordered Binary Decision Diagrams (ROBDD). Often, one refers to a ROBDD as simply a BDD for short, but there are also other types of BDDs. For us, BDD will always mean ROBDD.

BDDs are sometimes known as a type of symbolic model checking (in the sense of symbolic logic, which most students have already seen).

Although the main discussion will refer to the Knuth presentation of BDDs, there is an expanded introduction to BDDs with more examples by Andrei Voronkov (see below).

One look at BDDs is given in Knuth's "Pre-Fascicle 1b" for his famous The Art of Computer Programming (.ps version). There is also a local pdf version (access via CCIS account, only). The first few pages introduce BDDs.

Figure 25 shows a large example BDD computation (the and of three BDDs, and the result). Expression (54) on page 23 (which is the 31st page of the pdf) describes the algorithm discussed in class for conjunction of two BDDs.

Page 24 describes a memoization technique for optimizing the algorithm of Expression (54). Memoization here is exactly the same memorization that we encountered under dynamic programming. The same page then points out that this memoization can be done by hashing. We can memoize 'f∧g=r' by hashing using the key 'f,∧,g' (or the pair '(f,g)') and the value 'r'. At the hash index (or hash address), we store both the hash key ''f,∧,g' and the hash value 'r', so that we can easily detect hash collisions. This is called a memo cache.

Separately, one needs a unique table, a hash table to record each node of the BDD. Then, if two branches of the BDD are isomorphic (equivalent), then we can recognize this by looking up the root node of each branch in the unique table. A node of the unique table, x, has the form x = (v,p,q) for variable number v and left child node p and right child node q. For example, a node might be represented as: (4,0x1a30,0x2fbc) where it refers to Boolean variable x4 (at the fourth level in the DAG) with a left child node already stored at address 0x1a30 in the unique table, and a right child node already stored at address 0x2fbc in the unique table, The special nodes 'true' and 'false' at the bottom of the DAG are given special addresses, such as 0x1 and 0x0.

Expression (55) at the bottom of page 24 provides an expanded algorithm that describes how to use hash tables and memoization for lookup.
Notice that the algorithm is just a variation of a dynamic programming algorithm using memoization, as described in the previous web page. The top of page 25 then describes Algorithm U, the hash table lookup used in the expanded algorithm.

(Note that the author also refers to an Algorithm S based on breadth-first search. The more common algorithm is the Depth-First Search highlighted by Expression (55) and Algorithm U.)

Another introduction is given in this paper referred to

by the Wikipedia article. (The first eight pages give the main idea.)

And the following introduction to BDDs is also worth looking at:

Software Packages for Computing with BDDs (from the Wikipedia article)

Other papers on BDDs

While there is a paper by Akers in 1978 (and one in Russian by Ubar in 1976), the subject really got started with some papers by Bryant in 1986 and 1990. Some noteworthy links from the Wikipedia page are: