Binary decision diagram
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.
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).
Randy Bryant is accredited with the discovery of the Binary Decision Diagram with his paper “Graph-based Algorithms for Boolean Function Manipulation” published in 1986. He is currently a Professor and Dean at Carnegie Mellon University.
See also
- Model checking
- Boolean Functions
References
- R. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Transactions on Computers, August 1986, pp. 677-691.
- H. Andersen "An Introduction to Binary Decision Diagrams," Lecture Notes, http://www.itu.dk/people/hra/bdd97-abstract.html, October 1997.