Verifying a subtlety of Karp's original proof that SAT has a polynomial time reduction to 3SAT

Question

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.

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.