In popular usage, the term BDD almost always refers to Reduced Ordered Binary Decision Diagram (ROBDD in the literature, used when the ordering and reduction aspects need to be emphasized). The advantage of an ROBDD is that it is canonical (unique) for a particular functionality. This property makes it useful in functional equivalence checking and other operations like functional technology mapping.
A path from the root node to the 1-terminal represents a (possibly partial) variable assignment for which the represented Boolean function is true. As the path descends to a low child (high child) from a node, then that node's variable is assigned to 0 (1).
BDDs are extensively used in CAD software to synthesize circuits (logic synthesis) and in formal verification. There are several lesser known applications of BDD, including Fault tree analysis, Bayesian Reasoning and Product Configuration.
Every arbitrary BDD (even if it is not reduced or ordered) can be directly implemented by replacing each node with a 2 to 1 multiplexer; each multiplexer can be directly implemented by a 4-LUT in a FPGA. Unfortunately, it is not so simple to convert from an arbitrary network of logic gates to a BDD (unlike the and-inverter graph).
The binary decision tree of the left figure can be transformed into a binary decision diagram by maximally reducing it according to the two reduction rules. The resulting BDD is shown in the right figure.
The full potential for efficient algorithms based on the data structure was investigated by Randal Bryant at Carnegie Mellon University: 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). 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. The notion of a 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. Unlike other compressed representations, the actual operations are performed directly on that compressed representation, i.e. without decompression.
It is of crucial importance to care about variable ordering when applying this data structure in practice. The problem of finding the best variable ordering is NP-hard. For any constant c>1 it is even NP-hard to compute a variable ordering resulting in an OBDD with a size that is at most c times larger than an optimal one. However there exist efficient heuristics to tackle the problem.
There are functions for which the graph size is always exponential — independent of variable ordering. This holds e. g. for the multiplication function (an indication as to the apparent complexity of factorization ). Researchers have of late suggested refinements on the BDD data structure giving way to a number of related graphs: BMD (Binary Moment Diagrams), ZDD (Zero Suppressed Decision Diagram), FDD (Free Binary Decision Diagrams), PDD (Parity decision Diagrams), etc.
This is a crude way to build a BDD in C like language. Declare the data structure as follows and then proceed accordingly.
/* The basic data structure */
struct vertex *hi, *lo;
/* The interface to the Unique Table */
struct vertex *old_or_new(char *φ, struct vertex *hi, *lo)
if(“a vertex v = (φ, hi, lo) exists”)
v <- “new vertex pointing at (φ, hi, lo);
Data Structure for Building the ROBDD
struct vertex *robdd_build(struct expr , int i)
struct vertex *hi, *lo;
struct char *φ;
else if (equal(f, '1'))
φ ← п(i);
hi ← robdd_build(, i+1);
lo ← robdd_build(, i+1);
if(lo == hi)
return old_or_new(φ, hi, lo);}
US Patent Issued to International Business Machines on March 15 for "Enhanced Verification Through Binary Decision Diagram-Based Target Decomposition Using State Analysis Extraction" (Texas, Minnesota Inventors)
Mar 17, 2011; ALEXANDRIA, Va., March 17 -- United States Patent no. 7,908,575, issued on March 15, was assigned to International Business...
US Patent Issued to International Business Machines on April 5 for "Enhanced Verification Through Binary Decision Diagram-Based Target Decomposition" (Texas, Minnesota Inventors)
Apr 12, 2011; ALEXANDRIA, Va., April 12 -- United States Patent no. 7,921,394, issued on April 5, was assigned to International Business...
Logic circuit equivalence checking using Haar Spectral coefficients and partial BDDs.(binary decision diagram)
Jan 01, 2002; A probabilistic equivalence checking method is developed based on the use of partial Haar Spectral Diagrams (HSDs). Partial HSDs...