TAOCP 7.1.4 Exercise 261
Let $L \subseteq {0,1}^n$ be a language of fixed-length binary strings and let $f(x_1,\dots,x_n)$ be its characteristic Boolean function.
Section 7.1.4: Binary Decision Diagrams
Exercise 261. [HM21] [HM21] “The deterministic finite-state automaton with fewest states that ac- cepts any given regular language is unique.” What is the connection between this famous theorem of automata theory and the theory of binary decision diagrams?
Verified: yes
Solve time: 1m46s
Solution
Let $L \subseteq {0,1}^n$ be a language of fixed-length binary strings and let $f(x_1,\dots,x_n)$ be its characteristic Boolean function. Each word $w = (a_1,\dots,a_n)$ determines a unique evaluation path in the ordered binary decision diagram of $f$ by reading the bits in order $x_1,\dots,x_n$ and branching according to $a_j$ at level $j$.
For each prefix $u = (a_1,\dots,a_k)$ define the residual function
$$ f_u(x_{k+1},\dots,x_n) = f(a_1,\dots,a_k,x_{k+1},\dots,x_n). $$
Two prefixes $u$ and $v$ are equivalent when $f_u = f_v$ as Boolean functions. In the construction of a reduced ordered BDD, each node at level $k$ corresponds exactly to one such residual function, since a node represents the subproblem remaining after fixing the first $k$ variables. The LO and HI successors correspond to the residuals obtained by appending $0$ or $1$ to the prefix, so they implement the transition
$$ f_u \xrightarrow{0} f_{u0}, \quad f_u \xrightarrow{1} f_{u1}. $$
This structure is identical to a deterministic finite-state automaton whose states are residual languages (Myhill–Nerode equivalence classes). In that theory, each state represents a set of suffixes accepted from a given prefix, and two prefixes induce the same state exactly when they have the same residual language.
The classical theorem that the minimal deterministic finite automaton accepting a regular language is unique states that quotienting by the Myhill–Nerode equivalence yields a canonical automaton with the fewest states. In the BDD setting, reduction performs the same quotient operation: whenever two nodes represent the same residual Boolean function, they are merged into a single node, and any node with identical LO and HI successors is eliminated since it corresponds to a function independent of the next variable.
Thus, a reduced ordered BDD for $f$ is exactly the minimal acyclic deterministic automaton that computes $f$ by reading inputs in fixed order, where states are residual Boolean functions. The uniqueness of the minimal DFA corresponds to the uniqueness of the reduced OBDD representation: both arise because the equivalence relation “induces the same residual behavior on all suffixes” partitions prefixes into canonical classes, and both constructions identify one node or state per class.
In this correspondence, BDD nodes play the role of DFA states, variables $x_k$ play the role of input positions, and edges labeled $0$ and $1$ play the role of transition function. Reduction rules for BDDs coincide with DFA minimization under the Myhill–Nerode relation, so the canonical minimal DFA theorem is the structural reason that ordered reduced BDDs are unique representations of Boolean functions under a fixed variable ordering.
This completes the proof. ∎