[proofplan] We prove membership in $\mathrm{NP}$ by constructing an explicit deterministic polynomial-time verifier. The certificate for an encoded formula is a truth assignment to its variables. The verifier parses the formula, checks that the certificate has the correct length, evaluates the formula bottom-up along its parse tree, and accepts exactly when the resulting Boolean value is $1$. [/proofplan]

[step:Use truth assignments as polynomial-size certificates] Let $w \in \{0,1\}^*$ be an input string, and let $n := |w|$ be its length. If $w = \langle \varphi \rangle$ is the chosen binary encoding of a Boolean formula $\varphi$ over the fixed finite Boolean basis, define $m := |\operatorname{Var}(\varphi)|$. Since the encoding is fixed and each distinct variable occurring in $\varphi$ must occupy at least one symbol or token in the input, the number of distinct variables is bounded linearly by the input length. Hence there is a constant $C_0 > 0$, depending only on the fixed encoding convention, such that $m \leq C_0 n$. A certificate for $w$ is a binary string $c \in \{0,1\}^*$ intended to encode a map \begin{align*} a_c: \operatorname{Var}(\varphi) \to \{0,1\}. \end{align*} The verifier first checks that $c$ has the required length for assigning one Boolean value to each variable of $\varphi$. Thus every accepting certificate has length at most $C_0 n$, which is polynomial in the input length. [/step]

[step:Define the verifier by parsing and evaluating the formula]Define a deterministic verifier \begin{align*} V: \{0,1\}^* \times \{0,1\}^* \to \{0,1\} \end{align*} as follows. On input $(w,c)$, the verifier first attempts to parse $w$ as an encoded Boolean formula. If parsing fails, $V(w,c) := 0$. If parsing succeeds, write $w = \langle \varphi \rangle$ and let $T_\varphi$ be the parse tree of $\varphi$. Let $\mathcal{B}$ denote the fixed finite Boolean basis used by the encoding. For each connective $\beta \in \mathcal{B}$, let $r(\beta) \in \mathbb{N}$ denote its arity and let \begin{align*} \beta: \{0,1\}^{r(\beta)} \to \{0,1\} \end{align*} denote its fixed truth function. The verifier orders the variables in $\operatorname{Var}(\varphi)$ by the fixed ordering induced by the encoding, interprets $c$ as the corresponding assignment \begin{align*} a_c: \operatorname{Var}(\varphi) \to \{0,1\}, \end{align*} and rejects if $c$ does not encode exactly one Boolean value for every variable in $\operatorname{Var}(\varphi)$. The verifier then evaluates $T_\varphi$ from leaves to root. At a leaf labelled by a variable $x \in \operatorname{Var}(\varphi)$, it assigns the value $a_c(x)$. At an internal node labelled by a connective $\beta \in \mathcal{B}$ with children already assigned values $b_1, \dots, b_{r(\beta)} \in \{0,1\}$, it assigns the value $\beta(b_1, \dots, b_{r(\beta)})$. In particular, this covers the connectives $\neg$, $\wedge$, and $\vee$, and also any additional connectives in the fixed finite basis. Finally, if the root value is $1$, set $V(w,c) := 1$; otherwise set $V(w,c) := 0$.[/step]

[guided]The certificate should contain exactly the information needed to prove satisfiability: a proposed satisfying assignment. We therefore build the verifier \begin{align*} V: \{0,1\}^* \times \{0,1\}^* \to \{0,1\} \end{align*} so that its first input is the alleged formula encoding and its second input is the alleged assignment. On input $(w,c)$, the verifier first checks whether $w$ is the encoding of a well-formed Boolean formula. This parsing step is part of the fixed encoding convention, and the statement assumes the encoding is polynomial-time parseable. If $w$ is not well formed, then $w \notin \mathrm{SAT}$ by definition of the language, so the verifier sets $V(w,c) := 0$. Now suppose parsing succeeds, so $w = \langle \varphi \rangle$. Let $T_\varphi$ denote the parse tree of $\varphi$, and let $\mathcal{B}$ denote the fixed finite Boolean basis used by the encoding. The leaves of $T_\varphi$ are variables, and the internal nodes are labelled by connectives from $\mathcal{B}$. For each connective $\beta \in \mathcal{B}$, let $r(\beta) \in \mathbb{N}$ be its arity and let \begin{align*} \beta: \{0,1\}^{r(\beta)} \to \{0,1\} \end{align*} be its fixed truth function. This finite table of truth functions is part of the fixed language definition, so applying one connective to already computed child values takes constant time depending only on the basis. The certificate $c$ is interpreted using the fixed ordering of the variables in $\operatorname{Var}(\varphi)$ determined by the encoding. In this way, when $c$ has the correct length, it defines a map \begin{align*} a_c: \operatorname{Var}(\varphi) \to \{0,1\}. \end{align*} If $c$ does not contain exactly one bit for each variable of $\varphi$, then it does not encode a valid assignment, and the verifier rejects. Once the assignment has been decoded, the remaining task is deterministic evaluation of the formula. The verifier evaluates the parse tree bottom-up. A leaf labelled by a variable $x \in \operatorname{Var}(\varphi)$ receives the value $a_c(x)$. An internal node labelled by a connective $\beta \in \mathcal{B}$ receives the value $\beta(b_1, \dots, b_{r(\beta)})$, where $b_1, \dots, b_{r(\beta)} \in \{0,1\}$ are the already computed values of its child nodes in their encoded order. For the special connectives $\neg$, $\wedge$, and $\vee$, this is ordinary negation, conjunction, and disjunction; for any additional connective in the finite basis, this is its fixed truth-table operation. Because each internal node is evaluated only after its children have been evaluated, every assigned node value is exactly the Boolean value of the corresponding subformula under $a_c$. Therefore the value computed at the root is precisely $\operatorname{eval}_\varphi(a_c)$. The verifier accepts exactly when this root value is $1$.[/guided]

[step:Bound the verifier running time by a polynomial] Let $N_\varphi$ denote the number of nodes in the parse tree $T_\varphi$. Since $T_\varphi$ is obtained from the encoded formula, there is a constant $C_1 > 0$, depending only on the encoding, such that $N_\varphi \leq C_1 n$. Parsing the input takes polynomial time by the encoding hypothesis. Checking the certificate length takes time at most linear in $n + |c|$, and if the length is invalid the verifier rejects immediately. Evaluating the parse tree visits each node of $T_\varphi$ once and performs one constant-time Boolean operation at each internal node, where the constant depends only on the fixed finite basis, so this evaluation takes at most $C_2 N_\varphi$ elementary steps for some constant $C_2 > 0$. Hence $V$ runs in time polynomial in the combined input length $n + |c|$. Moreover, every accepting certificate satisfies $|c| \leq C_0 n$, so the certificate length is bounded by a polynomial $p: \mathbb{N} \to \mathbb{N}$ in the original input length, for example by choosing $p(n) = C n^2$ for a sufficiently large constant $C > 0$ depending only on the encoding and the computational model. [/step]

[step:Verify the acceptance condition exactly matches satisfiability] Suppose first that $w \in \mathrm{SAT}$. Then $w = \langle \varphi \rangle$ for a Boolean formula $\varphi$, and there exists an assignment \begin{align*} a: \operatorname{Var}(\varphi) \to \{0,1\} \end{align*} such that $\operatorname{eval}_\varphi(a) = 1$. Let $c_a \in \{0,1\}^*$ be the certificate encoding this assignment in the fixed variable order. By construction, $c_a$ has polynomial length, passes the verifier's length check, and causes the bottom-up evaluation to compute root value $1$. Hence $V(w,c_a) = 1$. Conversely, suppose there exists a certificate $c \in \{0,1\}^*$ such that $V(w,c) = 1$. Then the verifier must have successfully parsed $w$ as $w = \langle \varphi \rangle$, must have decoded $c$ as an assignment \begin{align*} a_c: \operatorname{Var}(\varphi) \to \{0,1\}, \end{align*} and must have computed $\operatorname{eval}_\varphi(a_c) = 1$. Therefore $\varphi$ is satisfiable, so $w \in \mathrm{SAT}$. Thus there is a deterministic polynomial-time verifier and polynomial-size certificates satisfying \begin{align*} w \in \mathrm{SAT} \iff \exists c \in \{0,1\}^* \text{ such that } |c| \leq p(|w|) \text{ and } V(w,c) = 1. \end{align*} This is precisely the verifier characterization of membership in $\mathrm{NP}$, and therefore $\mathrm{SAT} \in \mathrm{NP}$. [/step]