TAOCP 7.2.2.2 Exercise 370

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}).

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 370. [20] The clauses obtained by resolution might be needlessly complex even when exercise 369 doesn't apply. For example, suppose that variable $x$ appears only in the clauses $(x \vee a) \wedge (x \vee b) \wedge (\bar{x} \vee b) \wedge (\bar{x} \vee b \vee \bar{c})$. Resolution replaces those four clauses by three others: $(a \vee b) \wedge (a \vee b \vee \bar{c}) \wedge (a \vee b \vee \bar{c})$. Show, however, that only two clauses, both binary, would actually suffice in this particular case.

Verified: no
Solve time: 3m57s

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. ∎