[proofplan] Membership in NP is witnessed by a truth assignment and verified by evaluating the formula. For hardness, fix an arbitrary language $A \in \mathrm{NP}$ and encode the accepting computation of a nondeterministic polynomial-time Turing machine $M$ as a finite tableau. The Boolean formula has variables saying which tape/head-state marker occupies each tableau cell, and its constraints enforce uniqueness, the initial configuration, local transition correctness, and eventual acceptance. The local constraints have constant size because the transition function of $M$ sees only a bounded window, while the tableau has only polynomially many cells and times. [/proofplan]

[step:Verify that satisfiability has polynomial certificates] Let $\varphi$ be a Boolean formula, and let $V(\varphi)$ denote the finite set of variables occurring in $\varphi$. A certificate for $\varphi \in \mathrm{SAT}$ is a map \begin{align*} \sigma: V(\varphi) \to \{0,1\}. \end{align*} Given $\sigma$, one evaluates the parse tree of $\varphi$ from the leaves to the root, using the truth tables for $\neg$, $\wedge$, and $\vee$. This takes time polynomial in the length of $\varphi$. The formula is accepted exactly when the value at the root is $1$. Hence $\mathrm{SAT} \in \mathrm{NP}$. [/step]

[step:Choose a nondeterministic polynomial-time decider for the input language] Let $A \in \mathrm{NP}$. By the definition of $\mathrm{NP}$, there exist a nondeterministic Turing machine $M$ and a polynomial \begin{align*} p: \mathbb{N} \to \mathbb{N} \end{align*} such that $p(n) \ge n$ for every $n \in \mathbb{N}$ and, for every input $x \in \{0,1\}^*$, the machine $M$ halts on every computation branch within \begin{align*} T := p(|x|) \end{align*} steps, and $M$ accepts $x$ on at least one branch if and only if $x \in A$. If the polynomial obtained from the definition of $\mathrm{NP}$ does not satisfy $p(n) \ge n$, replace it by the polynomial $n \mapsto p(n)+n$. Let $\Gamma$ be the finite tape alphabet of $M$, let $Q$ be the finite set of states of $M$, let $q_0 \in Q$ be the start state, and let $F \subset Q$ be the set of accepting states. We assume, by replacing $M$ with an equivalent machine if needed, that once $M$ enters an accepting state it remains in an accepting state and leaves the tape unchanged. This modification changes the running time by at most a fixed polynomial factor, so the bound $T$ may be enlarged polynomially without changing the argument. Define the finite marker set \begin{align*} C := \Gamma \cup (Q \times \Gamma). \end{align*} A marker $a \in \Gamma$ means that a tape cell contains symbol $a$ and the head is not on that cell. A marker $(q,a) \in Q \times \Gamma$ means that the tape cell contains symbol $a$, the head is on that cell, and the machine is in state $q$. [/step]

[step:Introduce tableau variables for time and tape position] For the fixed input $x$, define the time index set \begin{align*} I_T := \{0,1,\dots,T\}. \end{align*} Define the tape index set \begin{align*} J_T := \{0,1,\dots,2T\}. \end{align*} We place the initial head at cell $T$. Since the head can move at most one cell per step, during the first $T$ steps it can visit only cells in $J_T$: after $s \le T$ steps its position lies between $T-s$ and $T+s$. Because $T \ge |x|$, the input cells $T,T+1,\dots,T+|x|-1$ also lie in $J_T$. For every $t \in I_T$, every $j \in J_T$, and every marker $c \in C$, introduce a Boolean variable $X_{t,j,c}$. The intended meaning is: \begin{align*} X_{t,j,c}=1 \iff \text{at time } t \text{ and tape cell } j \text{, the tableau marker is } c. \end{align*} [/step]

[step:Build constraints forcing each row to be a valid configuration]First impose exactly one marker in each tableau cell. For each pair $(t,j) \in I_T \times J_T$, include the formula \begin{align*} \bigvee_{c \in C} X_{t,j,c} \end{align*} and, for every two distinct markers $c,d \in C$, include \begin{align*} \neg X_{t,j,c} \vee \neg X_{t,j,d}. \end{align*} Next impose exactly one head-state marker in every row. For each $t \in I_T$, include \begin{align*} \bigvee_{j \in J_T}\bigvee_{q \in Q}\bigvee_{a \in \Gamma} X_{t,j,(q,a)}. \end{align*} For every $t \in I_T$, every two distinct cells $j,k \in J_T$, every $q,r \in Q$, and every $a,b \in \Gamma$, include \begin{align*} \neg X_{t,j,(q,a)} \vee \neg X_{t,k,(r,b)}. \end{align*} The first family guarantees that every cell receives a marker, the pairwise clauses guarantee uniqueness of the marker in each cell, and the head clauses guarantee that every row represents a configuration with one machine state and one head position.[/step]

[guided]The tableau is meant to describe a complete computation history. A computation history is not just an arbitrary array of symbols: every time row must be a genuine configuration of the Turing machine. That requires two uniqueness conditions. First, each individual cell must contain exactly one marker. For a fixed time $t \in I_T$ and cell $j \in J_T$, the disjunction \begin{align*} \bigvee_{c \in C} X_{t,j,c} \end{align*} says that at least one marker appears in that cell. The pairwise exclusions \begin{align*} \neg X_{t,j,c} \vee \neg X_{t,j,d} \end{align*} for distinct $c,d \in C$ say that two different markers cannot both appear there. Together these formulas say exactly one marker from $C$ occupies the cell. Second, each row must have exactly one head position and exactly one state. The variables of the form $X_{t,j,(q,a)}$ are precisely the variables saying that the head is at cell $j$, the state is $q$, and the scanned tape symbol is $a$. The disjunction \begin{align*} \bigvee_{j \in J_T}\bigvee_{q \in Q}\bigvee_{a \in \Gamma} X_{t,j,(q,a)} \end{align*} forces at least one head-state marker in row $t$. The exclusions \begin{align*} \neg X_{t,j,(q,a)} \vee \neg X_{t,k,(r,b)} \end{align*} for distinct cells $j,k \in J_T$ prevent two cells from both carrying head-state markers. Since every cell already has exactly one marker, this makes row $t$ a well-formed configuration: one state, one head position, and one tape symbol in every displayed cell.[/guided]

[step:Force the initial row to encode the input word] Write the input as \begin{align*} x = x_1x_2\cdots x_n \end{align*} with $n=|x|$ and each $x_i \in \{0,1\}$. Let $\blank \in \Gamma$ denote the blank tape symbol. The initial configuration places the head at cell $0$, starts in state $q_0$, writes $x_1,\dots,x_n$ in the first $n$ input cells according to the chosen machine convention, and writes blanks elsewhere. For each cell $j \in J_T$, include the unit clause selecting the corresponding initial marker. Concretely, if the initial head scans cell $T$ and cell $T+i-1$ contains the input symbol $x_i$ for $1 \le i \le n$, include \begin{align*} X_{0,T,(q_0,x_1)} \end{align*} when $n \ge 1$, include \begin{align*} X_{0,T+i-1,x_i} \end{align*} for $2 \le i \le n$, and include \begin{align*} X_{0,j,\blank} \end{align*} for every $j \in J_T \setminus \{T,T+1,\dots,T+n-1\}$. If $n=0$, replace the first clause by $X_{0,T,(q_0,\blank)}$ and include $X_{0,j,\blank}$ for every $j \in J_T \setminus \{T\}$. These clauses fix the entire first row to be the standard initial configuration of $M$ on $x$. [/step]

[step:Encode legal transitions by constant-size local windows] Define a two-row length-three window to be an element of $C^3 \times C^3$. Let \begin{align*} L_M \subset C^3 \times C^3 \end{align*} be the finite set of windows that can occur in three adjacent cells of two consecutive configurations related by one legal transition of $M$. Since $M$, $Q$, and $\Gamma$ are fixed independently of $x$, the set $L_M$ has constant size depending only on $M$. For each time $t \in \{0,\dots,T-1\}$, each center cell $j \in J_T$, each row index $s \in I_T$, each tape index $k \in \{j-1,j,j+1\}$, and each marker $c \in C$, define the literal or constant $Y_{s,k,c}$ as follows. If $k \in J_T$, set $Y_{s,k,c}:=X_{s,k,c}$. If $k \notin J_T$, set $Y_{s,k,\blank}:=1$ and set $Y_{s,k,c}:=0$ for every $c \in C \setminus \{\blank\}$. Thus missing boundary cells outside $J_T$ are interpreted as fixed blank cells. Include the formula asserting that the six markers in cells $j-1,j,j+1$ at times $t$ and $t+1$ form an element of $L_M$: \begin{align*} \bigvee_{((a_-,a_0,a_+),(b_-,b_0,b_+)) \in L_M} \Bigl(Y_{t,j-1,a_-} \wedge Y_{t,j,a_0} \wedge Y_{t,j+1,a_+} \wedge Y_{t+1,j-1,b_-} \wedge Y_{t+1,j,b_0} \wedge Y_{t+1,j+1,b_+}\Bigr). \end{align*} Because each row has exactly one head-state marker, there is a unique scanned cell and state in the row at time $t$. The window centered at that scanned cell selects one legal transition of $M$; the overlapping windows centered at the neighbouring cells force the written symbol, new state marker, and head displacement to agree with that same transition. Every window whose three cells do not include the scanned cell contains no head-state marker in its upper row, so membership in $L_M$ forces the corresponding lower-row tape symbols to remain unchanged. Hence a pair of consecutive rows is a legal transition of $M$ if and only if every adjacent two-row window belongs to $L_M$. [/step]

[step:Force acceptance in one of the tableau rows] Include the accepting formula \begin{align*} \bigvee_{t \in I_T}\bigvee_{j \in J_T}\bigvee_{q \in F}\bigvee_{a \in \Gamma} X_{t,j,(q,a)}. \end{align*} This formula says that at some time $t \le T$, the unique head-state marker is in an accepting state. [/step]

[step:Assemble the reduction and prove its size is polynomial] Let $\Phi_{M,x}$ be the conjunction of all formulas introduced above: cell uniqueness, unique head-state per row, initial configuration, local transition legality, and acceptance. The number of variables is \begin{align*} |I_T|\,|J_T|\,|C| = (T+1)(2T+1)|C|. \end{align*} Since $M$ is fixed, $|C|$ is constant with respect to $x$. The number of uniqueness clauses is bounded by a constant multiple of $(T+1)(2T+1)$, the number of head uniqueness clauses is bounded by a constant multiple of $(T+1)(2T+1)^2$, the number of local transition constraints is bounded by a constant multiple of $(T+1)(2T+1)$, and the accepting formula has size bounded by a constant multiple of $(T+1)(2T+1)$. Since $T=p(|x|)$, the length of $\Phi_{M,x}$ is bounded by a polynomial in $|x|$. The map \begin{align*} f: \{0,1\}^* \to \{\text{Boolean formulas}\}, \qquad x \mapsto \Phi_{M,x} \end{align*} is computable in polynomial time: for each polynomially many tableau location, it writes a fixed finite pattern of clauses determined by $M$, together with the input-dependent unit clauses specifying the first row. [/step]

[step:Show that the formula is satisfiable exactly for accepted inputs] Assume first that $x \in A$. Then $M$ has an accepting computation branch on $x$ of length at most $T$. Fill the tableau with the successive configurations on that branch, repeating the accepting configuration after acceptance if necessary. Assign $X_{t,j,c}=1$ exactly when marker $c$ is the actual marker at time $t$ and cell $j$, and assign all other tableau variables the value $0$. The uniqueness, initial, transition, and accepting constraints are satisfied by construction. Hence $\Phi_{M,x} \in \mathrm{SAT}$. Conversely, assume $\Phi_{M,x}$ is satisfiable, and let $\sigma$ be a satisfying truth assignment for its variables. The cell and head constraints extract from $\sigma$ a unique marker in every cell of every row and exactly one head-state marker in every row. The initial clauses make row $0$ the initial configuration of $M$ on $x$. The local transition clauses ensure that each row follows legally from the preceding row under one transition of $M$. The accepting clause gives a time $t \le T$ at which the unique state belongs to $F$. Therefore the extracted tableau is an accepting computation branch of $M$ on $x$, so $x \in A$. Thus, for every $x \in \{0,1\}^*$, \begin{align*} x \in A \iff \Phi_{M,x} \in \mathrm{SAT}. \end{align*} Since $A \in \mathrm{NP}$ was arbitrary, every language in $\mathrm{NP}$ polynomial-time many-one reduces to $\mathrm{SAT}$. Together with $\mathrm{SAT} \in \mathrm{NP}$, this proves that $\mathrm{SAT}$ is NP-complete. [/step]