Binary Decision Diagram

Binary Decision Diagram (BDD) is a canonical data structure for representing Boolean functions as a directed acyclic graph. Introduced by Sheldon Akers in 1978 and refined by Randal Bryant in 1986 with the addition of ordering constraints and reduction rules, the BDD provides a compact representation that enables efficient manipulation of Boolean expressions. When variable ordering is fixed, a reduced ordered BDD (ROBDD) is canonical: equivalent Boolean functions have identical diagram structures, and isomorphism checking is linear time.

The structure of a BDD is a rooted directed graph where each non-terminal node represents a variable and has two outgoing edges — a 'then' edge (variable true) and an 'else' edge (variable false). Terminal nodes are labeled 0 or 1. By imposing a total order on variables and merging isomorphic subgraphs, the BDD achieves compression that is often exponential in the number of variables. The cost of this compression is sensitivity to variable ordering: a poor ordering can yield a diagram of exponential size, while a good ordering yields a compact representation. Finding the optimal ordering is NP-hard, but heuristics based on dynamic reordering (sifting) are effective in practice.

BDDs are the foundational data structure for symbolic model checking, where sets of states are represented as Boolean functions rather than enumerated explicitly. The model checker SMV and its successors use BDDs to verify systems with vast state spaces that would be intractable for explicit-state methods. BDDs are also used in logic synthesis, equivalence checking, and constraint satisfaction. However, their scalability is limited: for certain functions, such as multiplication, no variable ordering yields a polynomial-size BDD, and modern model checkers increasingly use SMT solvers and SAT-based methods instead.

The BDD was the data structure that made symbolic model checking practical, and in doing so it transformed hardware verification from an artisanal craft into an industrial process. Yet its limitations are instructive: BDDs work when the Boolean structure of a problem is shallow, and they fail when it is deep. The shift from BDDs to SAT and SMT solvers in modern verification is not merely a change in technology. It is a recognition that the problems we want to verify have grown beyond the representational capacity of diagrams. The BDD is a monument to the era when hardware was simpler. It deserves our respect, but not our dependence.