TAOCP 7.1.4 Exercise 197

Section 7.1.4: Binary Decision Diagrams

Exercise 197. [25] [25] Modify the algorithm of exercise 138 so that it computes the “master z- profile chart” of f. (Then Zmin(f) and Zmax(f) can be found as in exercise 133.)

Verified: yes
Solve time: 1m57s

Solution

Let $f$ be a Boolean function on variables $x_1,\dots,x_n$, and let its BDD be given in the ordered and reduced form described in Section 7.1.4. For any node $v$ in the BDD, write $f_v$ for the subfunction represented by $v$. The sink nodes represent the constant functions $f_\bot \equiv 0$ and $f_\top \equiv 1$.

Exercise 138 constructs the $z$-profile of a function by traversing the structure that represents $f$ and combining contributions from subfunctions induced by fixing leading variables. The key feature used there is that every subfunction of $f$ arises as $f_v$ for some node $v$ in the BDD, and that the ordered structure ensures each such subfunction is determined entirely by the node label and its two successors.

The “master $z$-profile chart” of $f$ is the collection of $z$-profiles of all subfunctions of $f$, organized so that every subfunction that arises during the decomposition is recorded exactly once. Formally, it is the mapping that assigns to every BDD node $v$ the $z$-profile of $f_v$, including the sink nodes.

To compute this structure, the algorithm of exercise 138 is modified so that it is executed in a memoized bottom-up fashion over the directed acyclic graph of the BDD. A table $\mathcal{T}$ is maintained whose entries are indexed by nodes of the BDD. Each entry $\mathcal{T}[v]$ stores the $z$-profile of $f_v$ once it has been computed.

The computation begins at the sinks. Since $f_\bot$ and $f_\top$ are constant functions, their $z$-profiles are computed directly from the definition used in exercise 138, and stored as $\mathcal{T}[\bot]$ and $\mathcal{T}[\top]$.

For any internal node $v$, let $V(v)=x_i$ and let its LO and HI successors be $v_0$ and $v_1$. The subfunction $f_v$ is defined by the Shannon decomposition

$$ f_v = (x_i=0),?, f_{v_0} : f_{v_1}. $$

The $z$-profile construction in exercise 138 applies this decomposition recursively: the contribution of $v$ is determined entirely by the already-computed $z$-profiles of $v_0$ and $v_1$, together with the structural shift induced by introducing the variable $x_i$ at the root of the subfunction.

The modification consists of enforcing that this recursive computation is performed once per node. When computing $\mathcal{T}[v]$, the algorithm first checks whether $\mathcal{T}[v]$ is already defined. If so, it is returned immediately. Otherwise, $\mathcal{T}[v_0]$ and $\mathcal{T}[v_1]$ are computed recursively, and the original combination rule from exercise 138 is applied to produce $\mathcal{T}[v]$ from these two $z$-profiles, after which the result is stored.

Because the BDD is a directed acyclic graph, every path from the root eventually reaches a sink, and no node is visited more than once under this memoized evaluation. Therefore each node contributes exactly one $z$-profile computation, and the entire master chart is produced after processing all reachable nodes from the root.

Correctness follows from the fact that the computation at each node $v$ reproduces exactly the same recurrence as in exercise 138 applied to the subfunction $f_v$. Since every subfunction of $f$ corresponds to a unique BDD node by the bead correspondence, every entry in the master chart corresponds to a well-defined subfunction, and no subfunction is omitted or duplicated. The memoization step does not alter the computed values, only the order and number of recomputations.

The resulting algorithm therefore outputs the full master $z$-profile chart in time proportional to the number of BDD nodes, since each node is evaluated once and each evaluation performs a constant number of $z$-profile operations inherited from exercise 138.

This completes the proof. ∎