Cook-Levin 定理
In computational complexity theory, the Cook-Levin theorem, also known as Cook's theorem, states that the Boolean satisfiability problem is NP-complete.
在计算复杂度理论中，Cook-Levin 定理（也称为 Cook 定理）指出布尔可满足性问题是 NP 完全的。
That is, it is in NP, and any problem in NP can be reduced in polynomial time by a deterministic Turing machine to the Boolean satisfiability problem.
也就是说，它属于 NP 类，并且任何 NP 问题都可以通过确定性图灵机在多项式时间内归约为布尔可满足性问题。
The theorem is named after Stephen Cook and Leonid Levin.
该定理以 Stephen Cook 和 Leonid Levin 的名字命名。
An important consequence of this theorem is that if there exists a deterministic polynomial-time algorithm for solving Boolean satisfiability, then every NP problem can be solved by a deterministic polynomial-time algorithm.
该定理的一个重要推论是，如果存在确定性的多项式时间算法来解决布尔可满足性问题，那么每个 NP 问题都可以用确定性的多项式时间算法来解决。
The question of whether such an algorithm for Boolean satisfiability exists is thus equivalent to the P versus NP problem, which is one of the seven Millennium Prize Problems.
布尔可满足性问题是否存在这样的算法，等价于 P versus NP 问题，这是七个千禧年大奖问题之一。
Definitions
定义
A decision problem is in NP if it can be decided by a nondeterministic Turing machine in polynomial time.
如果一个问题能够被非确定性图灵机在多项式时间内判定，则它属于 NP。
An instance of the Boolean satisfiability problem is a Boolean expression that combines Boolean variables using Boolean operators such as AND, OR, and NOT.
布尔可满足性问题的实例是一个布尔表达式，它使用布尔运算符（如 AND、OR 和 NOT）组合布尔变量。
Such an expression is satisfiable if there is some assignment of truth values to the variables that makes the entire expression true.
如果存在一种对变量的真值赋值使得整个表达式为真，则该表达式是可满足的。
Idea
证明思路
Given any decision problem in NP, construct a non-deterministic machine that solves it in polynomial time.
对于任意 NP 中的判定问题，构建一个在多项式时间内求解它的非确定性机器。
Then for each input to that machine, build a Boolean expression that computes whether when that specific input is passed to the machine, the machine runs correctly, and the machine halts and answers "yes".
然后对于该机器的每个输入，构造一个布尔表达式，用于计算当该特定输入传递给机器时，机器是否正确运行并且机器是否停止并回答"是"。
Then the expression can be satisfied if and only if there is a way for the machine to run correctly and answer "yes",
那么该表达式可满足当且仅当机器有某种方式可以正确运行并回答"是"
so the satisfiability of the constructed expression is equivalent to asking whether or not the machine will answer "yes".
因此，所构造表达式的可满足性等价于询问机器是否会回答"是"。
Proof
证明
This proof is based on the one given by Garey & Johnson 1979.
该证明基于 Garey & Johnson 1979 年给出的证明。
There are two parts to proving that the Boolean satisfiability problem (SAT) is NP-complete.
证明布尔可满足性问题 (SAT) 是 NP 完全的需要两个部分。
One is to show that SAT is in NP.
一是证明 SAT 属于 NP。
The other is to show that every NP problem can be reduced to an instance of a SAT problem by a polynomial-time many-one reduction.
另一个是证明每个 NP 问题都可以通过多项式时间的多对一归约归约为 SAT 问题的一个实例。
SAT is in NP because any assignment of Boolean values to Boolean variables that is claimed to satisfy the given expression can be verified in polynomial time by a deterministic Turing machine.
SAT 属于 NP，因为任何声称满足给定表达式的布尔变量赋值都可以由确定性图灵机在多项式时间内验证。
Now suppose that a given problem in NP can be solved by the nondeterministic Turing machine M=(Q, Σ, s, F, δ) in polynomial time.
现在假设 NP 中的一个给定问题可以由非确定性图灵机 M=(Q, Σ, s, F, δ) 在多项式时间内求解。
Given an input w to M, we will construct a Boolean formula φM,w that is satisfiable if and only if M accepts w.
给定 M 的输入 w，我们将构造一个布尔公式 φM,w，使得当且仅当 M 接受 w 时它是可满足的。
The idea is to simulate the computation of M on w using propositional variables.
其思想是用命题变量模拟 M 在 w 上的计算。
If n = |w|, then any computation of M on w has at most n^k configurations (for some constant k).
如果 n = |w|，则 M 在 w 上的任何计算最多有 n^k 个格局（对于某个常数 k）。
Each configuration is an element of C^n^k, where C = Q ∪ Γ ∪ {#} (the set of states, tape alphabet symbols, and the endmarker).
每个格局是 C^n^k 中的元素，其中 C = Q ∪ Γ ∪ {#}（状态、带字母表符号和结束标记的集合）。
We define propositional variables x(i,j,s) for every cell in row i, column j, and element s ∈ C.
我们为第 i 行、第 j 列的每个单元格和每个元素 s ∈ C 定义命题变量 x(i,j,s)。
We interpret x(i,j,s) as true iff the cell (i,j) contains s.
我们解释 x(i,j,s) 为真当且仅当单元格 (i,j) 包含 s。
We require formulas that verify the computation expresses conditions for an accepting computation on w.
我们要求验证计算的公式表达 w 上接受计算的条件。
This includes: each cell contains exactly one symbol; at each step, the machine is in exactly one state; the start configuration is correct; transitions are valid; and the final state is an accepting state.
这包括：每个单元格恰好包含一个符号；每一步机器恰好处于一个状态；起始格局正确；转移有效；最终状态是接受状态。
The overall formula φ has the following structure: φcell ∧ φstart ∧ φaccept ∧ φmove
整体公式 φ 具有以下结构：φcell ∧ φstart ∧ φaccept ∧ φmove
Claim: M accepts w if and only if φM,w is satisfiable.
断言：M 接受 w 当且仅当 φM,w 是可满足的。
Thus, w → φM,w is a polynomial-time reduction from L to SAT.
因此，w → φM,w 是从 L 到 SAT 的多项式时间归约。
Since this holds for every L ∈ NP, SAT is NP-hard.
由于这对每个 L ∈ NP 都成立，所以 SAT 是 NP 难的。
Since SAT ∈ NP and SAT is NP-hard, SAT is NP-complete.
由于 SAT ∈ NP 且 SAT 是 NP 难的，因此 SAT 是 NP 完全的。
Consequences
意义
The Cook-Levin theorem shows that NP-complete problems exist.
Cook-Levin 定理证明了 NP 完全问题的存在。
Any NP-complete problem can be used to solve any other problem in NP, given a polynomial-time algorithm for the NP-complete problem.
任何 NP 完全问题都可以用来解决 NP 中的任何其他问题，前提是 NP 完全问题有多项式时间算法。
This is because any problem in NP can be reduced to any NP-complete problem in polynomial time.
这是因为 NP 中的任何问题都可以在多项式时间内归约为任何 NP 完全问题。
In particular, if P ≠ NP, then there exist problems in NP that are neither in P nor NP-complete.
特别地，如果 P ≠ NP，那么 NP 中存在既不在 P 中也不是 NP 完全的问题。