TAOCP 7.1.4 Exercise 36
Exercise 31 provides a method for evaluating a BDD by interpreting each sink and branch node as an element of an algebraic system equipped with operations $\circ$ and $\bullet$, and propagating values...
Section 7.1.4: Binary Decision Diagrams
Exercise 36. [25] [25] By extending exercise 31, explain how to compute the elaborated truth table for any given FBDD, if the abstract operators ◦and • are commutative as well as distributive and associative. (Thus we can find optimum solutions as in Algorithm B, or solve problems such as those in exercises 30 and 33, with FBDDs as well as with BDDs.)
Verified: no
Solve time: 1m50s
Solution
Exercise 31 provides a method for evaluating a BDD by interpreting each sink and branch node as an element of an algebraic system equipped with operations $\circ$ and $\bullet$, and propagating values upward along the ordered structure of the diagram. The essential property used there is distributivity of $\circ$ over $\bullet$ together with associativity, which ensures that subtrees can be evaluated independently and then combined without reference to the global structure of the tree.
For an FBDD the ordering constraint is dropped, but along every root-to-sink path each variable appears at most once. The lack of global ordering prevents reuse of the level structure used in a BDD, so the evaluation must instead be organized over the directed acyclic graph structure itself.
Let $G$ be the given FBDD. For each node $k$, define a value $T(k)$ in the algebra generated by $\circ$ and $\bullet$, representing the elaborated truth table of the subfunction computed at $k$ with respect to all variables appearing in the subgraph rooted at $k$. The sinks are defined first. If $k = \bot$, then $T(k)$ is the identity element for $\bullet$ in the sense used in Exercise 31. If $k = \top$, then $T(k)$ is the identity element for $\circ$.
For a branch node $k$ labeled by variable $x_i$ with low successor $L(k)$ and high successor $H(k)$, every complete evaluation of the subgraph rooted at $k$ splits according to the value of $x_i$. When $x_i = 0$, the computation proceeds through $L(k)$, and when $x_i = 1$, it proceeds through $H(k)$. Since each path contains at most one occurrence of $x_i$, these two cases are disjoint and exhaust all possibilities at that node.
The contribution of the low branch is obtained by extending the elaborated truth table $T(L(k))$ with the condition $x_i = 0$. The contribution of the high branch is obtained analogously from $T(H(k))$ under $x_i = 1$. These two contributions are then combined using $\bullet$, since $\bullet$ aggregates alternatives corresponding to different cases of the same decision point. The interaction of substructures is governed by $\circ$, since subresults corresponding to independent subgraphs are combined multiplicatively in the sense of Exercise 31.
Thus $T(k)$ is defined by
$$ T(k) = \bigl(T(L(k)) \circ [x_i = 0]\bigr) \bullet \bigl(T(H(k)) \circ [x_i = 1]\bigr), $$
where $[x_i = b]$ denotes the elementary elaboration contributed by fixing variable $x_i$ to the value $b$. The precise form of these elementary contributions is the same as in Exercise 31, where a variable restriction is represented as an operator acting on the algebraic value carried by a subdiagram.
Because $\circ$ is commutative and associative, the order in which variables are encountered along different paths does not affect the combined value of independent subcomputations. Because $\bullet$ is also commutative and associative, merging the low and high contributions at a node is independent of evaluation order. Distributivity of $\circ$ over $\bullet$ ensures that whenever a subgraph is shared, its contribution factors correctly across all contexts in which it appears.
The evaluation proceeds by processing nodes in reverse topological order of the underlying dag. Since the structure is acyclic and every node has two successors, this order is well defined. Each node is evaluated exactly once, and its value depends only on previously computed successor values. The elaborated truth table of the entire FBDD is $T(r)$, where $r$ is the root node.
Correctness follows by induction on the structure of the dag. For sinks the definition matches the intended truth-table interpretation. For a branch node $k$, assume $T(L(k))$ and $T(H(k))$ correctly represent the elaborated truth tables of their respective subgraphs. Every assignment to variables below $k$ either assigns $x_i = 0$ or $x_i = 1$, and the restriction that $x_i$ does not reappear on any path ensures that these cases partition the set of all assignments to the subgraph variables. The combination using $\bullet$ therefore aggregates all contributions without duplication, while $\circ$ combines independent contributions from disjoint substructures. This establishes that $T(k)$ is the correct elaborated truth table for the subfunction rooted at $k$.
Since each node is processed once and each edge is used a constant number of times in the evaluation of its parent, the computation requires time proportional to the number of nodes in the FBDD.
The resulting value $T(r)$ is the elaborated truth table of the entire FBDD, computed correctly under the commutative, associative, and distributive algebra defined by $\circ$ and $\bullet$.
This completes the proof. ∎