TAOCP 7.1.1 Exercise 39
Let the internal nodes of the extended binary tree be $v_1,\ldots,v_N$ and assign to each $v_k$ a Boolean variable $y_k$.
Exercise 39. ▶ [25] Let $f(x_1, \ldots, x_n)$ be a Boolean formula represented as an extended binary tree with $N > 0$ internal nodes and $N+1$ leaves. Each leaf is labeled with a variable $x_i$, and each internal node is labeled with one of the sixteen binary operators in Table 1; applying the operators from bottom to top yields $f(x_1, \ldots, x_n)$ as the value of the root.
Explain how to construct a formula $F(x_1, \ldots, x_n, y_1, \ldots, y_N)$ in 3CNF, having exactly $4N+1$ clauses, such that $f(x_1, \ldots, x_n) = \exists y_1 \ldots \exists y_N, F(x_1, \ldots, x_n, y_1, \ldots, y_N)$. (Thus $f$ is satisfiable if and only if $F$ is satisfiable.)
Verified: yes
Solve time: 1m05s
Solution
Let the internal nodes of the extended binary tree be $v_1,\ldots,v_N$ and assign to each $v_k$ a Boolean variable $y_k$. Each leaf is labeled by some input variable $x_i$. For a node $v_k$ with left child labeled by a variable $a_k$ and right child labeled by a variable $b_k$, where each of $a_k,b_k$ is either some $x_i$ or some $y_j$ with $j<k$, let the operator at $v_k$ be $f_k \in {\wedge,\vee,\oplus,\equiv,\ldots}$ as given by Table 1. The value computed at $v_k$ is required to satisfy
$$ y_k = f_k(a_k,b_k). $$
For each internal node $v_k$, construct a 3CNF formula enforcing this equivalence by excluding exactly those assignments of $(a_k,b_k,y_k)$ that violate the truth table of $f_k$. For each $(\alpha,\beta)\in{0,1}^2$, let $\gamma = f_k(\alpha,\beta)$. The assignment
$$ a_k=\alpha,\quad b_k=\beta,\quad y_k \ne \gamma $$
must be forbidden. This is achieved by the clause
$$ \ell(a_k,\alpha)\ \vee\ \ell(b_k,\beta)\ \vee\ \ell(y_k,\gamma), $$
where
$$ \ell(u,0)=u,\qquad \ell(u,1)=\bar u. $$
Each such clause is falsified exactly when $a_k=\alpha$, $b_k=\beta$, and $y_k=\gamma$, and is satisfied for all other assignments. This produces exactly $4$ clauses per internal node, one for each pair $(\alpha,\beta)\in{0,1}^2$.
Let $F_0$ be the conjunction of all clauses obtained from all internal nodes:
$$ F_0 = \bigwedge_{k=1}^N \bigwedge_{(\alpha,\beta)\in{0,1}^2} \left(\ell(a_k,\alpha)\ \vee\ \ell(b_k,\beta)\ \vee\ \ell(y_k,f_k(\alpha,\beta))\right). $$
This formula is in 3CNF since each clause contains exactly three literals.
The root of the tree corresponds to some variable $y_r$. The formula $F_0$ enforces that $y_r$ equals the value computed by the tree, but it does not force this value to be $1$. To enforce that the entire formula evaluates to true, adjoin the single clause
$$ (y_r). $$
Let the resulting formula be $F$.
The total number of clauses in $F_0$ is $4N$. The additional root clause contributes $1$ clause, so $F$ has exactly $4N+1$ clauses.
If $f(x_1,\ldots,x_n)=1$, assign each internal variable $y_k$ the value computed by evaluating the tree bottom-up from the given $x_i$. Each clause in $F_0$ is satisfied since every node respects its truth table, and the root clause is satisfied since $y_r=1$.
If $F$ is satisfiable, then the root clause forces $y_r=1$. Every clause in $F_0$ enforces correct local evaluation at each node, so the assignment to the $y_k$'s propagates consistently down the tree and yields a valid evaluation of the original formula. The value at the root equals $1$, so the induced evaluation of $f(x_1,\ldots,x_n)$ is $1$.
Thus
$$ f(x_1,\ldots,x_n) = \exists y_1\cdots \exists y_N, F(x_1,\ldots,x_n,y_1,\ldots,y_N). $$
This completes the proof. ∎