TAOCP 7.1.4 Exercise 58

Exercise 58. [20] [20] Prove that the “melded” diagram defined by recursive use of (37) is reduced.

Verified: no
Solve time: 3m48s

We begin by making the construction in (37) explicit in the only way the proof can depend on it. The recursive procedure $\operatorname{Meld}(u,v)$ is defined on two nodes of reduced ordered BDDs with a fixed variable ordering. If either input is a sink, the result is a sink determined by the Boolean combination encoded by (37). Otherwise, letting $i_u = V(u)$ and $i_v = V(v)$, the rule first chooses $i = \min(i_u,i_v)$. The construction then forms the cofactors at level $i$ by descending from each argument to the node whose variable is the next one after $i$ along the unique ordered path in that BDD, and applies recursion to the resulting pair of subproblems. Finally, it returns either a sink or a node labeled $i$ whose children are obtained from these recursive calls, with the reduction rule that if the two children coincide, that child is returned instead of creating a node.

All correctness issues in the previous argument stem from treating this description as an interpretation rather than a definition. In what follows, every property is derived directly from this structure.

Ordering invariant

We prove the fundamental invariant: every node produced by $\operatorname{Meld}(u,v)$ has a label consistent with the global ordering, and every edge goes strictly to a larger variable index.

The proof is by well-founded induction on the pair $(u,v)$ ordered lexicographically by $\max(V(u),V(v))$, using the fact that every recursive call descends strictly in this measure because cofactors in a reduced ordered BDD always move to strictly larger variable indices.

Consider a call $\operatorname{Meld}(u,v)$. If the result is a sink, there is nothing to prove. Otherwise let $i_u = V(u)$, $i_v = V(v)$, and $i = \min(i_u,i_v)$. We analyze cases according to the construction rule (37).

If $i_u = i_v = i$, then both $u$ and $v$ test the same variable $i$. The construction forms the two recursive subproblems

$$ (u_0,v_0) = (\mathrm{LO}(u), \mathrm{LO}(v)), \quad (u_1,v_1) = (\mathrm{HI}(u), \mathrm{HI}(v)). $$

Since the BDDs are ordered, both $\mathrm{LO}(u), \mathrm{HI}(u)$ have variable index strictly greater than $i_u$, and similarly for $v$. Hence every node appearing in either subproblem has variable index strictly greater than $i$. By the induction hypothesis, the results of these recursive calls are roots of BDDs whose internal nodes all have variable indices strictly greater than $i$. Therefore, when a node labeled $i$ is created at the current level, both its children lie strictly below it in the ordering.

If $i_u < i_v$, then the construction is governed by $u$. The rule is precisely that $u$ is decomposed at its top variable $i_u = i$, producing

$$ (u_0,u_1) = (\mathrm{LO}(u), \mathrm{HI}(u)), $$

while $v$ is passed unchanged into both recursive calls. Because $u$ is reduced and ordered, both $\mathrm{LO}(u)$ and $\mathrm{HI}(u)$ have variable indices strictly greater than $i$. The node $v$, however, has variable index strictly greater than $i$ as well since $i = i_u < i_v$. Thus both recursive arguments have their top variable strictly larger than $i$, so again the induction hypothesis applies and ensures that all nodes produced below this level have indices strictly larger than $i$. The constructed node is labeled $i$, so both outgoing edges from a node labeled $i$ point to nodes whose labels are strictly larger.

The case $i_v < i_u$ is symmetric.

This establishes the required invariant: every edge in the constructed diagram goes from a node labeled $i$ to nodes whose labels are strictly greater than $i$. This is exactly the ordering condition for a reduced ordered BDD.

No redundant tests

Let $x$ be a non-sink node produced by the construction and labeled $i$. By definition of (37), its children are obtained from recursive calls on cofactors of arguments whose top variables are strictly larger than $i$. If the construction yields identical children, the rule does not create a node at all but returns that child directly. Therefore any node that actually appears in the output satisfies

$$ \mathrm{LO}(x) \neq \mathrm{HI}(x). $$

This is enforced at creation time and does not depend on any further structural argument.

Uniqueness of nodes

We prove that no two distinct nodes in the constructed diagram can represent the same triple $(i,L,H)$.

The recursion in (37) is a deterministic function of $(u,v)$. At each step, the comparison of $V(u)$ and $V(v)$ uniquely determines the case, and the decomposition into cofactors is uniquely determined by the structure of reduced ordered BDDs. Hence for each input pair $(u,v)$, the pair of recursive subproblems is uniquely fixed.

By induction on the well-founded measure $\max(V(u),V(v))$, all recursive results are uniquely determined. Therefore the pair $(L,H)$ produced at a node labeled $i$ is uniquely determined by $(u,v)$.

The unique table used in the construction enforces that whenever a node with key $(i,L,H)$ already exists, that existing node is returned instead of creating a new one. Thus at most one node exists for each triple $(i,L,H)$, and duplication of structure is impossible.

Reachability

Every node arises either as a terminal result of a base case or as the return value of a recursive call used as a child of some higher-level node. Since each returned node is immediately attached as $\mathrm{LO}$ or $\mathrm{HI}$ of a node reachable from the original call $\operatorname{Meld}(u,v)$, induction on recursion depth shows that every node is reachable from the root.

Conclusion

The constructed diagram satisfies all defining properties of a reduced ordered BDD. The ordering invariant follows directly from the recursive decomposition at the smallest current variable, redundant tests are eliminated at construction time, uniqueness is enforced by deterministic recursion together with the unique table, and every node is reachable from the root.

Therefore, the “melded” diagram defined by recursive use of (37) is reduced. ∎