|
3-SAT is a restriction of SAT where each clause is required to have exactly 3 literals.
For example, formula
| (¬x ∨ y ∨ ¬w) ∧ |
| (¬y ∨ z ∨ w) ∧ |
| (x ∨ ¬z ∨ y) |
has exactly 3 literals per clause.
Because 3-SAT is a restriction of SAT, it is not obvious that 3-SAT is difficult to solve. Maybe the restriction makes it easier.
But, in reality, 3-SAT is just as difficult as SAT; the restriction to 3 literals per clause makes no difference.
Theorem. 3-SAT is NP-complete.
Proof. There are two parts to the proof.
Part (a). We must show that 3-SAT is in NP. But we already showed that SAT is in NP. Surely, and nondeterministic algorith for SAT also works for 3-SAT; it does not care about the restriction to 3 literals per clause.
Part (b). We need to show, for every problem X in NP, X ≤ 3-SAT. But we can accomplish that by showing that SAT ≤p 3-SAT.
So our goal is to find a polynomial-time reduction from SAT to 3-SAT. The reduction is a polynomial-time computable function f that takes a clausal formula φ and yields a clausal formula φ′ with 3 literals per clause.
The reduction function works on one clause of φ at a time. Here is what it does on a clause C.
If C already has 3 literals, leave it alone.
If C has fewer than 3 literals, just duplicate one or two of the literals. For example, if C is (x ∨ ¬y), then the reduction replaces that clause by (x ∨ x ∨ ¬y).
Suppose that clause C is (ℓ1 ∨ ℓ2 ∨ … ∨ ℓn), where n > 3. Create new variables λ1, λ2, etc., and replace C by clauses
| (ℓ1 ∨ ℓ2 ∨ λ1) ∧ |
| (¬λ1 ∨ ℓ3 ∨ λ2) ∧ |
| (¬λ2 ∨ ℓ4 ∨ λ3) ∧ |
| (¬λ3 ∨ ℓ5 ∨ λ4) ∧ |
| … |
| (¬λn−4 ∨ ℓn−2 ∨ λn−3) ∧ |
| (¬λn−3 ∨ ℓn−1 ∨ ℓn) |
For example, clause (x ∨ ¬y ∨ z ∨ u ∨ ¬v) is replaced by
| (x ∨ ¬y ∨ λ1) ∧ |
| (¬λ1 ∨ z ∨ λ2) ∧ |
| (¬λ2 ∨ u ∨ ¬v) |
Each clause gets its own new λ variables.
We need to show that doing this replacement does not affect whether the formula is satisfiable.
Suppose that φ is satisfiable. Select an assignment A of truth values to φ's variables that makes φ true.
Since assignment A makes φ true, it must make at least one of the literals in clause C true.
Select a true literal ℓi in C. Set λj = true for j = 1, …, i − 2 and λj = false for j = i − 1, ..., n−3. For example, if i = 4 and n = 7 then, with that assignment, the clauses in φ′ that represent clause C are as follows.
| (ℓ1 ∨ ℓ2 ∨ true) ∧ |
| (false ∨ ℓ3 ∨ true) ∧ |
| (false ∨ ℓ4 ∨ false) ∧ |
| (true ∨ ℓ5 ∨ false) ∧ |
| (true ∨ ℓ6 ∨ ℓ7) |
Since ℓ4 is true, every clause is true.
So every clause can be satisfied, and φ′ is satisfiable.
Suppose that φ′ is satisfiable. Choose values for the variables to make φ′ true. We need to show that, no matter how the values of the λ variables are chosen, each original clause C must have one true literal. That is, at least one of ℓ1, …, ℓn is true.
So suppose that all of ℓ1, …, ℓn are false. From the first clause,
| (ℓ1 ∨ ℓ2 ∨ λ1) |
λ1 must be true. But then, from the second clause,
| (¬λ1 ∨ ℓ3 ∨ λ2) |
λ2 must also be true. Working through the clauses that correspond to original clause C, we see that λ1, …, λn−3 must be true. But then the last clause,
| (¬λn−3 ∨ ℓn−1 ∨ ℓn) |
is false, contradicting the choice of variable values to make φ′ true. ◊
What if we restrict SAT even further, insisting that every clause have exactly 2 literals? Call that problem 2-SAT.
Then the problem becomes easy. There is a polynomial time algorithm to solve 2-SAT. The key to the algorithm is that, if you are looking at clause
and ℓ1 is false, then ℓ2 must be true. Choosing a value for a variable leads to other variable values being forced without much effort.
There is more to the algorithm than that, but that is the heart of it.
|