3SAT is NP-complete

For a clause $l_1\vee \cdots \vee l_m$ with $m>3$, use distinct fresh variables $y_1,\dots ,y_{m-3}$ and replace it by the clauses $l_1\vee l_2\vee y_1$, then $\mathrm{\neg }{y}_j\vee l_{j+2}\vee y_{j+1}$ for $1\le j\le m-4$, then $\mathrm{\neg }{y}_{m-3}\vee l_{m-1}\vee l_m$. All variables used for different clauses are distinct. Leave clauses of lengths zero, one, two and three unchanged.

If the original clause is true, set $y_j=1$ exactly when $l_1,\dots ,l_{j+1}$ are all false. The first clause holds by this definition. In a middle clause, either $y_j=0$, or the first $j+1$ literals are false and then either $l_{j+2}=1$ or $y_{j+1}=1$. In the last clause, either $y_{m-3}=0$ or the first $m-2$ literals are false, forcing one of the last two true. This explicitly extends every satisfying assignment.

If all original literals were false, the first new clause would force $y_1=1$, the middle clauses successively force every next $y_j=1$, and the last would be false. Therefore a satisfying extension implies the original clause is true. For $m=4$ there are no middle clauses and the same first/last argument applies. Separate fresh variables let the extensions be performed for all clauses simultaneously.

The replacement has $m-2$ clauses for a long clause. Summing lengths gives linear literal count; the encoded indices and a finite scan for unused indices give polynomial bit length and construction time. Malformed CNF strings map to the fixed CNF containing an empty clause. To reduce an arbitrary NP language, first use F2's CNF output and then this map; composition of two polynomial running-time bounds is polynomial, and the two membership equivalences compose. Membership in NP guesses one bit per distinct variable and evaluates clauses. Empty CNF remains satisfiable, and any retained empty clause makes both formulas unsatisfiable. Hence 3SAT is NP-complete.