跳转到内容
← 返回计算理论
计算理论当代约 20 分钟阅读

Cook 1971：定理证明手续的复杂度怎样把 SAT 写成 NP 完全

The Complexity of Theorem-Proving Procedures

Cook-LevinNP完全SATSTOC 1971多项式归约

1971 年 5 月 3 日至 5 日，第三届 ACM 计算理论年会（STOC）在俄亥俄州谢克海茨（Shaker Heights）举行。多伦多大学的斯蒂芬·库克（Stephen A. Cook）发表《The Complexity of Theorem-Proving Procedures》，页码 151 至 158。DOI 为 10.1145/800157.805047。本页的对象是这份已发表的八页短文：把命题演算里「公式是否为重言式」写成一类多项式时间完全问题，并给出把任意多项式时间非确定性图灵机的接受计算编译成布尔公式的装置。归约口径是带神谕的询问机，也就是后来所称的库克归约（多项式时间图灵归约），不是次年卡普才收紧的多一归约。

它不是 斯蒂芬·库克 的人物页，不是 计算复杂性 的总览，更不是卡普 1972 年的二十一个组合问题，也不是 SAT 求解 的工程史。列昂尼德·列文（Leonid Levin）是邻居，不是封面。本页不把千禧年悬赏当成对象。

破除误解：完全性不是「没有算法」，也不是 1972 年的多一归约

第一层误解把标题听成「定理证明没有算法」，或听成布尔可满足性不可判定。命题重言式有算法：枚举全部赋值即可。库克要给的不是停机意义上的不可能，而是一条关于多项式资源的完全性。可计算性 已经把「有没有手续」写成图灵机能否停机；本页假定手续存在，问的是手续能否被多项式时间的确定性机器替代。把 SAT 听成停机问题，会把 1971 年收进 1936 年。

第二层误解把教材里的标准句提前写进这一年：「库克证明 SAT 在多一归约下 NP 完全」。原文的目标语言首先是重言式，尤其是析取范式重言式。他先造一份合取范式 $A(w)$，使 $A(w)$ 可满足当且仅当非确定性机器接受 $w$；再取否定，用德摩根律改写成析取范式，¬A(w)\neg A(w) 为重言式当且仅当 $w$ 不被接受。询问机拿这份析取范式去问神谕，再把答案翻转。极性在这里必须翻一次。多一归约会把「是」映成「是」，因而后来标准定义里 SAT 落在 $NP$、重言式落在 coNP\mathrm{coNP}。库克允许神谕、允许翻转，两个互补问题因此落在同一多项式度数里。把 1971 年读成卡普口径，会把一次询问机归约收成一次实例映射。

第三层误解把「窗口」听成论文里已经印好的 2×32\times 3 格子，或听成求解器后来吃工业实例的那套局部传播。库克用三族命题变元记下每一步的磁带符号、状态与磁头位置，再用局部子句强迫相邻两步符合转移函数。后来教科书把同一件局部性画成计算表上的常数窗口。画法是教具，对象是：一步转移只碰常数个格子，因而可以写成常数大小的子句。本页不把窗口写成操作单，也不把稀疏性写成「因此 SAT 在实践里已经属于 $P$」。

第四层误解把对象听成千禧年问题，或听成卡普那张二十一题清单，或听成列文与库克是同一篇论文的两个署名。库克猜想重言式大概不在他记作 L∗L^* 的多项式时间类里，并写明证出这一点将是重大突破。他没有把这句话写成悬赏章程。列文 1973 年的俄文短文谈通用搜索问题，是平行发现，不是本页封面，对象见 Levin 1973。把后来的命名习惯读回这八页，会把一次存在性编译收成一部学科史。

询问机、非确定性时间，以及把接受计算写成公式

装置从询问机开始。询问机是多带图灵机，另加一条询问带，以及询问、是、否三个特殊状态。每次进入询问状态，神谕根据询问带上的串是否属于集合 $T$，把下一状态设成「是」或「否」。集合 $S$ 多项式可归约到 $T$，当且仅当存在一台询问机与一个多项式 $Q(n)$，使得对每个输入 $w$，以 $T$ 为神谕的计算在 $Q(|w|)$ 步内停机，并且停在接受态当且仅当 w∈Sw\in S。这种关系后来叫库克归约。它可传递。互相可归约的集合构成同一个多项式难度度数。库克把只含零函数的那一档记作 L∗L^*，并点明它是科巴姆（Alan Cobham）1964 年函数类 $L$ 的串语言对应物。用后来的符号，L∗L^* 就是 $P$。

非确定性图灵机在本页里是接受装置，不是「随机乱猜」。机器每一步可以有若干合法转移；接受意味着存在一条长度不超过多项式 $T=Q(n)$ 的转移序列走进接受态。库克假定机器只有一条向右无限的磁带，格子从左至右编号为 1,2,…1,2,\ldots。时间不超过 $T$ 则磁头扫不到第 $T$ 格以右。于是整段接受计算可以被一张 $T$ 步乘 $T$ 格的表写尽，变元数目随 T2T^2 增长。归约本身由确定性机器在 $|w|$ 的多项式时间内写出公式，不调用神谕去「帮忙编码」。

命题符号分成三族。Ps,tiP^i_{s,t} 为真，当且仅当第 $t$ 步时第 $s$ 格写着字母 σi\sigma_i。QtiQ^i_t 为真，当且仅当第 $t$ 步时状态为 qiq_i。Ss,tS_{s,t} 为真，当且仅当第 $t$ 步时磁头停在第 $s$ 格。公式 $A(w)$ 是合取 B∧C∧D∧E∧F∧G∧H∧IB\wedge C\wedge D\wedge E\wedge F\wedge G\wedge H\wedge I，并且整体保持合取范式。$B$ 说每一步恰好扫描一格：$T$ 个位置的析取，合上两两不能同时为真。$C$ 说每个时间—格子对上恰好一个符号。$D$ 说每一步恰好一个状态。$E$ 写下初始格局：起始状态、磁头在第 1 格、输入 $w$ 占前 $n$ 格、其余为空白。$F$、$G$、$H$ 分别更新符号、状态与磁头。库克给出的状态更新是局部的：若第 $t$ 步处于 qiq_i 且正扫描 σj\sigma_j，则第 $t+1$ 步必须进入转移函数指定的 qkq_k，写成对每个格子 $s$ 的子句 ¬Qti∨¬Ss,t∨¬Ps,tj∨Qt+1k\neg Q^i_t\vee\neg S_{s,t}\vee\neg P^j_{s,t}\vee Q^k_{t+1}。磁带上未被扫描的格子必须原样复制；被扫描的格子必须按转移函数改写。$I$ 说某个时刻出现接受态。库克要求机器在接受之后以平凡方式继续跑，好让接受态落在固定长度 $T$ 之内。

这就是窗口编码在 1971 年的原形状。磁头一步至多移动一格，所以第 $t+1$ 步第 $s$ 格的合法内容，只取决于第 $t$ 步里 $s-1$、$s$、$s+1$ 附近的符号、状态与磁头。后来教材把六个格子收成 2×32\times 3 窗口，并证明：起始行合法且每个窗口合法，则每一行都是合法格局。窗口不是另一种定理，它是把 $F$、$G$、$H$ 的局部性画出来。公式可满足，当且仅当存在一条接受计算。整张表的约束是这些常数子句的合取；每个变元只进入常数个窗口。稀疏性属于这份编译的几何，不是求解器手册。

询问机如何使用神谕，必须把极性写清。$A(w)$ 可满足当且仅当 $w$ 被接受。于是 ¬A(w)\neg A(w) 为重言式当且仅当 $w$ 不被接受。把 ¬A(w)\neg A(w) 改成析取范式之后，询问「它是不是析取范式重言式」，再把神谕的「是」读成拒绝、「否」读成接受，就得到定理 1：凡被多项式时间非确定性机器接受的集合，都多项式可归约到析取范式重言式。一次询问、一次翻转，已经用满库克归约比多一归约多出来的那一点自由。本页不把这套编译写成「如何把口令搜索改成公式」的步骤。它只证明：存在一份确定性的、多项式长的书写手续，把「存在接受计算」变成「存在满足赋值」。

定理 2 把同一度数里的几个语言钉在一起。任意重言式显然不比析取范式重言式更容易。析取范式重言式多项式可归约到 D3D_3：若某一析取项里合取了超过三个文字，就引入新原子 $P$，把长项拆成 (P∧R3∧⋯∧Rs)∨(¬P∧R1∧R2)(P\wedge R_3\wedge\cdots\wedge R_s)\vee(\neg P\wedge R_1\wedge R_2) 与其余项的析取，重言式真值不变；反复拆到每项至多三个合取。D3D_3 再归约到子图对：以每个析取项为一个顶点做成完全图 G1G_1，以每项的三个文字为顶点做成 G2G_2，仅在文字不互补时连边；再给每项贴上彼此足够不同的小图，迫使同态必须在每一项里恰好选一个文字去证伪。经过这套改写，G1′G'_1 能嵌入 G2′G'_2 当且仅当原公式不是 D3D_3 重言式。极性再次翻转，这在询问机口径下合法。库克写明：他没能把素数或图同构对加进这张名单。把重言式归约到素数，在他看来需要数论深处的结果；归约到图同构，则会触动科内尔当时关于图同构可在多项式时间解决的猜想。戴维斯（Martin Davis）与普特南（Hilary Putnam）1960 年的手续足以把每项至多两个合取的 D2D_2 放进 L∗L^*，对偶即后来的 2-SAT 属于 $P$。

它证明了什么，没有覆盖什么

它证明了：多项式时间非确定性可识别的语言，都可以通过询问机归约到析取范式重言式；因而重言式、受限重言式与子图同构检测落在同一多项式度数。它给出一张存在性证书：若重言式（或 SAT）可在确定性多项式时间内判定，则 L∗L^* 将吞掉整个非确定性多项式时间类。用后来的符号，这就是「SAT 对 $NP$ 完全」在库克口径下的原句。编码开销来自表的尺寸 O(T2)O(T^2) 与每个窗口的常数子句，不是来自对神谕的多次自适应询问——定理 1 的主编译其实只问一次。

它没有证明重言式不属于 L∗L^*。库克把这一点写成值得投入巨大努力的猜想，并指出停机问题那套对角化在这里套不上：若把 $NP$ 看成「在多项式界限内存在一条证据、而核对属于 $P$」的类 L+L^+，则判定重言式正是这个类里的完全度数，恰如停机问题是递归可枚举集里的完全度数；拿掉量词上的多项式界限，L+L^+ 就变回递归可枚举。类比说明完全性的形状，不提供分离。相对化障碍是 1975 年的后话，见 P vs NP 的证明障碍；原装神谕构造见 Baker–Gill–Solovay 1975。电路复杂度 也不是本页对象。

它没有采用多一归约作为定义。理查德·卡普（Richard Karp）1972 年在《Reducibility among Combinatorial Problems》里把归约收紧为一次确定性多项式映射、答案相同，并从 SAT 出发拉出二十个组合问题，连同 SAT 共二十一个。多一归约更严，后来成为 NP 完全性的标准定义；库克度数在互补之下闭合，卡普度数把 $NP$ 与 coNP\mathrm{coNP} 分开。主编译把 $A(w)$ 本身做成可满足性实例，本来就是多一的；需要翻转的是目标语言叫重言式还是 SAT。卡普证明组合问题的海洋与 SAT 同生共死。收紧发生在后一年，不是 1971 年的定义。

它没有覆盖列文。列文 1973 年在《信息传输问题》上把「通用搜索问题」写成：存在一些问题，任何搜索任务都可以有效地译成它们。西方文献过了数年才充分对照。今日写库克–列文，承认的是同一数学对象被发现了两次，不是 STOC 论文有第二作者。原文第三节用赫布兰德替换实例计量谓词演算证明器，那是另一套测量，不是本页对象。

稳健性来自局部性，不来自后来的产品。只要计算模型一步只改动常数个格子，窗口编译就可以从单带图灵机搬到多带、搬到随机存取，多项式次数会变，完全性这一档不会变。卡普口径收紧之后，SAT 仍然完全；D3D_3 的对偶就是 3-SAT。他当时不肯写入名单的素数与图同构，后来也没有被强迫进 NP 完全：素数判定进入了 $P$，图同构的度数仍开放。密码学基础 后来需要的是平均情况困难与单向函数，不是「SAT 最坏情况完全因此密文安全」。本页是编译的证据对象，不提供如何把攻击编码进公式、如何用求解器去拆协议的步骤。

概念证据到此为止。询问机回答的是「完全性在 1971 年用哪一种归约写下」；窗口回答的是「非确定性时间如何变成局部子句」。两句都不是操作单。工业求解器能解开许多带结构的实例，并不把最坏情况的地图作废，那是 SAT 求解 的另一页。

跨域连接

  • 计算复杂性：总览页把 $P$、$NP$ 与完全性收成一张学科地图；本页只提供地图上的第一枚钉子。钉子的形状是询问机度数，不是后来教材默认的多一箭头。把两页叠在一起读，才能看见：完全性先作为「与重言式同一度数」出现，再被收紧成「每个 $NP$ 语言一次映射到 SAT」。地图可以后写；钉子的金属成分以 1971 年的定义为准。
  • 可计算性：停机问题是递归可枚举集的完全问题；库克把重言式写成 L+L^+ 里的完全问题。类比是形状上的，不是证明上的。停机的对角化依赖「机器可以吃自己的描述并反过来」；多项式时钟把这句自指挡住了，因为模拟必须在 $T$ 步内结束，不能再要一个无界的「最终」。可判定与多项式可判定因此是两层边界。把 SAT 听成不可判定，会把资源问题收成存在问题。
  • 证明：库克把「存在一条接受计算」编译成可满足公式，等于把一次机器运行写成命题证明的对象。赋值若存在，它就是那条计算的证书；验证赋值只消多项式时间，这正是 $NP$ 作为「短证明可核」的原义。数学里的证明要求从公理推出必然为真；这里的证书只要求局部窗口全部合法。必然性被换成存在性：公式不必是重言式，它只须有一次成真。把 SAT 证书听成欧几里得式的普遍证明，会把搜索到的一条路径说成对所有路径的裁决。
  • 认识论：神谕被允许瞬间回答「这是不是重言式」，询问机仍须在多项式步内决定自己的输入是否属于 $S$。完全性说的是：若你拥有关于重言式的可靠神谕，你就拥有关于整个短证书类的知识。它不说你已经拥有神谕。把「可归约到重言式」听成「我们已经知道重言式的答案」，是把一种证据关系做成了占有。库克提供的是翻译手续，不是神谕本身。翻转极性尤其提醒：同一份公式，问可满足与问重言式，是对互补命题的两种知识请求。
  • 逻辑与计算：命题连接词在这里不是程序验证里的类型，而是把局部一致性写成合取与析取的纸。库克选用布尔公式，因为一步转移的查表恰好是常数个文字的布尔组合。谓词演算被他放到第三节去计量自动证明器，并不进入定理 1 的完全性。柯里–霍华德把证明当成程序；本页把计算当成待满足的命题。方向相反，对象不同。不要把 SAT 编译读成在 Coq 里构造了一条接受路径。
  • 科学哲学：库克把「看起来难」改写成可检验的关系：一个问题与重言式同度数，当且仅当两边可以互相多项式归约。经验上的难不再是实验室口碑，而是一份编译是否存在。证伪完全性需要的不是又一个解得很快的实例，而是一个反例语言，它在 $NP$ 里却不能归约到 SAT——在标准假设下这样的语言不应存在。科学理论在这里的内容是归约闭包，不是对单个谜题的直觉。把完全性听成「旅行商很难所以 SAT 很难」，说反了箭头：先有通用机器的编译，后有组合问题的海洋。

参考文献

  • Stephen A. Cook, "The Complexity of Theorem-Proving Procedures", Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, Shaker Heights, Ohio, 1971, pp. 151–158. DOI: 10.1145/800157.805047. —— 本文对象：询问机多项式归约、把非确定性计算编译为公式，以及重言式的多项式完全性。
  • Alan Cobham, "The Intrinsic Computational Difficulty of Functions", in Proceedings of the 1964 International Congress for Logic, Methodology and Philosophy of Science, North-Holland, 1965, pp. 24–30. —— 论文点名的多项式时间函数类 $L$，库克的 L∗L^* 是其串语言对应物。
  • Martin Davis & Hilary Putnam, "A Computing Procedure for Quantification Theory", Journal of the ACM 7(3), 1960, pp. 201–215. DOI: 10.1145/321033.321034. —— 论文用来说明 D2D_2 属于 L∗L^* 的手续。
  • Richard M. Karp, "Reducibility among Combinatorial Problems", in Complexity of Computer Computations, Plenum Press, 1972, pp. 85–103. —— 次年的多一归约与二十一个组合问题，用以标明口径收紧不是 1971 年的定义。
  • Leonid A. Levin, "Universal Sequential Search Problems", Problemy Peredachi Informatsii 9(3), 1973, pp. 115–116. 英译：Problems of Information Transmission 9(3), 1973, pp. 265–266. —— 平行发现，用以标明列文是邻居不是封面。
  • John E. Hopcroft & Jeffrey D. Ullman, Formal Languages and Their Relation to Automata, Addison-Wesley, 1969. —— 论文对角化一步所引，用以标明停机问题的对角化为何不能直接搬来分离 L∗L^*。

延伸阅读

  • 与 斯蒂芬·库克 对读：人物页管完全性之后的证明复杂性与图灵奖；本页停在 1971 年的询问机与窗口。
  • 与 计算复杂性 对读：先看 $P$ 与 $NP$ 的类语言，再看本页如何把其中一个类钉到具体公式问题上。
  • 与 可计算性 对读：停机完全性与重言式完全性形状相似，对角化能否搬迁是分界。
  • 与 P vs NP 的证明障碍 对读：库克已指出对角化套不上；相对化把这句观察收成定理。
  • 与 SAT 求解 对读：最坏情况完全性与工业实例可解可以叠在同一语言上，不互相取消。
  • 与 密码学基础 对读：单向函数要的是平均情况，不是 SAT 的最坏情况完全性。
  • 与 户田 1991 对读：判定完全性钉的是 NP；一次计数神谕可以把整座多项式层次吞掉，那是后到的力量，不是 1971 年的窗口编译。

正文中引用本条 · 25