
3SAT 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 3SAT is a restriction of SAT, it is not obvious that 3SAT is difficult to solve. Maybe the restriction makes it easier.
But, in reality, 3SAT is just as difficult as SAT; the restriction to 3 literals per clause makes no difference.
Theorem. 3SAT is NPcomplete.
Proof. There are two parts to the proof.
Part (a). We must show that 3SAT is in NP. But we already showed that SAT is in NP. Surely, and nondeterministic algorith for SAT also works for 3SAT; 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 ≤_{} 3SAT. But we can accomplish that by showing that SAT ≤_{p} 3SAT.
So our goal is to find a polynomialtime reduction from SAT to 3SAT. The reduction is a polynomialtime 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 2SAT.
Then the problem becomes easy. There is a polynomial time algorithm to solve 2SAT. 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.
