TAOCP 7.1.4 Exercise 83
Let (55) denote the recursive apply procedure for $\mathrm{AND}(f,g)$ on BDDs, where each call is indexed by a pair of nodes $(u,v)$ and recursively generates calls on $(u_0,v_0)$, $(u_0,v_1)$, $(u_1,...
Section 7.1.4: Binary Decision Diagrams
Exercise 83. [M20] [M20] Prove that if f and g both have reference count 1, we needn’t consult the memo cache when computing AND(f, g) by (55).
Verified: yes
Solve time: 2m59s
Solution
Let (55) denote the recursive apply procedure for $\mathrm{AND}(f,g)$ on BDDs, where each call is indexed by a pair of nodes $(u,v)$ and recursively generates calls on $(u_0,v_0)$, $(u_0,v_1)$, $(u_1,v_0)$, $(u_1,v_1)$ as determined by the Shannon expansion at the top variable of $u$ and $v$, followed by reduction and memoized lookup.
Assume that every node in the BDD of $f$ and of $g$ has reference count $1$. In the sense of Section 7.1.4, this implies that every node has exactly one incoming pointer from its parent structure, hence no node is shared by two distinct parents. Therefore each of $f$ and $g$ is represented not as a DAG with merging, but as a rooted ordered tree whose nodes correspond to distinct subfunctions without duplication of substructure.
Consider the recursion graph generated by evaluating $\mathrm{AND}(f,g)$ via (55). Each state is a pair $(u,v)$ where $u$ is a node of $f$ and $v$ is a node of $g$. From such a pair, the algorithm generates recursive calls only on pairs formed from the children of $u$ and $v$. Because $u$ and $v$ each have unique parent chains, every node in $f$ occurs in exactly one path from the root of $f$ to a sink, and similarly every node in $g$ occurs in exactly one such path.
Fix any pair $(u,v)$. Any occurrence of this pair in the recursion corresponds to a choice of a path from the root of $f$ to $u$ together with a path from the root of $g$ to $v$. Since neither structure contains shared nodes, each node $u$ is reached by exactly one path and each node $v$ is reached by exactly one path. Consequently the pair $(u,v)$ is reached by exactly one combined pair of paths, so it can appear at most once in the entire recursion tree.
Since the memo cache in (55) is only consulted to detect whether a pair $(u,v)$ has already been computed, and since no pair can occur more than once under the given reference-count-1 hypothesis, no cache lookup can ever yield a previously stored entry. Therefore the cache contains no reusable information during the computation, and every lookup would be unsuccessful even if performed.
Hence the computation of $\mathrm{AND}(f,g)$ under (55) does not require consulting the memo cache when both $f$ and $g$ have reference count $1$.
This completes the proof. ∎