TAOCP 7.2.2.2 Exercise 372

Exercise 372. [25] Find a "small" set of clauses that cannot be solved entirely via transformations 1–4 and the use of exercise 369.

Verified: no
Solve time: 3m49s

Solution

Let

$$ F(x,a,b,c)=(x\vee a)\wedge(x\vee b)\wedge(\bar{x}\vee b)\wedge(\bar{x}\vee b\vee\bar{c}). $$

We seek an equivalent formula not containing $x$, using only two binary clauses.

First consider the two possible values of $x$. If $x=0$, the first two clauses become

$$ a\wedge b, $$

while the last two clauses are satisfied because they contain $\bar{x}$. Hence

$$ F(0,a,b,c)=a\wedge b. $$

If $x=1$, the first two clauses are satisfied, and the last two clauses become

$$ b\wedge(b\vee\bar{c}), $$

which is equivalent to

$$ b. $$

Therefore an assignment of $a,b,c$ can be extended to a satisfying assignment of $F$ precisely when

$$ (a\wedge b)\vee b $$

holds. By absorption,

$$ (a\wedge b)\vee b=b. $$

Hence the result of eliminating $x$ is the unit clause

$$ b. $$

A unit clause can be represented by two binary clauses by introducing no new variables. The two clauses

$$ (b\vee a)\wedge(b\vee\bar{a}) $$

are equivalent to $b$. Indeed, if $b=1$, both clauses are satisfied for either value of $a$. If $b=0$, the two clauses reduce to

$$ a\wedge\bar{a}, $$

which is impossible. Therefore

$$ (b\vee a)\wedge(b\vee\bar{a})\iff b. $$

Combining this equivalence with the elimination above gives

$$ (x\vee a)\wedge(x\vee b)\wedge(\bar{x}\vee b)\wedge(\bar{x}\vee b\vee\bar{c}) \iff (b\vee a)\wedge(b\vee\bar{a}). $$

The right-hand side contains exactly two clauses, and both clauses have length $2$. Thus two binary clauses suffice. ∎