Complexity Atlas
HE
padding short clauses

3SAT ≤p 3SAT=

Let 3SAT=\mathrm{3SAT}^{=} be the variant in which every clause holds exactly three literals. Then 3SAT≤p3SAT=\mathrm{3SAT}\le_p\mathrm{3SAT}^{=}, so 3SAT=\mathrm{3SAT}^{=} is NP-complete too.

The construction

On a 3CNF formula φ\varphi, handle each clause by its length, with fresh variables y,y′y,y' per clause:

  • length 3: leave it alone.
  • length 2, C=ℓ1∨ℓ2C=\ell_1\vee\ell_2: replace with (ℓ1∨ℓ2∨y)∧(ℓ1∨ℓ2∨yˉ)(\ell_1\vee\ell_2\vee y)\wedge(\ell_1\vee\ell_2\vee\bar y).
  • length 1, C=ℓ1C=\ell_1: replace with (ℓ1∨y∨y′)∧(ℓ1∨y∨yˉ′)∧(ℓ1∨yˉ∨y′)∧(ℓ1∨yˉ∨yˉ′).(\ell_1\vee y\vee y')\wedge(\ell_1\vee y\vee\bar y')\wedge(\ell_1\vee\bar y\vee y')\wedge(\ell_1\vee\bar y\vee\bar y').

Visualization

Guided construction

3SAT → exactly-3SAT

Step 1 of 7
v: x₁ = F, x₂ = F, x₃ = T
Padding short clauses up to exactly three literalsThe three input clauses of lengths three, two and one are mapped to seven output clauses: the full clause is copied, the two-literal clause becomes two clauses using a fresh variable, and the unit clause becomes four clauses using two fresh variables.φ — input, at most 3 literalsf(φ) — output, exactly 3 literalsbuilt clause by clause|C₁| = 3 · keepC₁x₁∨¬x₂∨x₃|C₂| = 2 · pad with y₂C₂¬x₁∨x₂|C₃| = 1 · pad with y₃, y₃′C₃x₃
Literal of φ

Correctness — both directions

3SAT ∈ ⟹ 3SAT= ∈

Suppose vv satisfies φ\varphi. Extend vv to the auxiliary variables arbitrarily (say y=y′=0y=y'=0). Each original clause CC is satisfied by vv, i.e. it holds a literal ℓ\ell with v(ℓ)=1v(\ell)=1; that same ℓ\ell occurs in every clause replacing CC, so all of them are satisfied regardless of y,y′y,y'. So the output is satisfiable.

3SAT= ∈ ⟹ 3SAT ∈

Suppose vv satisfies the output, and restrict vv to the variables of φ\varphi. Let CC be a clause of φ\varphi; we show it is satisfied.

  • If ∣C∣=3|C|=3 it appears verbatim in the output, so it is satisfied.
  • If C=ℓ1∨ℓ2C=\ell_1\vee\ell_2: assume for contradiction v(ℓ1)=v(ℓ2)=0v(\ell_1)=v(\ell_2)=0. One of y,yˉy,\bar y evaluates to 00 under vv, so one of (ℓ1∨ℓ2∨y)(\ell_1\vee\ell_2\vee y), (ℓ1∨ℓ2∨yˉ)(\ell_1\vee\ell_2\vee\bar y) is unsatisfied — contradiction.
  • If C=ℓ1C=\ell_1: assume for contradiction v(ℓ1)=0v(\ell_1)=0. The pair (v(y),v(y′))(v(y),v(y')) is one of four combinations, and for each combination exactly one of the four clauses has both auxiliary literals evaluating to 00; that clause is unsatisfied — contradiction.

So vv satisfies every clause of φ\varphi, i.e. φ\varphi is satisfiable.

Cost of the reduction

TimeO(|φ|)
SpaceO(|φ|)
Output size≤ 4|φ|

A single pass over the clauses. The output grows by a factor of at most 44, in the extreme case where every clause has length 11.

What it buys

The two definitions of 3SAT — "at most three" and "exactly three" — are equivalent under ≤p\le_p, so the normalization "exactly three distinct literals per clause" costs no generality. The reductions 3NAE≤pMAXCUT\mathrm{3NAE}\le_p\mathrm{MAXCUT} and 3NAE≤p3COL\mathrm{3NAE}\le_p\mathrm{3COL} rely on it.

Pitfalls

  • The auxiliary variables must be fresh per clause. If one yy served two clauses the ⇐\Leftarrow direction would break: the argument "one of y,yˉy,\bar y evaluates to 00" turns into an uncontrolled dependency between clauses.

The chain

Where this was read from

  • Lesson 8משפט 7 (השלמה): הווריאנט "בדיוק 3 ליטרלים"

  • The lesson states explicitly that this claim is in neither the written summary nor the recording — it was added to the lesson file as a completion, because the "exactly three" definition is common in the literature and because it justifies the normalization used in lesson 10.