Binary decision diagram

A binary decision diagram (BDD) is a data structure that is used to represent a Boolean function. The Boolean function is represented in a BDD as a rooted, directed, acyclic graph where each non-terminating vertex is labeled by a variable and has two directed edges, one dotted and one solid, connecting to child nodes. The dotted line represents a variable’s assignment to zero and the solid line represents an assignment to one. A 1 or 0 labels all terminal vertexes.

BDD's are essentially a specific form of Patricia tries (also called Crit bit trees) where the value associated with each key is restricted to be a boolean value.

For example, take Figure 1 below. There are three variables x1, x2 and x3 and there is a truth table to represent the function f(x1, x2, x3). By following a path down the graph to a terminal, you can determine a value for the function. Therefore, to find (x1=0, x2=1,x3=1), begin at x1, traverse down the dotted line to x2 (since x1 has an assignment to 0), then down two solid lines (since x2 and x3 each have an assignment to one). This leads to the terminal 1, which is the value of f(x1=0, x2=1, x3=1).

History

The basic idea from which the data structure was created is the Shannon extension. A switching function is split into two sub-functions (cofactors) by assigning one variable (cf. if-then-else normal form). If such a sub-function is considered as sub-tree, it can be represented by a binary decision tree. Binary decision diagrams (BDD) were introduced by Lee (Lee 1959), and further studied and made known by Akers (Akers 1978). Two years before Lee the same idea was introduced in former Soviet Union, in Tallinn University of Technology (Ubar 1976). For a long time, this representation was called Alternative Graphs, until it was once renamed.

The full potential for efficient algorithms based on the data structure was investigated by Bryant: his key extensions were to use a fixed variable ordering (for canonical representation) and shared sub-graphs (for compression). Applying these two concepts results in an efficient data structure and algorithms for the representation of sets and relations (Bryant 1986, Bryant 1992). By extending the sharing to several BDDs, i.e. one sub-graph is used by several BDDs, the data structure Shared Reduced Ordered Binary Decision Diagram is defined (Brace, Rudell, Bryant 1990). The notion BDD is now generally used to refer to that particular data structure.

On a more abstract level, BDDs can be considered as a compressed representation of sets or relations. In difference to other compressions, the actual operations are performed on that compressed representation, without decompression.

See also

• Model checking
• Crit bit tree
• Patricia trie

References

• C. Y. Lee. "Representation of Switching Circuits by Binary-Decision Programs". Bell Systems Technical Journal, 38:985–999, 1959.
• Sheldon B. Akers. "Binary Decision Diagrams". IEEE Transactions on Computers, C-27(6):509–516, Juni 1978.
• Randal E. Bryant. "Graph-Based Algorithms for Boolean Function Manipulation (http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.ps)". IEEE Transactions on Computers, C-35(8):677–691, 1986.
• R. E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams" (http://www.cs.cmu.edu/~bryant/pubdir/acmcs92.ps), ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293-318.
• Karl S. Brace, Richard L. Rudell and Randal E. Bryant. "Efficient Implementation of a BDD Package". In Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC 1990), pages 40–45. IEEE Computer Society Press, 1990.
• H. Andersen "An Introduction to Binary Decision Diagrams," (http://www.itu.dk/people/hra/bdd97.ps) Lecture Notes, http://www.itu.dk/people/hra/bdd97-abstract.html, October 1997.
• Ch. Meinel, T. Theobald, "Algorithms and Data Structures in VLSI-Desing: OBDD - Foundations and Applications" (http://www.informatik.uni-trier.de/~meinel/books/obddbook.html), Springer-Verlag, Berlin, Heidelberg, New York, 1998.
• R. Ubar, "Test Generation for Digital Circuits Using Alternative Graphs (in Russian)", in Proc. Tallinn Technical University, 1976, No.409, Tallinn Technical University, Tallinn, Estonia, pp.75-81.

de:Binary Decision Diagram