SAT ≤p 3SAT | Complexity Atlas

The construction

The splitting step (Algorithm 1). On a CNF formula $\varphi$ :

If $\varphi$ is already 3CNF — return it.
Otherwise let $C=\ell_1\vee\ell_2\vee\dots\vee\ell_k$ be the first clause with $k>3$ literals. Define $C'=\ell_1\vee\ell_2\vee z,\qquad C''=\ell_3\vee\dots\vee\ell_k\vee\bar z,$ where $z$ is a fresh variable not occurring in $\varphi$ .
Return $\hat\varphi$ , obtained from $\varphi$ by replacing $C$ with $C'\wedge C''$ .

The reduction. While $\varphi$ is not 3CNF, run the splitting step, choosing a new auxiliary variable each time; finally return $\varphi$ . An input that is not a valid CNF encoding is replaced by a fixed unsatisfiable 3CNF formula, e.g. $(y)\wedge(\bar y)$ .

Termination. A clause of length $k>3$ is replaced by clauses of lengths $3$ and $k-1$ , and clauses of length $\le3$ never change. So the quantity $\sum_{|C|>3}(|C|-3)$ drops by exactly $1$ per iteration and is a non-negative integer — the loop halts, and in the output every clause has length $\le3$ .

Visualization

Source clause(a ∨ b ∨ c ∨ d ∨ e)

Fresh variableOutput triple

Correctness — both directions

SAT ∈ ⟹ 3SAT ∈

It suffices to prove the single-step lemma — $\varphi$ satisfiable $\iff$ $\hat\varphi$ satisfiable — and then chain it by induction.

Suppose $\varphi$ is satisfiable, with satisfying assignment $v$ . In particular $v$ satisfies $C=\ell_1\vee\dots\vee\ell_k$ , so some $t$ has $v(\ell_t)=1$ . Extend $v$ to $z$ :

if $t\in\{1,2\}$ — set $v(z)=0$ . Then $C'=\ell_1\vee\ell_2\vee z$ is satisfied by $\ell_t$ , and $C''$ is satisfied by $\bar z$ .
otherwise $t\ge3$ — set $v(z)=1$ . Then $C'$ is satisfied by $z$ , and $C''$ by $\ell_t$ .

The other clauses are unchanged and do not contain $z$ , so they stay satisfied. Hence $\hat\varphi$ is satisfiable.

3SAT ∈ ⟹ SAT ∈

Suppose $\hat\varphi$ is satisfiable, with satisfying assignment $v$ . Restrict $v$ to the variables of $\varphi$ (forget the value it gave $z$ ) and check that it satisfies $\varphi$ .

Every clause of $\varphi$ other than $C$ appears unchanged in $\hat\varphi$ and does not contain $z$ , so it is satisfied. That leaves $C$ . Split on $v(z)$ :

if $v(z)=1$ : the clause $C''=\ell_3\vee\dots\vee\ell_k\vee\bar z$ is satisfied while $\bar z$ evaluates to $0$ , so some $t\ge3$ has $v(\ell_t)=1$ . That literal occurs in $C$ , so $C$ is satisfied.
if $v(z)=0$ : the clause $C'=\ell_1\vee\ell_2\vee z$ is satisfied while $z$ evaluates to $0$ , so $v(\ell_1)=1$ or $v(\ell_2)=1$ . Again a literal of $C$ , so $C$ is satisfied.

Either way $v$ satisfies $C$ , hence all of $\varphi$ .

Since the lemma holds at every step, induction along $\varphi_0=\varphi,\varphi_1,\dots,\varphi_m$ (the output) gives $\varphi$ satisfiable $\iff$ $\varphi_m$ satisfiable — that is, $\langle\varphi\rangle\in\mathrm{SAT}\iff\langle\varphi_m\rangle\in\mathrm{3SAT}$ .

Cost of the reduction

TimeO(|φ|²)

SpaceO(|φ|)

Output sizeO(|φ|) symbols, O(|φ| log |φ|) bits

The number of iterations is exactly $\sum_{|C|>3}(|C|-3)\le L\le|\varphi|$ , where $L$ counts literal occurrences. Each iteration adds exactly $2$ literal occurrences, so $L_{\text{final}}\le L+2L=3L$ — the formula does not blow up, it stays linear. A single iteration costs $O(|\varphi|)$ (scan and copy), for $O(|\varphi|^2)$ overall.

At the bit level: the reduction adds up to $L$ new variables and an index costs $O(\log L)$ bits, so the output is $O(|\varphi|\log|\varphi|)$ bits — still polynomial.

What it buys

With Cook–Levin ( $\mathrm{SAT}$ is NP-hard) and transitivity of $\le_p$ : every $A\in\mathrm{NP}$ satisfies $A\le_p\mathrm{SAT}\le_p\mathrm{3SAT}$ , so $\mathrm{3SAT}$ is NP-complete. From here on nearly every reduction in the course starts at $\mathrm{3SAT}$ rather than $\mathrm{SAT}$ — the rigid three-literals-per-clause shape is far easier to copy into graphs and sets.

Pitfalls

$C'\wedge C''$ is not equivalent to $C$ . It is only equisatisfiable: a satisfying $v$ for $C$ extends to $z$ so as to satisfy both, and conversely. Logical equivalence fails — an assignment giving $1$ to $\ell_1$ and $1$ to $z$ satisfies $C$ but not $C'\wedge C''$ .
$z$ must be fresh at every iteration. Reusing the same $z$ ties two different clauses through one variable, and extending the assignment in the forward direction may then demand $z=0$ and $z=1$ at once.
Do not split $C$ by distributivity. Turning a long CNF into a logically equivalent 3CNF blows the formula up exponentially. The auxiliary variable buys linear size at exactly the price of dropping logical equivalence.

The chain

Rests on

A ∈ NP ≤p SAT

Used later by

Where this was read from

Lesson 8משפט 6: $\mathrm{SAT} \le_p \mathrm{3SAT}$
Guided exercisesat-to-3sat-clause-splitting
2024 '1 מועד 1One clause of 6 literals — how many literals and how many variables the output holds.