Binary decision diagrams

A binary decision diagram (BDD) represents a Boolean function as a graph of decisions. Each node tests one variable and has a 0-edge and a 1-edge; paths end in a 0 or 1 terminal. With a fixed variable order and two reduction rules — merge identical sub-graphs and remove nodes whose two edges go to the same place — the result is a reduced ordered BDD, which is canonical: two functions are equivalent exactly when their BDDs are the same graph.

Variable order matters — a lot

The size of a BDD depends heavily on the variable order. For a comparator x == y on n-bit vectors, interleaving the bits (x₀, y₀, x₁, y₁, …) gives a BDD that grows linearly with n; putting all x bits first and then all y bits makes it grow exponentially. Finding a good order is itself hard, and some functions — notably multipliers — have no small BDD under any order.

Model checking with BDDs

BDDs can represent sets of states (as the characteristic function "is this state in the set?") and the transition relation. Computing successors of a whole set then becomes a few BDD operations, called image computation. Repeating it until the fixed point — the reachable-set iteration from lesson 2.2 — gives a complete, unbounded proof. This symbolic model checking was the breakthrough of the early 1990s, and BDD engines still appear in tool portfolios today, mostly for small, deep control logic.