The Tseitin transformation has linear size and preserves satisfiability

For each subformula $\theta$ of $\phi$, introduce the extension variable from [L1]. If $\theta$ is a literal $\mathrm{\ell }$, add $(\mathrm{\neg }{y}_{\theta }\vee \mathrm{\ell })$ and $(y_{\theta }\vee \mathrm{\neg }\mathrm{\ell })$. If $\theta =\alpha \wedge \beta$, add $(\mathrm{\neg }{y}_{\theta }\vee y_{\alpha })$, $(\mathrm{\neg }{y}_{\theta }\vee y_{\beta })$, and $(y_{\theta }\vee \mathrm{\neg }{y}_{\alpha }\vee \mathrm{\neg }{y}_{\beta })$. If $\theta =\alpha \vee \beta$, add $(y_{\theta }\vee \mathrm{\neg }{y}_{\alpha })$, $(y_{\theta }\vee \mathrm{\neg }{y}_{\beta })$, and $(\mathrm{\neg }{y}_{\theta }\vee y_{\alpha }\vee y_{\beta })$. If $\theta =\mathrm{\neg }\alpha$, add $(\mathrm{\neg }{y}_{\theta }\vee \mathrm{\neg }{y}_{\alpha })$ and $(y_{\theta }\vee y_{\alpha })$. If $\theta =\mathrm{\top }$ or $\theta =\mathrm{\perp }$, add the unit clause $(y_{\theta })$ or $(\mathrm{\neg }{y}_{\theta })$ respectively. Finally add the unit clause $(y_{\phi })$. Every clause has at most three literals.

Any satisfying assignment of $\phi$ extends to the new variables by setting each $y_{\theta }$ equal to the truth value of $\theta$ under that assignment. Then every local clause from step 1.1 is satisfied, including the negation and constant clauses, and $y_{\phi }=1$ because $\phi$ itself is true. So satisfiability of $\phi$ implies satisfiability of $T(\phi )$.

Conversely, suppose $T(\phi )$ is satisfiable. The clauses of step 1.1 force each $y_{\theta }$ to agree with the Boolean value prescribed by its immediate subformulas, and an induction on subformula complexity shows that every extension variable equals the value of its subformula under the restricted assignment to the original variables. Since the clause $(y_{\phi })$ is satisfied, the original formula $\phi$ is true.

Each subformula of $\phi$ contributes one fresh variable and only constantly many clauses, so the total size of $T(\phi )$ is linear in $\mathrm{\mid }\phi \mathrm{\mid }$. Together with steps 2.1 and 3.1, this proves the statement.