11.7

Reduction idea
Given a CNF formula F = C₁ ∧ … ∧ C_m where every clause C_i contains any number of literals, we replace each clause independently so that every new clause has exactly three literals while keeping the whole formula equi-satisfiable. Fresh auxiliary variables z₁, z₂, … are introduced on demand.

Per-clause transformation (k = number of literals in the clause)
1. k = 1, clause (ℓ₁) :
    Replace by  (ℓ₁ ∨ a ∨ ¬a)  using one fresh variable a.

2. k = 2, clause (ℓ₁ ∨ ℓ₂) :
    Replace by the pair
    (ℓ₁ ∨ ℓ₂ ∨ a) ∧ (ℓ₁ ∨ ℓ₂ ∨ ¬a).

3. k = 3 : keep the clause unchanged.

4. k > 3, clause (ℓ₁ ∨ … ∨ ℓ_k) :
    Create k − 3 fresh variables z₁, …, z_k-3 and output the chain
    (ℓ₁ ∨ ℓ₂ ∨ z₁) ∧ (¬z₁ ∨ ℓ₃ ∨ z₂) ∧ … ∧ (¬z_k-4 ∨ ℓ_k-1 ∨ ℓ_k).
    Intuition: z_i passes the “responsibility” of satisfying the big clause down the chain; the construction is satisfiable iff at least one original literal is true.

Correctness sketch
• If the original clause is satisfied by some ℓ_j, set every auxiliary variable occurring before ℓ_j to false and those after it arbitrarily; every new 3-clause holds.
• Conversely, if all new 3-clauses hold, propagating their truth values shows that at least one ℓ_j must be true, hence the original clause is satisfied.
Applying the argument clause–by–clause proves F is satisfiable ⇔ its 3-CNF image is satisfiable.

Reference implementation (Python)

def sat_to_3sat(cnf): """Convert a CNF (list of lists of signed ints) into 3-CNF.""" new_cnf, fresh = [], max(abs(l) for cls in cnf for l in cls) + 1 for cls in cnf: k = len(cls) if k == 1: a = fresh; fresh += 1 new_cnf.append([cls[0], a, -a]) elif k == 2: a = fresh; fresh += 1 new_cnf.append([cls[0], cls[1], a]) new_cnf.append([cls[0], cls[1], -a]) elif k == 3: new_cnf.append(cls) else: # k > 3 lits = list(cls) z_prev = None for i in range(k - 3): z = fresh; fresh += 1 if i == 0: new_cnf.append([lits[0], lits[1], z]) else: new_cnf.append([-z_prev, lits[i+1], z]) z_prev = z # last clause closes the chain new_cnf.append([-z_prev, lits[-2], lits[-1]]) return new_cnf

The procedure introduces ≤ max(1, k − 3) auxiliaries per original clause, keeps the total size linear, and runs in O(|F|) time.

Hence, we obtain an efficient, size-preserving SAT → 3-SAT reduction that proves 3-SAT is NP-complete.

Back to Chapter 11