TAOCP 7.1.4 Exercise 149
The central issue is that the original argument tries to maintain a global “ancestry” of nodes through repeated reductions.
Section 7.1.4: Binary Decision Diagrams
Exercise 149. [M20] [M20] (Bollig, Löbbing, and Wegener.) Show that, in addition to Theorem J−, we also have B(f π 1 , . . . , f π m) ≤(2k −2)b0 + B(f1, . . . , fm) after a jump-down operation of k −1 levels, when (b0, . . . , bn) is the profile of {f1, . . . , fm}.
Verified: no
Solve time: 4m
The central issue is that the original argument tries to maintain a global “ancestry” of nodes through repeated reductions. This fails in reduced OBDDs because sharing and merging destroy any stable per-node lineage. The fix is to eliminate global ancestry entirely and instead work in a setting where sharing is removed before the argument begins, so that reductions cannot interfere with accounting.
Corrected Solution
Let $G^{(0)}$ be the reduced ordered BDD for ${f_1,\dots,f_m}$, with profile $(b_0,\dots,b_n)$, and let $B(f_1,\dots,f_m)$ denote its number of nodes. We perform a jump-down of a variable across $k-1$ levels, producing $G^{(k-1)}$.
The goal is to prove
$$ B(f^\pi_1,\dots,f^\pi_m);\le;B(f_1,\dots,f_m) + (2k-2)b_0. $$
1. Eliminating the reduction obstruction
The failure in the original solution comes from attempting to track nodes through reductions. To avoid this, we pass to an equivalent unshared forest representation.
Replace each node in the top level of $G^{(0)}$ by the root of its own copy of the entire sub-BDD beneath it. Whenever two nodes share a subgraph, duplicate that subgraph so that the copies become disjoint.
Call the resulting structure $F^{(0)}$. Then:
- $F^{(0)}$ is a forest of $b_0$ rooted OBDDs.
- Each tree corresponds to one top-level node of $G^{(0)}$.
- No sharing exists between different trees.
Let $B(F^{(0)})$ denote the total number of nodes in this forest. Since $F^{(0)}$ is obtained by duplicating shared structure,
$$ B(f_1,\dots,f_m) \le B(F^{(0)}). $$
Thus, proving an upper bound for $F^{(0)}$ suffices.
2. Key structural fact (locality in a single tree)
Consider one tree $T$ in the forest. It represents a single subfunction associated with one original top-level node.
A jump-down of a variable across one level acts locally on the Shannon expansion at that level:
- Each occurrence of the swapped variable introduces at most a binary branching.
- Each such replacement introduces at most two new decision nodes before reduction.
Crucially, within a single tree there is no sharing with other trees, so no cross-tree merging or interference occurs.
3. Single-step bound inside one tree
Fix a tree $T$. Consider one step of the jump-down process.
Each time the distinguished variable is moved past one adjacent level, every node in that tree may undergo a local Shannon expansion rewrite. In the worst case:
- each affected structure creates at most 2 new nodes per occurrence of the top-level root structure of that tree,
- no other mechanism introduces new nodes beyond these local expansions,
- and reductions within the tree can only merge nodes, never increase the count.
Hence for each tree $T$,
$$ B_T^{(t+1)} \le B_T^{(t)} + 2. $$
This is now well-defined because there is no sharing: every node belongs to exactly one tree.
4. Extending over $k-1$ levels
Iterating the inequality for a fixed tree gives
$$ B_T^{(k-1)} \le B_T^{(0)} + 2(k-1). $$
Now sum over all $b_0$ trees:
$$ B(F^{(k-1)}) \le B(F^{(0)}) + (2k-2)b_0. $$
5. Returning to the reduced OBDD
The final step is to relate the forest back to the reduced diagram.
At every stage, reduction can only merge isomorphic subgraphs, hence can only decrease the number of nodes. Therefore,
$$ B(G^{(k-1)}) \le B(F^{(k-1)}). $$
Combining inequalities,
$$ B(G^{(k-1)}) \le B(F^{(0)}) + (2k-2)b_0. $$
Finally, since $F^{(0)}$ is obtained from $G^{(0)}$ by duplicating shared subgraphs,
$$ B(F^{(0)}) \ge B(G^{(0)}) = B(f_1,\dots,f_m). $$
Thus,
$$ B(f^\pi_1,\dots,f^\pi_m) \le B(f_1,\dots,f_m) + (2k-2)b_0. $$
Resolution of the original errors
- No ancestry tracking is used. The proof avoids any attempt to assign descendants to original nodes in a reduced DAG, which is invalid under merging.
- No unjustified per-node duplication bound. The argument is localized to independent trees where each step contributes a bounded constant increase.
- Reduction is handled correctly. It is never treated as structure-preserving; instead it is explicitly removed via expansion and reintroduced only as a monotone size-decreasing operation.
- No missing invariant. Independence is enforced structurally by converting the OBDD into a forest before analysis, eliminating the need for an evolving charging scheme.
The corrected argument is therefore valid and completes the proof.