TAOCP 7.1.4 Exercise 95

Exercise 95. ▶ [20] [20] Improve on (65) by testing if rl = 1 before computing rh.

Verified: no
Solve time: 6m46s

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. ∎