[proofplan] We first verify that $\mathrm{CNF\text{-}SAT}$ lies in NP by using a truth assignment as a certificate and checking every clause directly. For NP-hardness, we reduce the general satisfiability problem $\mathrm{SAT}$ to $\mathrm{CNF\text{-}SAT}$ by the Tseitin transformation. The transformation introduces one fresh variable for each subformula occurrence and adds constant-size CNF constraints forcing each fresh variable to represent the truth value of its subformula. The final unit clause forces the variable corresponding to the whole formula to be true, giving an equisatisfiable CNF formula of linear size. [/proofplan] [step:Verify membership in NP by checking a proposed assignment clause by clause] Let $\Phi$ be a CNF formula with variables $x_1,\dots,x_n$ and clauses $C_1,\dots,C_m$. A certificate for $\Phi \in \mathrm{CNF\text{-}SAT}$ is a truth assignment \begin{align*} a:\{x_1,\dots,x_n\}\to \{0,1\}. \end{align*} For each clause $C_j$, the verifier evaluates each literal appearing in $C_j$ under $a$ and accepts precisely when at least one literal in every clause evaluates to $1$. The number of literal evaluations is bounded by the length of the input encoding of $\Phi$, so this verification runs in polynomial time. Hence $\mathrm{CNF\text{-}SAT}\in \mathrm{NP}$. [guided] To show that a language is in NP, we must describe a certificate whose validity can be checked in polynomial time. For a CNF formula, the natural certificate is a proposed satisfying assignment. Thus, for a CNF formula $\Phi$ with variables $x_1,\dots,x_n$, let \begin{align*} a:\{x_1,\dots,x_n\}\to \{0,1\} \end{align*} be the proposed assignment. Write the clauses of $\Phi$ as $C_1,\dots,C_m$. The verifier checks each clause $C_j$ separately. A positive literal $x_i$ evaluates to $a(x_i)$, and a negative literal $\neg x_i$ evaluates to $1-a(x_i)$. The clause $C_j$ is satisfied exactly when at least one of its literals evaluates to $1$. The whole CNF formula is satisfied exactly when every clause passes this test. The running time is polynomial because each literal in the input is inspected a constant number of times. Therefore the verifier runs in time bounded by a polynomial in the input length of $\Phi$. This proves $\mathrm{CNF\text{-}SAT}\in \mathrm{NP}$. [/guided] [/step] [step:Construct a linear-size CNF formula from an arbitrary Boolean formula] Let $\mathrm{SAT}$ denote the language of satisfiable Boolean formulas over the connectives $\neg$, $\wedge$, and $\vee$: \begin{align*} \mathrm{SAT}:=\{\varphi : \varphi\text{ is a satisfiable Boolean formula over }\neg,\wedge,\vee\}. \end{align*} We use the NP-completeness of $\mathrm{SAT}$, given by the Cook-Levin Theorem, as the starting point of the hardness reduction. Let $\varphi$ be a Boolean formula built from variables using $\neg$, $\wedge$, and $\vee$. For each subformula occurrence $\psi$ of $\varphi$, introduce a fresh Boolean variable $y_\psi$. Define a transformation \begin{align*} T:\{\text{Boolean formulas over } \neg,\wedge,\vee\}\to \{\text{CNF formulas}\} \end{align*} as follows. For each variable occurrence $\psi=x_i$, add the two clauses encoding $y_\psi\leftrightarrow x_i$: \begin{align*} (\neg y_\psi\vee x_i)\wedge (y_\psi\vee \neg x_i). \end{align*} For each negation occurrence $\psi=\neg\alpha$, add the two clauses encoding $y_\psi\leftrightarrow \neg y_\alpha$: \begin{align*} (\neg y_\psi\vee \neg y_\alpha)\wedge (y_\psi\vee y_\alpha). \end{align*} For each conjunction occurrence $\psi=\alpha\wedge\beta$, add the three clauses encoding $y_\psi\leftrightarrow (y_\alpha\wedge y_\beta)$: \begin{align*} (\neg y_\psi\vee y_\alpha)\wedge(\neg y_\psi\vee y_\beta)\wedge(y_\psi\vee\neg y_\alpha\vee\neg y_\beta). \end{align*} For each disjunction occurrence $\psi=\alpha\vee\beta$, add the three clauses encoding $y_\psi\leftrightarrow (y_\alpha\vee y_\beta)$: \begin{align*} (\neg y_\psi\vee y_\alpha\vee y_\beta)\wedge(y_\psi\vee\neg y_\alpha)\wedge(y_\psi\vee\neg y_\beta). \end{align*} Finally add the unit clause $y_\varphi$. Let $T(\varphi)$ be the conjunction of all these clauses. This is a CNF formula, and the number of clauses is at most three times the number of subformula occurrences plus one. Therefore $\varphi\mapsto T(\varphi)$ is computable in polynomial time and has output size linear in the size of $\varphi$. [/step] [step:Prove that the Tseitin constraints preserve satisfiability] Suppose first that $\varphi$ is satisfiable, and let \begin{align*} a:\{\text{variables of }\varphi\}\to\{0,1\} \end{align*} be a satisfying assignment. Extend $a$ to the variables of $T(\varphi)$ by defining $a(y_\psi)$ to be the truth value of the subformula occurrence $\psi$ under the original assignment. Each group of clauses was chosen to be exactly the truth-table encoding of the corresponding equivalence, so all Tseitin clauses are satisfied. Since $a(y_\varphi)=1$, the unit clause $y_\varphi$ is also satisfied. Hence $T(\varphi)$ is satisfiable. Conversely, suppose $T(\varphi)$ is satisfiable, and let \begin{align*} b:\{\text{variables of }T(\varphi)\}\to\{0,1\} \end{align*} be a satisfying assignment. The clauses attached to each subformula occurrence force $b(y_\psi)$ to equal the truth value of $\psi$ under the restriction of $b$ to the original variables of $\varphi$. This is proved by induction on the formation of $\psi$: the variable case is forced by $y_\psi\leftrightarrow x_i$, and the negation, conjunction, and disjunction cases are forced by their corresponding equivalence clauses. Since the unit clause $y_\varphi$ is present, $b(y_\varphi)=1$. Therefore $\varphi$ evaluates to true under the restricted assignment, so $\varphi$ is satisfiable. [guided] The point of the construction is not that $T(\varphi)$ is logically equivalent to $\varphi$ using the same variables. It uses extra variables. What we need is the weaker and correct property: $\varphi$ is satisfiable if and only if $T(\varphi)$ is satisfiable. Assume first that $\varphi$ is satisfiable. Choose a satisfying assignment \begin{align*} a:\{\text{variables of }\varphi\}\to\{0,1\}. \end{align*} We extend this assignment to every new variable $y_\psi$ by setting $a(y_\psi)$ equal to the truth value of the subformula occurrence $\psi$ under the original assignment. With this definition, each equivalence $y_\psi\leftrightarrow x_i$, $y_\psi\leftrightarrow \neg y_\alpha$, $y_\psi\leftrightarrow (y_\alpha\wedge y_\beta)$, or $y_\psi\leftrightarrow (y_\alpha\vee y_\beta)$ holds by construction. The clauses we inserted are precisely the CNF truth-table encodings of these equivalences, so every inserted clause is satisfied. Since $\varphi$ itself is true under $a$, the variable $y_\varphi$ is assigned value $1$, and the final unit clause $y_\varphi$ is satisfied. Thus $T(\varphi)$ is satisfiable. For the converse, suppose $T(\varphi)$ has a satisfying assignment \begin{align*} b:\{\text{variables of }T(\varphi)\}\to\{0,1\}. \end{align*} Restrict $b$ to the original variables of $\varphi$. We prove by structural induction on subformula occurrences $\psi$ that $b(y_\psi)$ is the truth value of $\psi$ under this restricted assignment. If $\psi=x_i$, the two clauses $(\neg y_\psi\vee x_i)$ and $(y_\psi\vee\neg x_i)$ force $b(y_\psi)=b(x_i)$. If $\psi=\neg\alpha$, the two clauses $(\neg y_\psi\vee\neg y_\alpha)$ and $(y_\psi\vee y_\alpha)$ force $b(y_\psi)=1-b(y_\alpha)$. If $\psi=\alpha\wedge\beta$, the three conjunction clauses force $b(y_\psi)=1$ exactly when both $b(y_\alpha)=1$ and $b(y_\beta)=1$. If $\psi=\alpha\vee\beta$, the three disjunction clauses force $b(y_\psi)=1$ exactly when at least one of $b(y_\alpha)$ and $b(y_\beta)$ equals $1$. These are exactly the Boolean semantics of variables, negation, conjunction, and disjunction. Applying the induction statement to the top formula $\varphi$, the value $b(y_\varphi)$ equals the truth value of $\varphi$ under the restricted assignment. But $T(\varphi)$ contains the unit clause $y_\varphi$, so every satisfying assignment of $T(\varphi)$ has $b(y_\varphi)=1$. Therefore $\varphi$ is true under the restricted assignment. Hence $\varphi$ is satisfiable. [/guided] [/step] [step:Conclude NP-hardness and combine with membership in NP] The previous steps give a polynomial-time many-one reduction \begin{align*} \varphi\in \mathrm{SAT}\iff T(\varphi)\in \mathrm{CNF\text{-}SAT}. \end{align*} Since $\mathrm{SAT}$ is NP-complete by the Cook-Levin Theorem and $\mathrm{SAT}$ has been defined as the language of satisfiable Boolean formulas, every language in NP reduces in polynomial time to $\mathrm{SAT}$ and then to $\mathrm{CNF\text{-}SAT}$. Thus $\mathrm{CNF\text{-}SAT}$ is NP-hard. Together with $\mathrm{CNF\text{-}SAT}\in\mathrm{NP}$, this proves that $\mathrm{CNF\text{-}SAT}$ is NP-complete. [/step]