Cook's classes $\mathbf{P}$, $\mathbf{NP}$, $\mathbf{E}$, p-reducibility, $\mathbf{NP}$-completeness, and the languages SAT and 3-SAT over $\{0,1\}$

Str

$\mathrm{Str}$ is an abbreviation for the type of finite lists of Booleans, i.e. finite bit strings $w = (w_1,\dots,w_n)$ with each $w_i \in \{\mathsf{false},\mathsf{true}\}$, including the empty string $[\,]$ of length $0$. Its length is written $|w|$. (Everywhere below, a "language over $\{\mathsf{false},\mathsf{true}\}$" means an arbitrary subset $L \subseteq \mathrm{Str}$; membership $w \in L$ is plain set membership, and no decidability or definability of $L$ is assumed.)

PolyTimeDecider

For a total function $\chi : \mathrm{Str} \to \{\mathsf{false},\mathsf{true}\}$, $\mathrm{PolyTimeDecider}(\chi)$ is the proposition that there exists at least one "polynomial-time machine computing $\chi$" in the following exact sense (Mathlib's TM2ComputableInPolyTime with input encoding the identity on bit strings and output encoding $b \mapsto [b]$). A machine is a bundled multi-stack machine (Mathlib's TM2 model, FinTM2) consisting of: a finite index set $K$ of stacks (with decidable equality); two distinguished indices $k_0 \in K$ (input stack) and $k_1 \in K$ (output stack), which are allowed to coincide; for each $k \in K$ a type $\Gamma_k$ of stack symbols, where only $\Gamma_{k_0}$ is required to be finite; a finite set $\Lambda$ of program labels with a distinguished label $\mathrm{main}$; a finite set $\Sigma$ of internal states with a distinguished initial state $s_0$; and a program $m$ assigning to every label $\ell \in \Lambda$ a statement $m(\ell)$. A statement is a finite tree built from the constructors: push onto stack $k$ the symbol $g(v)$, where $g : \Sigma \to \Gamma_k$ is an arbitrary function of the current internal state $v$, then continue with a sub-statement; peek at the top symbol of stack $k$ (or "empty") and replace the internal state by $g(v,\text{top})$ for an arbitrary function $g : \Sigma \times (\Gamma_k \cup \{\text{empty}\}) \to \Sigma$, then continue; pop, which is peek followed by removal of the top symbol of stack $k$ (popping an empty stack leaves it empty), then continue; load, replacing the internal state by $g(v)$ for an arbitrary $g : \Sigma \to \Sigma$, then continue; branch between two sub-statements according to an arbitrary predicate $\Sigma \to \{\mathsf{false},\mathsf{true}\}$ of the internal state; goto, which sets the current label to $g(v)$ for an arbitrary $g : \Sigma \to \Lambda$ and ends the statement; and halt, which sets the current label to "none" and ends the statement. A configuration is a triple (current label, which is either some $\ell \in \Lambda$ or "none"; current internal state $v \in \Sigma$; the contents of every stack $k \in K$ as a finite list over $\Gamma_k$ whose first entry is the top of the stack). One step of the machine from a configuration with label $\ell$ executes the whole statement $m(\ell)$ down to its terminating goto or halt (however many pushes, pops, peeks, loads and branches that statement contains) and returns the resulting configuration; a configuration with label "none" has no successor. Time is the number of steps in this sense. The initial configuration on an input list $u$ over $\Gamma_{k_0}$ has label $\mathrm{main}$, internal state $s_0$, stack $k_0$ equal to $u$ (first symbol of $u$ on top), and every other stack empty. The halting configuration for an output list $o$ over $\Gamma_{k_1}$ has label "none", internal state equal to the initial state $s_0$, stack $k_1$ equal to $o$ (first symbol on top), and every other stack empty (in particular, if $k_0 \neq k_1$ the input stack must have been emptied). Now $\mathrm{PolyTimeDecider}(\chi)$ asserts the existence of: such a machine $M$; a bijection $\iota : \Gamma_{k_0} \cong \{\mathsf{false},\mathsf{true}\}$ (so the input alphabet has exactly two symbols); a bijection $\omega : \Gamma_{k_1} \cong \{\mathsf{false},\mathsf{true}\}$; a polynomial $p \in \mathbb{N}[X]$ with natural-number coefficients; and, for every bit string $w \in \mathrm{Str}$, a natural number $s$ with

$$s \le p(|w|)$$

such that iterating the step function exactly $s$ times from the initial configuration on input $\iota^{-1}(w)$ (the string $w$ transported symbolwise into $\Gamma_{k_0}$) yields exactly the halting configuration whose output stack is the one-symbol list $[\omega^{-1}(\chi(w))]$; here iteration is understood so that once a configuration has no successor all later iterates are "no configuration", so the requirement says that the machine is not yet halted before step $s$ and at step $s$ is in precisely that halting configuration (label none, state $s_0$, stack $k_1 = [\omega^{-1}(\chi(w))]$, all other stacks empty). Since the initial configuration has a label and the halting one has none, necessarily $s \ge 1$. No computability restriction is placed on the functions $g$ inside statements beyond the finiteness of $\Sigma$, $\Lambda$ and $\Gamma_{k_0}$; stacks other than $k_0$ may have infinite symbol types.

P

$\mathrm{P}$ is the set of languages $L \subseteq \mathrm{Str}$ over $\{\mathsf{false},\mathsf{true}\}$ for which there exists a total function $\chi : \mathrm{Str} \to \{\mathsf{false},\mathsf{true}\}$ such that (i) $\mathrm{PolyTimeDecider}(\chi)$ holds, i.e. there exists a bundled multi-stack machine in Mathlib's TM2 model (finitely many stacks; finite input-stack alphabet in bijection with $\{\mathsf{false},\mathsf{true}\}$; output-stack alphabet in bijection with $\{\mathsf{false},\mathsf{true}\}$; finitely many labels and internal states; one step = full execution of one labelled statement, made of arbitrarily many push/pop/peek/load/branch operations ending in a goto or halt) together with a polynomial $p \in \mathbb{N}[X]$ such that for every $w \in \mathrm{Str}$, started with $w$ on the input stack (first symbol on top), initial internal state, all other stacks empty, and label $\mathrm{main}$, the machine reaches after exactly some $s \le p(|w|)$ steps the configuration with label "none", internal state equal to the initial state, output stack exactly the one-symbol list $[\chi(w)]$ (transported through the alphabet bijection), and all other stacks empty; and (ii) for every $w \in \mathrm{Str}$,

$$w \in L \iff \chi(w) = \mathsf{true}.$$

So $L$ is exactly the set of strings on which $\chi$ outputs $\mathsf{true}$; nothing is asserted about $L$ beyond the existence of such a $\chi$ and such a machine.

encodePair

For a pair $(x, y)$ of bit strings, $\mathrm{encodePair}(x,y)$ is the list over the four-element alphabet $\{\mathsf{false},\mathsf{true}\} \sqcup \{\mathsf{false},\mathsf{true}\}$ (disjoint union, with left and right copies) obtained by tagging every symbol of $x$ as a left-copy symbol, every symbol of $y$ as a right-copy symbol, and concatenating:

$$\mathrm{encodePair}(x,y) = (\mathrm{inl}\,x_1,\dots,\mathrm{inl}\,x_{|x|},\ \mathrm{inr}\,y_1,\dots,\mathrm{inr}\,y_{|y|}).$$

Its length is $|x| + |y|$; either component may be empty.

PolyTimeChecker

For a total function $R : \mathrm{Str} \times \mathrm{Str} \to \{\mathsf{false},\mathsf{true}\}$, $\mathrm{PolyTimeChecker}(R)$ is the proposition that there exists at least one machine computing $R$ in polynomial time in the following exact sense (Mathlib's TM2ComputableInPolyTime with input encoding $\mathrm{encodePair}$ and output encoding $b \mapsto [b]$). The machine model is Mathlib's bundled TM2 multi-stack machine: a finite index set $K$ of stacks (decidable equality), distinguished input index $k_0$ and output index $k_1$ (possibly equal), a symbol type $\Gamma_k$ for each stack with only $\Gamma_{k_0}$ required finite, a finite label set $\Lambda$ with distinguished label $\mathrm{main}$, a finite internal-state set $\Sigma$ with initial state $s_0$, and a program $m : \Lambda \to \text{statements}$, where a statement is a finite tree of push (push $g(v)$ onto a chosen stack, $g : \Sigma \to \Gamma_k$ arbitrary), peek (update the state by an arbitrary function of the state and the top symbol-or-empty), pop (peek and then remove the top; popping an empty stack is a no-op on the stack), load (arbitrary state update), branch (on an arbitrary predicate of the state), ending in goto (set label to an arbitrary function of the state) or halt (set label to "none"). A configuration is (label or none, internal state, contents of all stacks as lists with head = top); one step executes the entire statement of the current label; a configuration with label none has no successor; time is the number of steps. $\mathrm{PolyTimeChecker}(R)$ asserts the existence of such a machine, a bijection $\iota : \Gamma_{k_0} \cong \{\mathsf{false},\mathsf{true}\} \sqcup \{\mathsf{false},\mathsf{true}\}$ (so the input alphabet has exactly four symbols), a bijection $\omega : \Gamma_{k_1} \cong \{\mathsf{false},\mathsf{true}\}$, a polynomial $p \in \mathbb{N}[X]$ with natural-number coefficients, and for every pair $(x,y) \in \mathrm{Str} \times \mathrm{Str}$ a natural number $s$ with

$$s \le p(|x| + |y|)$$

such that, starting from the configuration with label $\mathrm{main}$, internal state $s_0$, stack $k_0$ holding $\iota^{-1}(\mathrm{encodePair}(x,y))$ (the left-tagged symbols of $x$ followed by the right-tagged symbols of $y$, first symbol on top) and all other stacks empty, exactly $s$ iterations of the step function lead to precisely the configuration with label "none", internal state $s_0$ (the initial state again), stack $k_1$ equal to the one-symbol list $[\omega^{-1}(R(x,y))]$, and every other stack empty (iterates past a halted configuration count as "no configuration", so the machine must halt exactly at step $s$ in exactly that configuration). Note that the time bound is a polynomial in the combined length $|x|+|y|$, not in $|x|$ alone.

NP

$\mathrm{NP}$ is the set of languages $L \subseteq \mathrm{Str}$ over $\{\mathsf{false},\mathsf{true}\}$ for which there exist a total function $R : \mathrm{Str} \times \mathrm{Str} \to \{\mathsf{false},\mathsf{true}\}$ and a natural number $k \in \mathbb{N}$ (with $k = 0$ allowed) such that (i) $\mathrm{PolyTimeChecker}(R)$ holds, i.e. there is a bundled TM2 multi-stack machine (finitely many stacks, finite input alphabet in bijection with the four-element set $\{\mathsf{false},\mathsf{true}\}\sqcup\{\mathsf{false},\mathsf{true}\}$, output alphabet in bijection with $\{\mathsf{false},\mathsf{true}\}$, finitely many labels and internal states, one step = complete execution of one labelled statement) and a polynomial $p \in \mathbb{N}[X]$ such that for every $(x,y)$, started with the tagged concatenation $\mathrm{encodePair}(x,y)$ on the input stack, initial state, other stacks empty, label $\mathrm{main}$, the machine halts after exactly some $s \le p(|x|+|y|)$ steps in the configuration with label none, internal state equal to the initial state, output stack exactly $[R(x,y)]$ (through the alphabet bijection) and all other stacks empty; and (ii) for every $w \in \mathrm{Str}$,

$$w \in L \iff \exists\, y \in \mathrm{Str}:\ |y| \le |w|^{k} \ \text{ and }\ R(w,y) = \mathsf{true}.$$

Here $|w|^k$ is natural-number exponentiation with the convention $n^0 = 1$ for all $n$ (including $0^0 = 1$); thus for $k = 0$ the certificate $y$ must have length at most $1$, and for $k \ge 1$ and $w = [\,]$ the only admissible certificate is $y = [\,]$. The bound on $|y|$ is $\le$, and $y$ ranges over all bit strings of that length or shorter.

PolyTimeComputable

For a total function $f : \mathrm{Str} \to \mathrm{Str}$, $\mathrm{PolyTimeComputable}(f)$ is the proposition that there exists at least one machine computing $f$ in polynomial time in the following exact sense (Mathlib's TM2ComputableInPolyTime with both input and output encodings the identity on bit strings). The machine is a bundled TM2 multi-stack machine: a finite index set $K$ of stacks (decidable equality), input index $k_0$ and output index $k_1$ (possibly equal), symbol types $\Gamma_k$ with only $\Gamma_{k_0}$ required finite, a finite label set $\Lambda$ with distinguished $\mathrm{main}$, a finite state set $\Sigma$ with initial state $s_0$, and a program $m$ assigning to each label a statement, i.e. a finite tree of push/peek/pop/load/branch operations (each driven by arbitrary functions of the finite internal state and, for peek/pop, of the top symbol-or-empty of the chosen stack; popping an empty stack leaves it empty) terminated by goto (label becomes an arbitrary function of the state) or halt (label becomes "none"). A configuration is (label or none, state, all stack contents as lists with head = top); one step executes the whole statement of the current label; halted configurations (label none) have no successor; time is the number of steps. $\mathrm{PolyTimeComputable}(f)$ asserts the existence of such a machine, bijections $\iota : \Gamma_{k_0} \cong \{\mathsf{false},\mathsf{true}\}$ and $\omega : \Gamma_{k_1} \cong \{\mathsf{false},\mathsf{true}\}$, a polynomial $p \in \mathbb{N}[X]$ with natural-number coefficients, and for every $x \in \mathrm{Str}$ a natural number $s$ with

$$s \le p(|x|)$$

such that from the initial configuration (label $\mathrm{main}$, state $s_0$, stack $k_0 = \iota^{-1}(x)$ with the first symbol of $x$ on top, all other stacks empty) exactly $s$ steps lead to precisely the configuration with label "none", state $s_0$, stack $k_1 = \omega^{-1}(f(x))$ (the whole output string, first symbol on top) and all other stacks empty. The time bound depends only on $|x|$; the length of $f(x)$ is not separately constrained (it is implicitly bounded by what can be pushed in $s$ steps, but no explicit bound appears).

PReducible

For two languages $L_1, L_2 \subseteq \mathrm{Str}$ over $\{\mathsf{false},\mathsf{true}\}$, $\mathrm{PReducible}(L_1, L_2)$ is the proposition that there exists a total function $f : \mathrm{Str} \to \mathrm{Str}$ such that (i) $\mathrm{PolyTimeComputable}(f)$ holds, i.e. there is a bundled TM2 multi-stack machine (finitely many stacks; input and output stack alphabets each in bijection with $\{\mathsf{false},\mathsf{true}\}$; finitely many labels and internal states; one step = complete execution of one labelled statement) and a polynomial $p \in \mathbb{N}[X]$ such that for every $x$, started with $x$ on the input stack, initial state, other stacks empty and label $\mathrm{main}$, the machine halts after exactly some $s \le p(|x|)$ steps in the configuration with label none, internal state equal to the initial state, output stack exactly $f(x)$ and all other stacks empty; and (ii) for every $x \in \mathrm{Str}$,

$$x \in L_1 \iff f(x) \in L_2.$$

This is a many-one reduction by a single total function; the equivalence is required for all $x$, including $x = [\,]$.

NPComplete

For a language $L \subseteq \mathrm{Str}$ over $\{\mathsf{false},\mathsf{true}\}$, $\mathrm{NPComplete}(L)$ is the conjunction of two statements: (i) $L \in \mathrm{NP}$, i.e. there exist $R : \mathrm{Str}\times\mathrm{Str} \to \{\mathsf{false},\mathsf{true}\}$ and $k \in \mathbb{N}$ with $\mathrm{PolyTimeChecker}(R)$ (a bundled TM2 multi-stack machine over the four-symbol tagged input alphabet, with a polynomial $p \in \mathbb{N}[X]$, halting on input $\mathrm{encodePair}(x,y)$ after at most $p(|x|+|y|)$ full-statement steps in the configuration with label none, initial internal state, output stack $[R(x,y)]$ and all other stacks empty) and $w \in L \iff \exists y,\ |y| \le |w|^k \wedge R(w,y) = \mathsf{true}$ for all $w$; and (ii) for every language $L' \in \mathrm{NP}$ (in the same sense), $\mathrm{PReducible}(L', L)$ holds, i.e. there is a total $f : \mathrm{Str} \to \mathrm{Str}$ computed by some bundled TM2 machine with two-symbol input and output alphabets within a polynomial number of steps in $|x|$ (halting in the configuration with label none, initial state, output stack $f(x)$, other stacks empty) such that $x \in L' \iff f(x) \in L$ for all $x$.

E

$\mathrm{E}$ is the set of languages $L \subseteq \mathrm{Str}$ over $\{\mathsf{false},\mathsf{true}\}$ for which there exists a total function $\chi : \mathrm{Str} \to \{\mathsf{false},\mathsf{true}\}$ such that (i) there exist a machine-with-time-bound $M$ of Mathlib's type TM2ComputableInTime (input encoding the identity on bit strings, output encoding $b \mapsto [b]$) computing $\chi$, together with natural numbers $c, C \in \mathbb{N}$ such that for every $n \in \mathbb{N}$,

$$\mathrm{time}_M(n) \le C \cdot 2^{\,c\, n};$$

and (ii) for every $w \in \mathrm{Str}$, $w \in L \iff \chi(w) = \mathsf{true}$. Here $M$ consists of: a bundled TM2 multi-stack machine (finite index set $K$ of stacks with decidable equality; input index $k_0$ and output index $k_1$, possibly equal; symbol types $\Gamma_k$ with only $\Gamma_{k_0}$ required finite; finite label set $\Lambda$ with distinguished $\mathrm{main}$; finite state set $\Sigma$ with initial state $s_0$; program assigning to each label a statement, i.e. a finite tree of push/peek/pop/load/branch operations driven by arbitrary functions of the state and top-of-stack, ending in goto or halt); bijections $\iota : \Gamma_{k_0} \cong \{\mathsf{false},\mathsf{true}\}$ and $\omega : \Gamma_{k_1} \cong \{\mathsf{false},\mathsf{true}\}$; an arbitrary time function $\mathrm{time}_M : \mathbb{N} \to \mathbb{N}$ (not required to be a polynomial); and, for every $w \in \mathrm{Str}$, a number of steps $s \le \mathrm{time}_M(|w|)$ such that from the initial configuration (label $\mathrm{main}$, state $s_0$, stack $k_0 = \iota^{-1}(w)$ with first symbol on top, all other stacks empty) exactly $s$ applications of the step function (one step = complete execution of the current label's statement; halted configurations have no successor) yield precisely the configuration with label "none", state $s_0$, stack $k_1 = [\omega^{-1}(\chi(w))]$ and all other stacks empty. The exponent $c$ may be $0$, in which case the bound is the constant $C$; if $C = 0$ the bound forces $\mathrm{time}_M \equiv 0$, which cannot be met since at least one step is needed to pass from a labelled to an unlabelled configuration, so any witness has $C \ge 1$. The bound $C \cdot 2^{cn}$ must hold for all $n$, including $n = 0$.

Literal

$\mathrm{Literal}$ is an abbreviation for the type $\{\mathsf{false},\mathsf{true}\} \times \mathbb{N}$: a literal is a pair $(s, i)$ of a sign bit $s$ and a variable index $i \in \mathbb{N}$ (variables are indexed by all natural numbers, starting at $0$). No further structure is imposed here; the meaning of the sign is fixed only by $\mathrm{evalLiteral}$ below.

Clause

$\mathrm{Clause}$ is an abbreviation for finite lists of literals, i.e. finite sequences $((s_1,i_1),\dots,(s_r,i_r))$ with $r \ge 0$; the empty clause is allowed, repeated literals are allowed, and a clause may contain both $(\mathsf{true},i)$ and $(\mathsf{false},i)$ for the same $i$. Order is part of the data (a clause is a list, not a set).

CNF

$\mathrm{CNF}$ is an abbreviation for finite lists of clauses, i.e. finite sequences $(c_1,\dots,c_m)$ of clauses with $m \ge 0$; the empty formula is allowed, repeated clauses are allowed, and order is part of the data.

evalLiteral

For an assignment $\tau : \mathbb{N} \to \{\mathsf{false},\mathsf{true}\}$ (a total function on all variable indices) and a literal $l = (s,i)$, $\mathrm{evalLiteral}(\tau, l)$ is the Boolean

$$\mathrm{evalLiteral}(\tau,(s,i)) = \begin{cases} \tau(i) & \text{if } s = \mathsf{true},\\ \neg\,\tau(i) & \text{if } s = \mathsf{false}. \end{cases}$$

So sign $\mathsf{true}$ denotes the positive literal $x_i$ and sign $\mathsf{false}$ the negated literal $\neg x_i$.

evalClause

For an assignment $\tau : \mathbb{N} \to \{\mathsf{false},\mathsf{true}\}$ and a clause $c = (l_1,\dots,l_r)$, $\mathrm{evalClause}(\tau, c)$ is $\mathsf{true}$ if and only if there exists some $j$ with $\mathrm{evalLiteral}(\tau, l_j) = \mathsf{true}$ (the disjunction of the literal values); in particular the empty clause evaluates to $\mathsf{false}$ under every $\tau$.

evalCNF

For an assignment $\tau : \mathbb{N} \to \{\mathsf{false},\mathsf{true}\}$ and a formula $F = (c_1,\dots,c_m)$, $\mathrm{evalCNF}(\tau, F)$ is $\mathsf{true}$ if and only if $\mathrm{evalClause}(\tau, c_j) = \mathsf{true}$ for every $j$ (the conjunction of the clause values); in particular the empty formula evaluates to $\mathsf{true}$ under every $\tau$, and any formula containing an empty clause evaluates to $\mathsf{false}$ under every $\tau$.

Satisfiable

For a formula $F \in \mathrm{CNF}$, $\mathrm{Satisfiable}(F)$ is the proposition that there exists a total assignment $\tau : \mathbb{N} \to \{\mathsf{false},\mathsf{true}\}$ (defined on all natural-number indices, not only those occurring in $F$) with $\mathrm{evalCNF}(\tau, F) = \mathsf{true}$, i.e. every clause of $F$ contains at least one literal $(s,i)$ with $\tau(i) = s$. The empty formula is satisfiable; a formula containing an empty clause is not.

encodeLiteral

For a literal $l = (s, i)$, $\mathrm{encodeLiteral}(l)$ is the bit string built as follows. Let $\mathrm{bits}(i)$ denote the binary digits of $i$ listed least-significant first with no leading zeros, so $\mathrm{bits}(0) = [\,]$, $\mathrm{bits}(1) = [1]$, $\mathrm{bits}(2) = [0,1]$, $\mathrm{bits}(6) = [0,1,1]$, and for $i \ge 1$ the list has length $\lfloor \log_2 i \rfloor + 1$ and ends in $1$ (writing $0$ for $\mathsf{false}$ and $1$ for $\mathsf{true}$). Form the list $(b_0, b_1, \dots, b_m) = (s, \mathrm{bits}(i))$ (the sign bit followed by the digits of $i$, so $m = |\mathrm{bits}(i)|$), replace each entry $b_j$ by the two-symbol block $(0, b_j)$, concatenate, and append the terminator $(1, 0)$:

$$\mathrm{encodeLiteral}(s,i) = (0, s,\ 0, b_1,\ \dots,\ 0, b_m,\ 1, 0).$$

Its length is $2m + 4 = 2|\mathrm{bits}(i)| + 4$. For example $\mathrm{encodeLiteral}(s, 0) = (0, s, 1, 0)$ and $\mathrm{encodeLiteral}(\mathsf{true}, 2) = (0,1,\ 0,0,\ 0,1,\ 1,0)$.

encodeClause

For a clause $c = (l_1, \dots, l_r)$, $\mathrm{encodeClause}(c)$ is the concatenation $\mathrm{encodeLiteral}(l_1)\,\cdots\,\mathrm{encodeLiteral}(l_r)$ followed by the two-symbol terminator $(1,1)$ (writing $1$ for $\mathsf{true}$). The empty clause encodes as $(1,1)$.

encodeCNF

For a formula $F = (c_1,\dots,c_m)$, $\mathrm{encodeCNF}(F)$ is the concatenation $\mathrm{encodeClause}(c_1)\,\cdots\,\mathrm{encodeClause}(c_m)$ with no additional delimiter; the empty formula encodes as the empty string $[\,]$.

SAT

$\mathrm{SAT}$ is the language over $\{\mathsf{false},\mathsf{true}\}$ consisting of all bit strings $w$ for which there exists a formula $F \in \mathrm{CNF}$ (a finite list of finite lists of sign/index pairs) with

$$\mathrm{encodeCNF}(F) = w \quad\text{and}\quad \mathrm{Satisfiable}(F),$$

where $\mathrm{encodeCNF}$ is the concatenation over clauses of (concatenation over literals $(s,i)$ of the blocks $(0,s),(0,b_1),\dots,(0,b_m),(1,0)$ with $b_1\dots b_m$ the least-significant-first binary digits of $i$ without leading zeros, followed by $(1,1)$), and $\mathrm{Satisfiable}(F)$ means some total assignment $\tau : \mathbb{N} \to \{\mathsf{false},\mathsf{true}\}$ makes every clause of $F$ contain a literal $(s,i)$ with $\tau(i) = s$. Strings that are not the encoding of any formula are not in $\mathrm{SAT}$; the empty string is in $\mathrm{SAT}$ (it encodes the empty formula, which is satisfiable). Membership only requires some formula with encoding $w$ to be satisfiable; no injectivity of the encoding is asserted in the definition.

ThreeSAT

$\mathrm{ThreeSAT}$ is the language over $\{\mathsf{false},\mathsf{true}\}$ consisting of all bit strings $w$ for which there exists a formula $F \in \mathrm{CNF}$ such that

$$\mathrm{encodeCNF}(F) = w, \qquad \text{every clause } c \text{ occurring in } F \text{ has list length exactly } 3, \qquad \text{and } \mathrm{Satisfiable}(F),$$

with $\mathrm{encodeCNF}$ and $\mathrm{Satisfiable}$ as in $\mathrm{SAT}$ (encoding: per literal $(s,i)$ the blocks $(0,s),(0,b_1),\dots,(0,b_m),(1,0)$ with $b_1\dots b_m$ the least-significant-first binary digits of $i$, per clause a trailing $(1,1)$, clauses concatenated; satisfiability: some total $\tau : \mathbb{N} \to \{\mathsf{false},\mathsf{true}\}$ makes each clause contain a literal $(s,i)$ with $\tau(i) = s$). "Length exactly $3$" counts list entries, so a clause such as $((\mathsf{true},0),(\mathsf{true},0),(\mathsf{true},0))$ or one containing both $(\mathsf{true},i)$ and $(\mathsf{false},i)$ qualifies; the condition is vacuous for the empty formula, so the empty string is in $\mathrm{ThreeSAT}$. Strings not encoding any formula all of whose clauses have length $3$ are excluded.