库克-列文定理(Cook-Levin Theorem)

库克-列文定理(Cook-Levin Theorem)是计算复杂度理论的奠基性结果。它证明布尔可满足性问题(SAT)属于 NP 完全,即 SAT 既在 NP 类中,又能让 NP 中的每一个问题在多项式时间内归约到它。这意味着如果 SAT 能被高效求解,那么 NP 中所有问题都能被高效求解。

概述

该定理由斯蒂芬·库克(Stephen Cook)于 1971 年发表,列昂尼德·列文(Leonid Levin)几乎同时独立得到类似结果,因此以二人共同命名。它是第一个自然问题被证明为 NP 完全的例子,开启了通过归约寻找 NP 完全问题的研究浪潮。此后卡普等人在此基础上证明了大量常见问题同样是 NP 完全的。

核心原理

• 模拟计算过程:证明的核心是把任意非确定图灵机在多项式时间内的计算过程,编码成一个布尔公式。
• 可满足即接受:该公式可满足当且仅当图灵机存在一条接受的计算路径。
• 多项式规模:所构造公式的规模是输入长度的多项式,保证了归约在多项式时间内完成。
• 确立完全性:由于覆盖了 NP 中所有问题,SAT 因此成为 NP 完全问题的原型。

应用场景

库克-列文定理是判定问题困难性的起点。要证明一个新问题是 NP 完全的,只需将已知的 NP 完全问题多项式归约到它,而这条归约链最终都可追溯到 SAT。它深刻影响了算法设计:面对 NP 完全问题,人们转而寻求近似算法、启发式或针对特殊情形的解法。

常见问题

问:为什么 SAT 如此重要?答:因为它是第一个被证明的 NP 完全问题,成为后续所有 NP 完全性证明的归约源头,是理论体系的锚点。

问:该定理解决了 P 是否等于 NP 吗?答:没有。它只确立了 NP 完全性的存在,P 与 NP 是否相等至今仍是未解难题。