TAOCP 7.1.4 Exercise 94

Exercise 94. [21] [21] Explain why (65) performs existential quantification correctly.

Verified: no
Solve time: 6m

Solution

Let $f$ be a Boolean function represented by an ordered reduced BDD, and let $x_j$ be the variable being eliminated. Let the operation defined in (65) produce a new BDD $g$, denoted

$g = \exists x_j, f,$

by a recursive transformation on nodes.

The semantic definition of existential quantification is that for every input $x = (x_1,\dots,x_{j-1},x_{j+1},\dots,x_n)$,

$g(x) = 1 \iff f(x_1,\dots,x_{j-1},0,x_{j+1},\dots,x_n)=1 \ \text{or}\ f(x_1,\dots,x_{j-1},1,x_{j+1},\dots,x_n)=1.$

Thus $g$ depends only on assignments to variables other than $x_j$, and its truth value is the disjunction of the two restrictions of $f$ obtained by fixing $x_j=0$ and $x_j=1$.

Let a BDD node $v$ be labeled by variable $V(v)=i$, with children $\mathrm{LO}(v)$ and $\mathrm{HI}(v)$ representing cofactors $f_{x_i=0}$ and $f_{x_i=1}$. The existential operation is defined recursively as follows.

If $v$ is a sink, the result is unchanged since sinks do not depend on $x_j$.

If $V(v) > j$, the variable $x_j$ does not occur at or below $v$ because the BDD is ordered, so every path below $v$ avoids $x_j$. The subfunction represented by $v$ already satisfies $\exists x_j f_v = f_v$, so the algorithm returns $v$ unchanged.

If $V(v) = j$, the node represents the decomposition

$f_v = (f_{\mathrm{LO}(v)} \text{ under } x_j=0) ;\lor; (f_{\mathrm{HI}(v)} \text{ under } x_j=1).$

For existential quantification, both branches become relevant for the same external assignment, so the correct function is

$\exists x_j f_v = f_{\mathrm{LO}(v)} ;\lor; f_{\mathrm{HI}(v)}.$

Hence (65) replaces node $v$ by the BDD node representing the reduced form of $\mathrm{Apply}(\lor,\mathrm{LO}(v),\mathrm{HI}(v))$, followed by reduction.

If $V(v) < j$, the variable $x_j$ appears deeper in the structure. For a fixed assignment to variables above $v$, the evaluation of $f_v$ depends on $x_j$ only through its children, so existential quantification distributes over the structure:

$\exists x_j f_v = \text{node with variable } V(v), \text{LO}=\exists x_j f_{\mathrm{LO}(v)}, \text{HI}=\exists x_j f_{\mathrm{HI}(v)}.$

Correctness follows by induction on the partial order induced by the BDD variable ordering. Assume the transformation is correct for all descendants of a node $v$. Three cases occur.

If $V(v) > j$, both $f_v$ and the computed result evaluate identically on all assignments since $x_j$ is not tested below $v$. Thus equivalence holds.

If $V(v) = j$, for every assignment $\alpha$ to variables other than $x_j$, the evaluation of the transformed node equals

$1 \iff f_{\mathrm{LO}(v)}(\alpha)=1 \ \text{or}\ f_{\mathrm{HI}(v)}(\alpha)=1,$

which matches the semantic definition of $\exists x_j f_v$.

If $V(v) < j$, let $\alpha$ be an assignment to variables excluding $x_j$. The evaluation of the constructed node follows the same branching as $v$, and by the induction hypothesis the children already compute the correct existentially quantified subfunctions. Therefore the parent node computes the correct combination of those values, preserving equality with the semantic definition.

Since every node is treated in one of these cases and the recursion terminates because variable indices strictly increase along every path, the constructed BDD computes exactly the truth table of $\exists x_j f$. Reduction steps preserve the represented function because they only merge isomorphic subgraphs or eliminate redundant tests, both of which do not change the evaluated Boolean function.

This completes the proof. ∎