TAOCP 7.2.2.2 Exercise 477

Section 7.2.2.2: Satisfiability

Exercise 477. ▶ [23] [23] (Optimum Boolean evaluation.) Construct clauses that are satisfiable if and only if an $r$-step normal Boolean chain that computes $m$ given functions $g_1$,

$\ldots, g_m$ on $n$ variables. (For example, if $n = 3$ and $g_1 = (x_1 x_2 x_3)$, $g_2 = x_1 \oplus x_2 \oplus x_3$, such clauses with $r = 4$ and $5$ enable a SAT solver to discover a "full adder" of minimum cost; see 7.1.2–(1) and 7.1.2–(22).) Hint: Represent each bit of the truth tables.

Verified: no
Solve time: 4m58s

Solution

Let the possible truth-table rows be indexed by $a\in{0,1}^n$. Introduce variables $X_{j,a}$ for $1\le j\le r$ and $G_{i,a}$ for $1\le i\le m$. The intended meaning of $X_{j,a}$ is that the $j$th entry of the Boolean chain has value $1$ on input $a$, and the intended meaning of $G_{i,a}$ is that the given function $g_i$ has value $1$ on input $a$. The variables $G_{i,a}$ are fixed by unit clauses: include ${G_{i,a}}$ if $g_i(a)=1$ and include ${\bar G_{i,a}}$ if $g_i(a)=0$.

For each step of a normal Boolean chain, introduce variables describing which allowed elementary Boolean operation is used and which earlier entries are selected as its arguments. If the $j$th chain entry is formed from two earlier entries $u$ and $v$ by the Boolean operation $\phi$, let $A_{j,u,v,\phi}$ denote the corresponding choice variable. Add clauses forcing exactly one such variable to be true for each $j$, and add clauses forbidding choices with $u\ge j$ or $v\ge j$, since a chain entry may depend only on previously available values. The at-most-one clauses are

$$ (\bar A_{j,u,v,\phi}\vee \bar A_{j,u',v',\phi'}) $$

for every pair of distinct choices $(u,v,\phi)\ne(u',v',\phi')$ belonging to the same step $j$, together with the single clause

$$ \bigvee_{u,v,\phi} A_{j,u,v,\phi}. $$

For each input $a\in{0,1}^n$ and each possible choice $A_{j,u,v,\phi}$, add clauses encoding the truth-table relation between $X_{j,a}$ and the preceding entries. If $\phi(p,q)=1$, include

$$ (\bar A_{j,u,v,\phi}\vee \bar X_{u,a}\vee \bar X_{v,a}\vee X_{j,a}) $$

and the corresponding clauses for the other three assignments of $(X_{u,a},X_{v,a})$. If $\phi(p,q)=0$, replace $X_{j,a}$ by $\bar X_{j,a}$ in these four clauses. Thus whenever $A_{j,u,v,\phi}$ is true, the clauses force $X_{j,a}$ to equal $\phi(X_{u,a},X_{v,a})$ for every input $a$.

Finally, for every output function $g_i$ and every input $a$, force the appropriate chain entry to equal $g_i(a)$. If the $i$th required output is the entry $X_{s_i}$, add

$$ (\bar X_{s_i,a}\vee G_{i,a}) $$

and

$$ (X_{s_i,a}\vee \bar G_{i,a}). $$

The resulting clauses are satisfiable if an $r$-step normal Boolean chain computing $g_1,\ldots,g_m$ exists. Given such a chain, choose the corresponding variables $A_{j,u,v,\phi}$ to be true, set each $X_{j,a}$ to the value produced by that chain on input $a$, and set the $G_{i,a}$ variables according to the truth tables of the given functions. Every clause above is then satisfied, because the clauses encoding the chosen operations agree with the chain values and the output clauses agree with the required truth tables.

Conversely, suppose the clauses are satisfiable. The exactly-one clauses select a unique operation, pair of predecessors, and step number for each $j$. The relation clauses then force every $X_{j,a}$ to have precisely the value obtained by applying that selected Boolean operation to the selected earlier entries. Hence the satisfying assignment determines a valid normal Boolean chain of $r$ steps. The output clauses force the designated entries to have the truth tables of $g_1,\ldots,g_m$, so this chain computes the required functions. Therefore the constructed clauses are satisfiable if and only if an $r$-step normal Boolean chain computing $g_1,\ldots,g_m$ exists. ∎