Stated briefly, my question is: is Karp's original proof reducing SAT to 3SAT unnecessarily elaborate? The details are as follows.

In his 1972 paper Reducibility Among Combinatorial Problems, Karp proved that SAT reduces to 3SAT by stating:

Replace a clause $\sigma_1 \cup \sigma_2 \cup \ldots \cup \sigma_m$, where the $\sigma_i$ are literals and $m>3$, by $$ (\sigma_1 \cup \sigma_2 \cup u_1) (\sigma_3 \cup \ldots \cup \sigma_m \cup \bar{u}_1) (\bar{\sigma}_3 \cup u_1) \ldots (\bar{\sigma}_m \cup u_1), $$ where $u_1$ is a new variable. Repeat this transformation until no clause has more than three literals.

It seems to me that the final $m-2$ clauses (i.e. the clauses containing two literals) here are unnecessary. So, the construction is correct as written but it is more elaborate than necessary. Without the 2-literal clauses, we obtain the construction usually given in undergraduate textbooks. Is this correct, or am I missing something obvious? I feel extremely unsure of myself suggesting that anything done by Karp could be expressed more elegantly.


1 Answer 1


The conjunction of the first two clauses, $(\sigma_1\cup\sigma_2\cup u_1)(\sigma_3\cup\ldots\cup\sigma_m\cup\bar{u}_1)$ is equisatisfiable to the original clause, as can be easily checked (any valuation satisfying one of the $\sigma_i$ also satisfies one of the two new clauses, and can be extended to $u_1$ as needed to satisfy the other; any valuation satisfying both new clauses has to satisfy some $\sigma_i$, since it cannot satisfy both $u_1$ and $\bar{u}_1$.)

The additional clauses ensure that $u_1$ is in fact equivalent to $\sigma_3\cup\ldots\cup\sigma_m$, but as far as I can see, Karp does not actually use this. He credits Cook's 1971 paper for this particular reduction, but the version found there (actually for DNF tautologies rather than CNF satisfiability) does not feature these extra constraints.

  • $\begingroup$ Thanks for the helpful answer. Rephrasing to amplify and check my understanding, another way of stating this is that the extra clauses ensure this is a reduction from #SAT to #3SAT (since they preserve the number of solutions and not just the existence of solutions). $\endgroup$ Commented Mar 15, 2016 at 14:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.