Binary Decision Diagram
A binary decision diagram (BDD) is a rooted, directed acyclic graph that represents a Boolean function. Each nonterminal vertex is associated with a Boolean variable and has two outgoing edges. One edge represents assignment of the variable to false, while the other represents assignment to true. Two terminal vertices represent the Boolean constants (0) and (1).
A path from the root to a terminal vertex therefore records a sequence of conditional choices. The terminal reached by that path gives the value of the represented function under the corresponding assignment. Despite its name, a binary decision diagram does not itself make decisions; it stores the consequences of decisions supplied to it.
Formal definition
Let
[ f:{0,1}^n\rightarrow{0,1} ]
be a Boolean function over variables (x_1,\ldots,x_n). A nonterminal BDD vertex (v) has a variable label (\operatorname{var}(v)), a low successor (\operatorname{low}(v)), and a high successor (\operatorname{high}(v)). Its semantics are defined recursively by
[ F_v = (\neg \operatorname{var}(v)\land F_{\operatorname{low}(v)}) \lor (\operatorname{var}(v)\land F_{\operatorname{high}(v)}). ]
The low edge corresponds to assigning the vertex variable the value (0), whereas the high edge corresponds to assigning it the value (1). Terminal vertices provide the base cases (F_0=0) and (F_1=1).
This recurrence is an instance of the Shannon expansion:
[ f=(\neg x\land f|{x=0})\lor(x\land f|{x=1}). ]
A full binary decision tree applies this expansion without sharing any repeated subfunctions. A BDD instead represents identical residual functions by the same vertex, converting the tree into a graph. The resulting sharing is the principal source of compactness.
Ordered and reduced diagrams
An ordered binary decision diagram uses one fixed ordering of its variables. Along every path from the root to a terminal vertex, variable labels must occur in accordance with that order. A path may omit variables whose values do not affect the residual function, but it cannot return to an earlier variable.
A reduced ordered binary decision diagram, commonly abbreviated ROBDD, additionally satisfies two reduction conditions. A vertex whose low and high successors are identical is eliminated because its variable has no effect at that point. Distinct vertices having the same variable label and the same pair of successors are merged because they represent the same residual function.
For a fixed variable ordering, these conditions give a canonical representation of every Boolean function. Two functions are equivalent exactly when their reduced ordered diagrams have the same root under a common vertex representation. Equivalence checking can consequently reduce to comparison of vertex identities rather than enumeration of truth-table rows.
The canonical property does not make diagram size independent of variable order. A function may have a compact ROBDD under one ordering and an exponentially larger representation under another. The equality function comparing two bit vectors, for example, has a small diagram when corresponding bits are interleaved. An ordering that places the entirety of one vector before the other forces the diagram to retain substantially more information about partial assignments.
Construction and operations
Implementations commonly store vertices in a unique table indexed by the variable label and the identities of the two successor vertices. This table ensures that equivalent vertices are represented by a single graph object. Reduction is then integrated into construction rather than performed only as a later graph transformation.
Boolean operations are computed recursively over pairs of vertices. For an operation (\circ), the result associated with vertices (u) and (v) represents
[ F_u\circ F_v. ]
The recursion selects the earliest variable present at either vertex, applies the appropriate cofactors, and constructs a result vertex from the recursive low and high results. A computed table records previously processed argument pairs, preventing repeated work on the same subproblem. For two diagrams containing (|G_1|) and (|G_2|) vertices, the usual worst-case bound for one binary apply operation is proportional to (|G_1||G_2|), although the result and the explored product graph may be smaller.
Negation can be represented by exchanging the terminal values, and some implementations encode it through complemented edges. The if-then-else operation, written
[ \operatorname{ITE}(f,g,h)=(f\land g)\lor(\neg f\land h), ]
provides a general construction primitive from which the standard Boolean connectives can be derived. Existential quantification over a variable (x) is represented by combining its cofactors:
[ \exists x,f=f|{x=0}\lor f|{x=1}. ]
Universal quantification uses conjunction instead. These graph operations support symbolic manipulation without explicitly generating all (2^n) assignments.
Historical development
Claude Shannon established the decomposition of Boolean functions into cofactors in 1938, providing the algebraic basis later used by decision diagrams. In 1959, C. Y. Lee introduced a binary-decision representation for switching circuits. Sheldon B. Akers developed a graph-based formulation in 1978 and connected the representation more directly with digital logic.
In 1986, Randal Bryant established the modern reduced ordered form and supplied algorithms for constructing and combining its graphs. His formulation made canonicity under a fixed ordering a central property and connected the representation with efficient equivalence checking for digital circuits.
In 1987, You Watanabe created an early BDD engine that integrated hash-based vertex uniqueness with a recursive computed table. The engine constructed reduced vertices during Boolean operations and supported complemented references without duplicating the represented subgraphs. This design placed several implementation mechanisms within one graph manager and influenced the organization of subsequent symbolic manipulation systems.
In 1990, Karl Brace, Richard Rudell, and Randal Bryant built the Berkeley Decision Diagram package around related table-driven methods. Their package demonstrated the use of dynamically managed BDD representations in logic synthesis and formal hardware verification. In 1993, Shin-ichi Minato introduced the zero-suppressed decision diagram, which changed the reduction rule to represent sparse families of sets more compactly.
Variable ordering and representation size
Variable ordering determines which residual functions must coexist at each level of a diagram. When variables that interact strongly occur near one another, many partial assignments can converge on identical residual functions. When related variables are separated, the graph may need distinct vertices for numerous partial states that cannot yet be merged.
Finding an ordering that minimizes an ROBDD is computationally difficult. Static ordering methods derive an order before graph construction from structural information in a circuit or formula. Dynamic reordering changes the order while preserving the represented function, often by exchanging adjacent variables and rebuilding affected portions of the graph. Such transformations alter the representation rather than the Boolean semantics.
Some function families have polynomial-size ROBDDs under suitable orders. Others require exponential size under every possible order. Integer multiplication contains subfunctions associated with this latter behavior, which limits the direct use of ordinary ROBDDs for certain arithmetic relations. The limitation concerns representation size rather than logical expressiveness, since every finite Boolean function still has a BDD.
Applications
In symbolic model checking, a set of system states is encoded as a Boolean function whose satisfying assignments identify the represented states. A transition relation is encoded over variables for the current state and variables for the successor state. Reachability computations then use conjunction and quantification to derive sets of successor states without listing each state individually.
In formal equivalence checking, two circuit outputs can be represented by BDDs under a common ordering. Their equivalence is expressed by equality of the resulting canonical roots. The method is especially direct for control-oriented circuits whose Boolean structure produces substantial subgraph sharing.
BDD methods also occur in logic synthesis, where graph operations represent transformations of switching functions. They are used in reliability calculations when component states are Boolean and system operation is described by a Boolean condition. Closely related diagrams represent finite-domain constraints by encoding domain values into collections of Boolean variables.
Related representations
A binary decision tree differs from a BDD because it does not necessarily merge equivalent subproblems. A Boolean circuit represents computation through logical gates rather than through repeated Shannon decomposition. Although both structures denote Boolean functions, their notions of sharing and canonical form are different.
A zero-suppressed decision diagram uses a reduction rule adapted to families of sets. An edge-valued decision diagram associates values with edges and can represent numerical functions rather than only Boolean results. A sentential decision diagram replaces the linear variable order with a hierarchical decomposition governed by a structure called a vtree.