Reduce SAT to 3SAT by clause splitting

Replace long CNF clauses by equisatisfiable triples using fresh variables, without exponential distributivity.

Problem

Describe a polynomial-time many-one reduction from CNF-SAT to 3SAT. Given a CNF formula that may contain clauses of arbitrary length, produce an equisatisfiable 3CNF formula. Handle clauses of length $1$ and $2$ as well as length at least $4$. Prove both directions and bound the output size.

Hint 1

Do not distribute an arbitrary Boolean formula into CNF; start from CNF and only split long clauses.

Hint 2

For a clause $(\ell_1\lor\ell_2\lor\cdots\lor\ell_t)$ with $t\ge4$, introduce fresh variables that chain overlapping triples.

Full solution

Assume the input is already in CNF (the Cook–Levin output, or a prior Tseitin conversion). Process each clause independently.

• Length $3$: keep the clause.
• Length $1$: replace $(\ell)$ by $(\ell\lor y\lor z)\land(\ell\lor y\lor\neg z)\land(\ell\lor\neg y\lor z)\land(\ell\lor\neg y\lor\neg z)$ for fresh $y,z$, or any fixed equisatisfiable padding that forces $\ell$ true. A shorter common padding uses two fresh variables and four triples as above.
• Length $2$: similarly pad with one fresh variable to four triples, or use a fixed library of constant-size gadgets.
• Length $t\ge4$: replace [ (\ell_1\lor\cdots\lor\ell_t) ] by [ (\ell_1\lor\ell_2\lor y_1)\land(\neg y_1\lor\ell_3\lor y_2)\land\cdots\land(\neg y_\lor\ell_\lor\ell_t) ] with fresh $y_1,\ldots,y_{t-3}$.

If the original clause is satisfied by some $\ell_i$, set the chain variables so each triple containing a false prefix is completed by a true $y_j$, and each remaining triple inherits a true literal. Conversely, if every triple is satisfied, some original $\ell_i$ must be true: otherwise the chain of $y$-implications forces a contradiction at the final triple. Fresh variables do not appear elsewhere, so assignments extend independently per clause.

The number of triples per clause is $O(t)$, and $\sum t$ is linear in the input length, so the output size and construction time are polynomial. The identity map on already-3CNF instances is a special case; claiming “return $x$ unchanged” for arbitrary SAT is incorrect because long clauses are not 3SAT instances.

Checkpoint

Equisatisfiability must be proved both ways for the splitting chain; padding short clauses must not introduce unintended satisfying assignments that leave $\ell$ false.

Common mistakes

• Using distributivity on a general formula, risking exponential blowup.
• Returning the input unchanged while claiming a reduction to 3SAT.
• Reusing the same fresh variable across unrelated clauses.

Provenance note

Original course-and-textbook-aligned synthesis of the standard SAT→3SAT normalization appearing in the reduction atlas. Assignment prompts that audit broken “identity” reductions (e.g. Semester A 2026 exercise 3) motivate the exercise but are not copied.

Sources and verification

• Sipser 3e, sec. 7.5
• Garey-Johnson LO-family formulations
• Catalog mapping: data/exercises.json; statements and solutions are independently written.

Open in the visualization gallery: SAT → 3SAT