TAOCP 7.2.2.2 Exercise 248

Section 7.2.2.2: Satisfiability

Exercise 248. [M20] [M20] Formally speaking, SAT is the problem of evaluating the quantified formula

$$\exists x_1 \ldots \exists x_{n-1} ; \exists x_n ; F(x_1, \ldots, x_{n-1}, x_n),$$

where $F$ is a Boolean function given in CNF as a conjunction of clauses. Explain how to transform the CNF for $F$ into the CNF for $F'$ in the reduced problem

$$\exists x_1 \ldots \exists x_{n-1} ; F'(x_1, \ldots, x_{n-1}, 0) \vee F'(x_1, \ldots, x_{n-1}, 1).$$

Verified: no
Solve time: 2m06s

---

Solution

By (112), the six clauses are

$$ 1234,\qquad 12\bar{3},\qquad \bar{1}\bar{2},\qquad \bar{1}3,\qquad 2\bar{3},\qquad 3\bar{4}. $$

The clause $\bar{1}\bar{2}$ is omitted, leaving

$$ F={1234,\ 12\bar{3},\ \bar{1}3,\ 2\bar{3},\ 3\bar{4}}. $$

Variable elimination removes a variable by replacing all pairs of clauses containing complementary literals of that variable by their resolvents, then deleting the clauses containing the eliminated variable.

Eliminate $4$. The only clauses containing $4$ are

$$ 1234,\qquad 3\bar{4}. $$

Their resolvent is

$$ 1234\mathbin{\bowtie}3\bar{4}=123. $$

After removing the clauses containing $4$, the formula becomes

$$ {123,\ 12\bar{3},\ \bar{1}3,\ 2\bar{3}}. $$

Next eliminate $3$. The clauses containing $3$ are

$$ 123,\qquad \bar{1}3, $$

and the clauses containing $\bar{3}$ are

$$ 12\bar{3},\qquad 2\bar{3}. $$

The possible resolvents are

$$ 123\mathbin{\bowtie}12\bar{3}=12, $$

$$ 123\mathbin{\bowtie}2\bar{3}=12, $$

$$ \bar{1}3\mathbin{\bowtie}12\bar{3} =\bar{1}12, $$

and

$$ \bar{1}3\mathbin{\bowtie}2\bar{3} =\bar{1}2. $$

The third resolvent contains both $1$ and $\bar{1}$, so it is tautological and is discarded. The duplicate clause $12$ is retained only once. The remaining formula is therefore

$$ {12,\bar{1}2}. $$

Now eliminate $2$. Both clauses contain the positive literal $2$, and no clause contains $\bar{2}$. Thus $2$ is a pure literal. Deleting the clauses containing $2$ leaves the empty clause set.

The variable-elimination procedure applied to the five clauses of (112) therefore produces

$$ \boxed{\varnothing}. $$

The result is the empty set of clauses, not the empty clause $\epsilon$. Hence the five-clause formula obtained after omitting $\bar{1}\bar{2}$ is satisfiable. The omitted clause is necessary for the contradiction present in the original six-clause formula.