A Boolean function has exactly one canonical shape. Bryant's reduced ordered BDD is that shape: fix the variable order, share every repeated subgraph, drop every node that decides nothing — and two functions are equal precisely when their diagrams are the same graph. Rendered, not quoted.
source R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Trans. Computers C-35(8):677–691, 1986 · doi:10.1109/TC.1986.1676819
A BDD node is a triple (var, lo, hi): test var, follow lo when it is 0 and hi when it is 1. Two terminals, 0 and 1. Variables obey a fixed global order x0 < x1 < x2.
Two reduction rules make it an ROBDD:
① Share — never store two isomorphic subgraphs; a unique table returns the existing node.
② Remove — a node whose lo and hi are identical decides nothing; bypass it.
Every node is built by Shannon expansion:
f = (¬x · f|x=0) + (x · f|x=1).
An ROBDD is a normal form for Boolean functions — the compressed, comparable shadow of the-boolean-circuit. The same reduction that shrinks a truth table to a shared graph is the data structure that lets the-model-checking represent whole state sets symbolically and test equivalence in constant time.
Neighbour → the-model-checking: reachable-set fixpoints become graph operations on ROBDDs.
Live re-check of canonicity. It builds h = (x0·x1)+(¬x0·x1) and x1 — the same function two ways — and confirms their ROBDDs are the same node id. If the reduction is tampered, the two diagrams diverge and this badge flips red.
redundant-node reduction: ON
Input space: the full truth table of majority-of-3, maj₃ = 1 iff (x0+x1+x2) ≥ 2 — all 2³ assignments.
| x0 | x1 | x2 | maj |
|---|
Real ROBDD manager: Shannon build + unique-table sharing + redundant-node removal, over a fixed order. The diagram below is the reduced graph of maj₃.
selfcheck idle
…
Proven exhaustively: correct on all 2³ inputs, canonical (equal ⇔ identical), reduction rules hold, Shannon reconstructs.
Instrument state: … · nodes(maj₃) = –
WALL Canonicity is relative to the variable order. The order is chosen, not given.
BDD size is exponentially sensitive to it: some functions are tiny under one order and exponential under another. The integer-multiplication middle bit has no polynomial-size ROBDD in any order (Bryant, 1991).
amber "a good order always exists and is findable" — assumed, not proven; order-finding is itself NP-hard.
"An ROBDD makes every Boolean function small."
✓ Only functions with bounded subfunction count. Multipliers and hidden-weighted-bit stay exponential.
"Any variable ordering gives the same size."
✓ Size can jump from linear to exponential across orders; canonicity holds per fixed order only.
"Skipping the redundant-node rule is a harmless optimisation."
✓ It destroys canonicity — equal functions get different diagrams (see window 6).
Disclosed planted void: skip reduction rule ② (keep a node whose two children are identical). Function values are unchanged, but two equal functions now build different diagrams — canonicity is lost, and the Witness (7) catches it live.