TAOCP 7.2.2.2 Exercise 152

Section 7.2.2.2: Satisfiability

Exercise 152. [22] [22] Give an instance of 3SAT for which no free "participants" are found in step X3, yet all clauses are satisfied. Also describe an instance with no forced satisfaction.

Verified: no
Solve time: 3m28s

Solution

The two phenomena concern different notions in Algorithm $L$. A free participant in step X3 is not a synonym for an unset variable in an arbitrary satisfying assignment. It is a variable that the lookahead procedure can choose as a new candidate because it still participates in an unsatisfied part of the residual formula. Likewise, forced satisfaction concerns literals whose truth values are implied during the propagation process, not merely literals that happen to occur in clauses.

For the first example, consider the $3$SAT instance

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

This is the complete set of all eight possible clauses on the three variables $1,2,3$. Every possible truth assignment satisfies exactly seven of these clauses and falsifies exactly one of them. Therefore the instance itself is not satisfiable. Hence this is not yet the desired example.

To obtain a satisfiable example with the required property, delete one clause, say $\bar 1\bar 2\bar 3$, and let

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

Now assign

$$ 1=0,\qquad 2=0,\qquad 3=0 . $$

The only clause falsified by this assignment would be

$$ \bar 1\bar 2\bar 3, $$

but that clause is not present. The remaining seven clauses are all satisfied. Thus the formula is satisfiable.

Run the lookahead procedure until it reaches the state represented by this complete assignment. At that point every clause is already satisfied. Step X3 examines the remaining unsatisfied clauses in order to find free participants, but there are none. The set of clauses requiring further attention is empty, so the participant list produced by X3 is empty. Nevertheless, the current state is a satisfying state.

This shows that the condition “X3 finds no free participants” does not imply that the formula is unsatisfied. The correct way to verify satisfaction is simply to scan every clause and check whether at least one literal in the clause has value $1$. For a formula with $m$ clauses and $n$ variables this requires $O(mn)$ literal inspections in the worst case, or $O$ of the total number of literal occurrences.

For an instance with no forced satisfaction, take the single-clause $3$SAT formula

$$ G={123}. $$

No literal is forced. The clause is satisfied whenever at least one of $1,2,3$ is true, so none of the three literals must be assigned a particular value. For example, the satisfying assignments

$$ (1,2,3)=(1,0,0),\qquad (0,1,0),\qquad (0,0,1) $$

all satisfy the formula, and the literal responsible for satisfaction is different in each case. Hence no literal is forced to satisfy the clause.

More generally, any $3$SAT instance consisting only of clauses of length three and containing no unit consequences under propagation has no forced satisfaction at the initial state. The example above is the smallest such instance. ∎