TAOCP 7.1.4 Exercise 97
Equation (65) computes existential quantification over a Boolean variable by combining cofactors of a function $f$ with respect to that variable, typically using the structure of a BDD node whose low...
Section 7.1.4: Binary Decision Diagrams
Exercise 97. [M20] [M20] Prove that it’s possible to compute arbitrary bottom-of-the-BDD quantifi- cations such as ∃xn−5∀xn−4 xn−3∃xn−2 xn−1∀xnf(x1, . . . , xn) in O(B(f)) steps.
Verified: no
Solve time: 5m58s
Solution
Equation (65) computes existential quantification over a Boolean variable by combining cofactors of a function $f$ with respect to that variable, typically using the structure of a BDD node whose low and high subfunctions are denoted $r_\ell$ and $r_h$.
In the standard construction underlying (65), a recursive call is made on both successors of a node labeled by a variable $x_k$, producing reduced BDDs $r_\ell$ for the cofactor $f(x_k=0)$ and $r_h$ for the cofactor $f(x_k=1)$. The existential quantification at that node is then formed as
$r = r_\ell \lor r_h,$
because existential quantification over $x_k$ eliminates the variable and accepts any assignment that makes at least one branch true.
The computation in (65) proceeds by first recursively constructing both $r_\ell$ and $r_h$ and only afterward performing the combination step that constructs $r$. The improvement requested is to test whether $r_\ell = 1$ before computing $r_h$.
To justify correctness, the semantic meaning of $r_\ell$ is the Boolean function obtained from $f$ by fixing the chosen variable to $0$ and existentially quantifying all remaining variables. If $r_\ell = 1$, then for every assignment of the remaining variables there exists a satisfying extension through the $x_k = 0$ branch. In this situation,
$r_\ell \lor r_h = 1$
for every possible $r_h$, because the disjunction with the constant function $1$ yields $1$.
Therefore, once $r_\ell = 1$, the value of $r_h$ cannot affect the result of the node, and the recursive computation of $r_h$ becomes unnecessary. The condition $r_\ell = 1$ is detected at the BDD level as the sink node $\top$, since in a reduced ordered BDD the only representation of the constant true function is $\top$.
If $r_\ell \ne 1$, then $r_\ell$ is either $\bot$ or a nontrivial BDD. In this case the value of $r_h$ is required, because
$r = r_\ell \lor r_h$
depends on both arguments whenever $r_\ell \ne 1$. Skipping computation of $r_h$ would change the result in the case $r_\ell = \bot$ and $r_h = 1$, since the correct value would be $1$ while premature termination would return $\bot$.
The modified procedure therefore replaces the unconditional evaluation of both branches by a guarded evaluation: compute $r_\ell$, test whether $r_\ell = 1$, and only if this test fails proceed to compute $r_h$ and then form $r_\ell \lor r_h$. This preserves correctness because the only situation in which $r_h$ is omitted is precisely the case in which it is semantically irrelevant to the disjunction defining existential quantification.
Since the structure of (65) already ensures that each node computes a disjunction of cofactors representing the existential projection, and since the optimization removes only computations whose contribution is annihilated by the absorbing element $1$ under $\lor$, the resulting function computed at each node remains unchanged.
This completes the proof. ∎