Cook–Levin 定理

把一条计算分支排成时间向下、纸带位置向右的 tableau。第 $t$ 行编码第 $t$ 步的完整配置。机器运行至多 $T$ 步，读写头离起点不会超过 $T$ 格；又因 $T\ge n$ 足以容纳输入，所以表格的高、宽都是 $O(T)$，共 $O(T^2)$ 个格子。

对每个时间 $t$、位置 $i$ 和局部标记 $a$ 引入变量 $X_{t,i,a}$。标记可以是普通带符号，也可以把“带符号 + 当前状态 + 读写头”合并在一个格中。公式由四类约束组成：

1. 单值约束：每个格子恰有一个标记。
2. 初始约束：第 $0$ 行精确编码输入、空白区、初始状态和头位置。
3. 转移约束：相邻两行的每个常数宽窗口符合 $N$ 的某条转移。
4. 接受约束：第 $T$ 行包含接受状态；接受自循环保证较短计算也能填满表格。

一次转移只改动头附近的常数个格子，远处格子保持不变。因此合法的相邻行关系可由有限种局部窗口描述；在所有重叠窗口上同时满足局部约束，就拼出一条全局一致的计算历史。非确定选择由满足赋值选择某个合法窗口序列，归约算法本身不需要猜中它。

单值约束怎样工作 ​

若某格允许标记集 $\{0,1,\bigsqcup \}$，简写对应变量为 $X_0,X_1,X_{\bigsqcup }$。该格恰有一个标记可写成

标记表对固定机器是常数大小，所以每格只增加常数个变量与子句。$O(T^2)$ 个格子的单值约束总规模仍为 $O(T^2)$；初始行有 $O(T)$ 个位置，相邻行的窗口有 $O(T^2)$ 个，每个窗口排除的非法局部图案数也只依赖固定机器 $N$。因此整份公式大小是 $\mathrm{poly}(T)=\mathrm{poly}(|x|)$。

双向正确性 ​

若 $N$ 有接受分支，就按该分支逐格填写 tableau，四类约束全部满足。若 ${\mathrm{\Phi }}_{N,x}$ 可满足，单值约束先给每格唯一标记，初始约束确定第一行，重叠的转移窗口再保证每一行确由前一行的一次合法转移得到；最后一行接受，故读出的确是一条接受分支。缺少反向论证，就无法排除满足公式但并非真实计算的伪表格。

容易漏掉的边界 ​

表格两侧需要端标记或足够的空白边界，较早停机的分支需要吸收式停机配置。若省略两两互斥子句，一个格子可以同时宣称多个标记；若只验证每行“像配置”而不检查相邻行，初始行与接受行可以被任意拼接。

定理首先得到一般 SAT。借助新变量对电路门或长子公式作 Tseitin 编码，可以在线性或多项式膨胀下得到与原公式等可满足的 3-CNF，从而导向3-SAT公理库3-SAT3-SAT · Three-satisfiability每个子句恰含三个文字的合取范式可满足性问题。；新公式不必在原变量上的每个赋值都与旧公式等价。这一步也不会让 2-SAT 变得困难，2-SAT 已知属于 P。除非证明 $\mathbf{P}\ne \mathbf{NP}$，Cook–Levin 本身还不能推出 SAT 的无条件超多项式下界。

Cook–Levin 为NP 完全性公理库NP 完全性NP-completeness同时属于 NP 且为 NP-hard 的性质。网络提供第一个通用起点。后续证明不必再次编码任意机器，只需从 SAT 或 3-SAT 出发，用局部构件把变量选择和约束传给图、集合、调度等目标。

tableau 还把NP公理库复杂度类 NPNP · Nondeterministic polynomial time由正实例拥有多项式长度、可在多项式时间内验证的证书所刻画的语言类。的抽象证书解释成一件具体对象：一份局部可核验的接受计算历史。多项式时间归约公理库多项式时间归约Polynomial-time reduction · Karp reduction用一个多项式时间可计算的变换把问题 A 的实例转换为问题 B 的实例。保存这份历史“存在或不存在”的答案，而不是保存解的数量、搜索顺序或某个求解器的运行轨迹。