Section 7.1.4: Binary Decision Diagrams

Exercise 103. ▶ [20] [20] Mr. B. C. Dull wanted to evaluate the formula ∃y1 . . . ∃ym((y1 = f1(x1, . . . , xn)) ∧· · · ∧(ym = fm(x1, . . . , xn)) ∧g(y1, . . . , ym)), for certain functions f1, . . . , fm, and g. But his fellow student, J. H. Quick, found a much simpler formula for the same problem. What was Quick’s idea?

Verified: no
Solve time: 3m30s

Solution

Let

$$ \Phi(x_1,\dots,x_n)

\exists y_1 \dots \exists y_m \Bigl( (y_1 = f_1(x_1,\dots,x_n)) \wedge \cdots \wedge (y_m = f_m(x_1,\dots,x_n)) \wedge g(y_1,\dots,y_m) \Bigr). $$

Fix any assignment of $(x_1,\dots,x_n)$. The conjunction forces each $y_i$ to satisfy $y_i = f_i(x_1,\dots,x_n)$. Each such constraint determines $y_i$ uniquely, so every satisfying assignment of the quantified variables must assign $y_i$ exactly the value $f_i(x_1,\dots,x_n)$ for $1 \le i \le m$.

Substituting these forced values into $g(y_1,\dots,y_m)$ reduces the inner formula to

$$ g(f_1(x_1,\dots,x_n),\dots,f_m(x_1,\dots,x_n)). $$

If the existential quantifiers are evaluated after the constraints are enforced, exactly one tuple $(y_1,\dots,y_m)$ is admissible for each fixed $(x_1,\dots,x_n)$, so the existential quantification contributes no additional choices. The truth value of $\Phi$ at $(x_1,\dots,x_n)$ therefore matches the truth value of the composed function.

Thus the entire formula is equivalent to

$$ g(f_1(x_1,\dots,x_n),\dots,f_m(x_1,\dots,x_n)). $$

$$ \boxed{g(f_1(x_1,\dots,x_n),\dots,f_m(x_1,\dots,x_n))} $$

This completes the solution. ∎