TAOCP 7.1.4 Exercise 11
Algorithm C in Section 7.
Section 7.1.4: Binary Decision Diagrams
Exercise 11. [20] [20] Does Algorithm C give the correct answer if it is applied to a binary decision diagram that is (a) ordered but not reduced? (b) reduced but not ordered?
Verified: no
Solve time: 4m26s
Solution
Algorithm C in Section 7.1.4 operates on a BDD representation that relies on two structural properties: ordering of variables along every path, and reduction of nodes so that no two distinct nodes represent the same triple $(V,LO,HI)$ and no node has $LO = HI$. Correctness of Algorithm C depends on the extent to which these properties guarantee that the structure is a canonical directed acyclic graph for the represented Boolean function.
Let $f$ be the Boolean function computed by a BDD $D$, and let Algorithm C compute an output value by recursively or iteratively following $LO$ and $HI$ pointers according to the variable assignments along a path from the root to a sink.
(a) Ordered but not reduced
Assume the BDD is ordered but not reduced. The ordering condition guarantees that along any path from the root, variables appear in strictly increasing index order, so no variable is tested more than once and the evaluation of a given input vector $x = (x_1,\dots,x_n)$ is well defined as a single root-to-sink traversal determined by the values of $x_j$.
Let $D$ be such a structure and let $D'$ be the reduced BDD obtained by merging any pair of nodes with identical triples $(V,LO,HI)$ and deleting nodes with $LO = HI$, as in Section 7.1.4. The evaluation semantics of a node depend only on its label $V$ and its two successors, so every node in $D$ computes exactly the same Boolean function as its image in $D'$ under this quotienting process. The ordering ensures that no cyclic dependence is introduced during this identification, since successor pointers always go to strictly larger variable indices.
Every root-to-sink path in $D$ corresponds to a path in $D'$ with identical variable tests and identical outcomes at sinks. Conversely, each path in $D'$ can be lifted to at least one path in $D$. Thus every input assignment yields the same sink value in $D$ and $D'$, since evaluation depends only on the unique path determined by ordering.
Algorithm C, which evaluates the BDD by following edges according to the input bits, depends only on path semantics and not on uniqueness of node representation. The absence of reduction does not introduce ambiguity in traversal or change any sink reached by a given assignment. Therefore Algorithm C returns the correct value of $f$.
(b) Reduced but not ordered
Assume the BDD is reduced but not ordered. Reduction ensures uniqueness of nodes and elimination of $LO = HI$ redundancies, but it does not constrain the order in which variables appear along paths.
If ordering fails, there exists at least one directed path in the BDD containing a node labeled $V(i)$ followed by a node labeled $V(j)$ with $j \le i$. This permits re-examination of a variable or out-of-order testing of variables along a path. Consequently, the same variable assignment $x$ does not induce a well-defined decision process based solely on the structure, since different paths may correspond to inconsistent sequences of variable tests.
To see the failure of correctness, consider that Algorithm C assumes the invariant that when a node labeled $x_k$ is visited, all variables $x_1,\dots,x_{k-1}$ have already been resolved and will not reappear. This invariant guarantees that the subfunction at a node depends only on untested variables. Without ordering, a node may depend on a variable already used earlier along the path, so the subfunction interpretation of nodes as functions on remaining variables breaks down.
Although reduction prevents duplication of identical local structures, it does not prevent semantic inconsistency caused by repeated or backward variable tests. Two different paths corresponding to the same input assignment can reach different nodes depending on the order in which variables are encountered, since the DAG structure no longer enforces a consistent decomposition of the truth table by variable index.
Therefore Algorithm C may follow a structurally valid path but one that does not correspond to the intended functional decomposition, and the resulting sink may disagree with the Boolean function intended by the unreduced semantics.
Thus Algorithm C is not guaranteed to be correct when the BDD is reduced but not ordered.
This completes the proof. ∎