Cook-Levin 定理 — NP-完全性的诞生

是什么

Cook-Levin 定理说的是：SAT（布尔可满足问题）是 NP 里最难的问题——任何”答案能快速验证”的问题，都可以翻译成 SAT 问题。

日常类比：一道很复杂的大题，比如”找到一种排课方案让所有冲突都消除”，可以拆成无数个小是非题——“x1 是真还是假？x2 是真还是假？……”——只要把所有小是非题答对，大题就解出来了。

1971 年 Stephen Cook 在加拿大多伦多发表了证明。1973 年 Leonid Levin 在苏联用俄语发表了几乎一样的结果。两人互不知道彼此，证明独立完成。1980 年代以后这个定理才合称 “Cook-Levin”。

这件事的意义：所有看似不同的难题，本质上都是同一个问题。

为什么重要

不理解 Cook-Levin，下面这些事都没法解释：

为什么旅行商问题、排课表、拼图、芯片布线、蛋白质折叠……上千个看似无关的难题，被算法学家一律称为”NP-完全”
为什么现代密码学（HTTPS / 银行 / 区块链）的安全性，全都建立在 “P ≠ NP” 这个未被证明的假设上——一旦这个假设被推翻，所有加密体系当天崩溃
为什么工业界遇到 NP-完全问题，老程序员立刻说”别想多项式时间算法了，要么近似要么启发式”
为什么 P vs NP 是 7 个千禧年难题之一，Clay 数学研究所悬赏 100 万美元，至今 50 多年无人能解

核心要点

要看懂 Cook-Levin，先要理解三个概念：

NP 类（难解但易验证）：找答案很难，但有人把答案告诉你，你可以快速检查它对不对。类比：数独——你自己解很费劲，但别人填好了你 30 秒就能验证每行每列每宫是否合法。
规约（A 转成 B）：把问题 A 的实例改写成问题 B 的实例，且改写过程很快（多项式时间），同时保证答案一致。类比：你不会做中文版数学题，但能快速翻译成英文题——只要英文题能解，中文题就能解。
NP-完全（NP 里最难的等价类）：一个问题如果是 NP 的，且 NP 中所有问题都能规约到它，那它就是 NP-完全。类比：班里 50 道题里最难的那一道，所有其他题都能转化成它——你做出它，全班题都做出。

Cook-Levin 证明的就是：SAT 是第一个被发现的 NP-完全问题。

实践案例

案例 1：一个简单的 SAT 实例

(x ∨ y) ∧ (¬x ∨ z)

读这个公式：

x、y、z 是布尔变量，只能取真（true）或假（false）
∨ 读作”或”——两个里至少一个为真，整体就为真
∧ 读作”且”——两个都为真，整体才为真
¬x 读作”非 x”——x 为真则 ¬x 为假，反之亦然

整个公式问的是：有没有一种 x、y、z 的取值，让整个式子为真？

试试 x=true, y=任意, z=true：

(x ∨ y) = (true ∨ ...) = true
(¬x ∨ z) = (false ∨ true) = true
整体 = true ∧ true = true，可满足！

这就是 SAT。变量多到几千几万个时，找出”是否存在可满足赋值”就变得极难——但给你一个赋值，验证只需把每个值代入算一下。这正是 NP 的特征。

案例 2：把图着色规约成 SAT

“3-着色”问题：给一张图，能不能用 3 种颜色给每个顶点上色，让相邻顶点颜色不同？

转成 SAT 大致这样做：

给每个顶点 v 准备 3 个布尔变量：v_红、v_蓝、v_绿，每个变量为真表示”顶点 v 是这个颜色”
写约束子句：
- 每个顶点至少一个颜色：(v_红 ∨ v_蓝 ∨ v_绿)
- 每个顶点最多一个颜色：(¬v_红 ∨ ¬v_蓝) 等
- 相邻顶点颜色不同：对每条边 (u, v)，写 (¬u_红 ∨ ¬v_红) ∧ (¬u_蓝 ∨ ¬v_蓝) ∧ (¬u_绿 ∨ ¬v_绿)

把所有约束 ∧ 起来，就是一个 SAT 公式。这个 SAT 可满足 ⟺ 原图能 3-着色。规约完成。

这就是规约的力量：一个问题被 SAT 接管了。

案例 3：现代 SAT 求解器

现实中有强大的 SAT 求解器，比如 Z3（微软研究院）、MiniSat（学术界经典）、CaDiCaL（SAT 比赛常胜冠军）。它们能秒级解决百万级变量的工业问题。

理论上 SAT 是 NP-完全（最坏情况指数时间），但实际工业实例往往有结构，求解器能利用结构跑得飞快。这个”理论难 vs 实际能跑”的 gap，本身就是研究热点。

踩过的坑

NP 不是 “non-polynomial” 的缩写：很多人望文生义。NP = Nondeterministic Polynomial（非确定性多项式时间），意思是”在非确定性图灵机上多项式时间能解”，等价于”答案可以多项式时间验证”。
NP-hard 不一定在 NP 内：停机问题是 NP-hard（NP 里所有问题都能规约到它），但停机问题不可判定——它根本不在 NP 里。“至少和 NP 最难的一样难”≠“在 NP 内”。
P = NP 还没被证伪：不少新人以为”P ≠ NP 已经是事实”。实际上两个方向都没人证明，是开放问题。绝大多数研究者相信 P ≠ NP，但这是直觉，不是定理。
量子计算机不是 NP 的杀手：流传”量子计算机能解所有 NP 问题”是误解。Grover 算法对 SAT 只有平方加速（2^(n/2) 而不是 2^n），不是指数级。BQP（量子多项式）vs NP 的关系至今未知。

适用 vs 不适用场景

适用（用 Cook-Levin 思路分析问题）：

看到一个新难题，先问”它在 NP 里吗？“——如果是，再试图规约一个已知 NP-完全问题过来证明它难
工业问题（排程 / 路由 / 装箱 / 调度）大多是 NP-hard，提前知道”别浪费时间找多项式精确解”
写论文证明算法效率：通过规约证明问题难度下界

不适用：

实例规模很小（n < 30）→ 暴力搜索就够了，不用复杂度理论
实例有特殊结构（树形 / 平面图 / 有界宽度）→ 可能有多项式特例算法
关心 average-case 而非 worst-case → NP-完全只刻画最坏情况，工业 SAT 实际”很容易”
近似解可接受 → 用近似算法 / 启发式 / 元启发式（遗传 / 模拟退火）绕过 NP-hard

历史小故事（可跳过）

1936 年：Turing 给出图灵机模型，回答”什么可计算”。停机问题被证明不可判定（turing-1936）。
1965 年：Hartmanis-Stearns 证明时间层次定理，复杂度类的研究开始。Edmonds 提出 “good algorithm = polynomial time” 的论断。
1971 年：Cook 在多伦多大学发表 STOC 论文，10 页，在图灵机模型上构造 SAT 公式编码任意 NP 问题的执行轨迹。
1973 年：Levin 在苏联用俄语发表 2 页论文 “Universal Sequential Search Problems”，给出 6 个 universal search problems。冷战时期信息隔绝，1980 年代西方学界才知道。
1972 年：Cook 论文出来一年后，Karp 写论文证明 21 个常见问题都是 NP-完全的（旅行商、装箱、图着色、独立集等）——把这条线推爆，归约工具箱建立（karp-21）。
1986 年：Levin 论文被翻译成英文。两人合称 “Cook-Levin 定理”。

之后 50 多年，整个算法理论的”难度刻画”全部站在 Cook-Levin 之上。

学到什么

“难”可以被数学化——Cook-Levin 之前，人们说”这个问题难”靠直觉；之后，“难”有了精确定义和分类。
规约是复杂度理论的核心武器——把新问题翻译成已知问题，是证明难度下界的基本套路。
NP-完全是一个等价类——3-SAT、旅行商、图着色、装箱……上千个问题本质上是同一个问题，解决任何一个就解决全部。
理论难 vs 实际能跑常常并存——SAT 理论上 NP-完全，工业 SAT 求解器实际秒级解大规模实例。这个 gap 是研究 average-case 复杂度的动力。
科学发现常常并行——Cook 和 Levin 互不知情、用不同语言、隔着冷战铁幕、独立给出本质相同的证明。这种”时代到了，答案自己出现”的故事在科学史上反复发生。

关联

turing-1936 —— Cook 的证明在图灵机模型上做，把 NP 问题编码成图灵机执行轨迹的布尔公式
karp-21 —— Karp 1972 跟进 Cook，证明 21 个常见问题 NP-完全，归约工具箱建立
lambda-calculus —— 与图灵机等价的另一套可计算性模型，Cook-Levin 之前可计算性理论的基石
hindley-milner —— 类型推导也是 NP-完全（一般情况下），HM 是它的可判定子集

反向链接

biere-bmc-1999 —— Bounded Model Checking — 把硬件验证翻译成一道 SAT 题
blinn-1977 —— Blinn 1977 — 用半角向量 H 把高光算量减半
chaff-2001 —— Chaff 2001 — 把 CDCL 工程化的两个杀手锏
davis-putnam-1960 —— Davis-Putnam 1960 — 让机器自动判断一堆逻辑式能不能同时成立
dijkstra-shortest-path —— Dijkstra 最短路径 — 一杯咖啡时间想出来的贪心算法
dpll-1962 —— DPLL 1962 — 把”逻辑判定”从内存爆炸救成栈式回溯
hindley-milner —— Hindley-Milner — 编译器自己猜变量类型
karp-21 —— Karp 21 — 21 个 NP-完全问题
lambda-calculus —— λ-演算 — 用三条规则表达所有可计算函数
li-t-closeness-2007 —— t-Closeness — 用”分布距离”堵住匿名化的最后漏洞
lsh-indyk-1998 —— LSH — 让相似点撞同一个桶，把高维最近邻查询从线性变成亚线性
marques-silva-grasp-1996 —— GRASP 1996 — 让 SAT 求解器从冲突里学到东西
minisat-2003 —— MiniSat 2003 — 600 行 C++ 把 CDCL 写成教科书
neumann-2015-large-joins —— Adaptive Optimization of Very Large Join Queries — 100 张表也敢精确求解
sweeney-k-anonymity-2002 —— k-匿名 — 发布数据时让攻击者无法锁定你是谁
turing-1936 —— Turing 1936 可计算性
zk-snark —— zk-SNARK 零知识证明