P26 · SAT → 3SAT

🔊 Listen

1 · What we are reducing, and why we care

SAT asks: given an arbitrary CNF formula, is there an assignment that satisfies it? 3SAT is the same question but restricted to formulas where every clause has exactly three literals. Cook–Levin proves SAT is NP-complete. Once we reduce SAT to 3SAT in polynomial time, 3SAT inherits the NP-completeness — and because 3SAT has a clean uniform shape, it becomes the starting point for almost every other NP-completeness proof in the chain (CLIQUE, VERTEX-COVER, HAM-PATH, SUBSET-SUM…).

Goal of the reduction

Given a CNF formula φ over variables x₁, …, x_n with clauses of arbitrary width, build in polynomial time a 3CNF formula φ′ such that φ is satisfiable iff φ′ is satisfiable.

The whole trick is one rule applied repeatedly. We replace each clause of width k with a chain of clauses of width 3, glued together by fresh auxiliary variables. The chain has the property that any satisfying assignment of the chain implies at least one of the original literals was true, and conversely if one of the original literals is true the chain can be satisfied by an appropriate choice of auxiliaries.

🔊 Listen

2 · The splitting rule, by clause width

The two "pad" cases (k = 1 and k = 2) are the ones students forget. The auxiliary variables p, q there are fresh — each clause-pad gets its own. The four-clause padding for k = 1 forces ℓ₁ to be true in every satisfying assignment, which is exactly what the unit clause (ℓ₁) demands. The two-clause padding for k = 2 forces ℓ₁ ∨ ℓ₂ for the same reason: no choice of p can satisfy both clauses unless ℓ₁ ∨ ℓ₂ already holds.

🔊 Listen

3 · Why satisfiability is preserved · both directions

Forward direction (⇒)

Suppose φ is satisfiable under assignment τ. Take any clause C of width k ≥ 4. Some literal ℓ_j in C is true under τ. Walk the chain left to right and set each auxiliary a_i to true while i < j − 1, then to false from i = j − 1 onward. Every chain-clause becomes satisfied: the early ones because their a_i is true; the clause containing ℓ_j because ℓ_j is true; the later ones because their ¬a_i is true.

Reverse direction (⇐)

Suppose φ′ is satisfied under τ′. Project τ′ back to the original variables. Claim: at least one ℓ_j of the original clause C is true. Suppose for contradiction that all ℓ₁, …, ℓ_k are false. Then the first chain-clause forces a₁ = true (else nothing in it is satisfied). The second chain-clause now needs a₂ = true (its ¬a₁ is false and both literals are false). Propagating, every a_i = true. But the final chain-clause is (¬a_k−3 ∨ ℓ_k−1 ∨ ℓ_k) — ¬a_k−3 is false, ℓ_k−1 and ℓ_k are false — contradiction. So some ℓ_j must be true.

🔊 Listen

4 · Worked example · one CNF formula start-to-finish

Take the formula

φ = (x₁ ∨ x₂ ∨ ¬x₃ ∨ x₄ ∨ ¬x₅) ∧ (¬x₁ ∨ x₃) ∧ (x₂)

Three clauses of widths 5, 2, 1. Apply the rules:

Clause 1, k=5 → (x₁ ∨ x₂ ∨ a₁) ∧ (¬a₁ ∨ ¬x₃ ∨ a₂) ∧ (¬a₂ ∨ x₄ ∨ ¬x₅) [2 fresh aux: a₁, a₂]
Clause 2, k=2 → (¬x₁ ∨ x₃ ∨ p₁) ∧ (¬x₁ ∨ x₃ ∨ ¬p₁) [1 fresh aux: p₁]
Clause 3, k=1 → (x₂ ∨ p₂ ∨ q₂) ∧ (x₂ ∨ p₂ ∨ ¬q₂) ∧ (x₂ ∨ ¬p₂ ∨ q₂) ∧ (x₂ ∨ ¬p₂ ∨ ¬q₂) [2 fresh aux: p₂, q₂]

Result: a 3CNF with 9 clauses and 5 new variables — same satisfiability as φ. Sanity check: original has 3 clauses summing to 5+2+1 = 8 literals, output has 9 clauses summing to 27 literals; the growth is linear in the size of φ.

🔊 Listen

5 · Animated demo · auto-plays · loops

🔊 Listen

6 · Polynomial-time check · why the reduction is a ≤_p

For a clause of width k, the splitting produces:

k − 2 new clauses
k − 3 new auxiliary variables

So if φ has m clauses with total literal count L, the output 3CNF has at most L clauses and L auxiliary variables in the worst case. The reduction runs in O(L) time — clearly polynomial in |φ|. Padding for k = 1 or 2 adds at most 4 clauses each, again linear.

🔊 Listen

7 · Pitfalls students stumble on

Auxiliary variables must be fresh per clause. If you reuse a₁ across two clause-splits, you create unwanted dependencies and break preservation. Every clause introduces its own batch.
Don't forget k = 1 and k = 2. Unit clauses and 2-clauses aren't already in 3CNF. You must pad them, otherwise the output isn't a 3CNF formula at all.
The reverse direction needs the chain argument, not "by symmetry." The proof above propagates a forced a_i = true through every link until the last clause fails. Glossing over this loses marks.
This is not the same as the "exactly-3" definition. Some sources define 3SAT as "at most 3 literals" and skip k ≤ 2 padding. Sipser uses "exactly 3" — check which convention the rubric expects.

🔊 Listen

8 · Q&A defence notes

Q1. Why a fresh auxiliary variable per clause?
Reusing an auxiliary across multiple clause-splits creates correlations between unrelated clauses — if a is forced true to satisfy one chain, the other chain inherits that constraint and might become unsatisfiable when the original was satisfiable. Freshness keeps the chains independent.
Q2. Is the reduction many-one or Turing?
Many-one (mapping reduction). The function takes the CNF formula as input and returns the 3CNF formula as output. No oracle calls.
Q3. What is the size blow-up?
Linear. Total clause-literals stay within O(L). The constant is small — typically 3× for the worst case of all-unit clauses, which pad 1 literal into 12.
Q4. Does the reduction work for 4SAT or kSAT for k ≥ 4?
Yes — any kSAT for fixed k ≥ 3 is NP-complete, and the same chain trick reduces SAT to it (chains of width k instead of 3). Only 2SAT escapes (it's in P).
Q5. Why is 2SAT in P but 3SAT NP-complete?
2SAT can be decided by implication graphs and strongly-connected components in linear time. The jump at 3 happens because once you allow three literals, you have enough room to encode arbitrary Boolean constraints — Cook–Levin's tableau clauses are all 3-literal for exactly this reason.

🔊 Listen

9 · Where to read more

Sipser: §7.4, Theorem 7.32 (the canonical statement of this reduction). Lecture notes: Module 5, slide 4 (the NP-complete chain starting from SAT). MIT 18.404J Lecture 16 covers the same construction with a slightly different diagram.