TAOCP 7.1.4 Exercise 16
Let the given BDD represent a Boolean function $f(x_1,\dots,x_n)$ in ordered and reduced form as defined in Section 7.
Section 7.1.4: Binary Decision Diagrams
Exercise 16. ▶ [22] [22] Design an algorithm that successively generates all vectors x1 . . . xn for which f(x1, . . . , xn) = 1, when a BDD for f is given.
Verified: no
Solve time: 3m14s
Solution
Let the given BDD represent a Boolean function $f(x_1,\dots,x_n)$ in ordered and reduced form as defined in Section 7.1.4. Each root-to-sink path corresponds to a consistent assignment of variables, and the evaluation rule assigns to each branch node $u$ the decision $x_{V(u)}=0$ for LO and $x_{V(u)}=1$ for HI.
The task is to generate exactly those assignments that reach $\top$.
A direct traversal of the BDD is insufficient unless variable gaps are handled, since orderedness allows nodes with labels skipping indices. When a path moves from a node labeled $i$ to a node labeled $j>i$, the variables $x_{i+1},\dots,x_{j-1}$ are not constrained by any decision in the BDD and must be explicitly assigned.
Define a recursive procedure $\mathrm{GEN}(u,k)$, where $u$ is a node of the BDD and $k$ is the largest index of a variable already assigned along the current partial assignment. The procedure implicitly maintains a partial vector $(x_1,\dots,x_k)$.
At a sink node, the procedure behaves according to the value of the sink. If $u=\bot$, no extension yields a solution, so the procedure terminates. If $u=\top$, then every completion of the current partial assignment to an $n$-tuple is a satisfying assignment, so the procedure outputs all vectors obtained by choosing arbitrarily each of $x_{k+1},\dots,x_n\in{0,1}$.
At a branch node $u$ with $V(u)=i$, the variables $x_{k+1},\dots,x_{i-1}$ are not fixed. Each assignment to these variables produces a distinct extension of the current partial vector, so the procedure first enumerates all $2^{i-k-1}$ binary strings $(x_{k+1},\dots,x_{i-1})$. For each such choice, it extends the current assignment and then branches on $x_i$.
If $x_i=0$, the procedure continues with $\mathrm{GEN}(\mathrm{LO}(u),i)$. If $x_i=1$, it continues with $\mathrm{GEN}(\mathrm{HI}(u),i)$.
The initial call is $\mathrm{GEN}(\mathrm{ROOT},0)$.
Correctness is established by induction on the structure of the BDD. At any call $\mathrm{GEN}(u,k)$, the partial assignment fixes exactly the variables $x_1,\dots,x_k$ along a unique consistent path prefix ending at $u$. Orderedness guarantees that no variable is ever revisited after being assigned, since all outgoing edges from $u$ go to nodes with strictly larger indices. Thus every extension of the current partial assignment corresponds to a unique extension of the path in the BDD.
If the procedure reaches $\top$, the path constraint is satisfied for all previously chosen variable values, so every completion of the remaining variables yields a full assignment satisfying $f=1$. Conversely, if an assignment satisfies $f=1$, the evaluation path induced by that assignment must reach $\top$, and the procedure necessarily follows the same sequence of LO and HI choices; the only additional freedom arises from variables skipped between successive node labels, which are explicitly enumerated. Hence every satisfying assignment is generated exactly once, and no non-satisfying assignment is produced.
This completes the proof. ∎