形式陈述
直觉
任何多项式时间非确定性计算都能编码成一个多项式大小的布尔公式;公式的满足赋值恰好描述一条接受计算历史。
例子与边界
定理证明一般 SAT 的完备性;对 2-SAT 等受限版本,问题可能属于 P。NP 完全不等于已证明需要指数时间,除非进一步证明
推论与应用
Cook–Levin 开启了 NP 完全性理论,后续可通过归约建立 3-SAT、团、顶点覆盖和哈密顿回路等问题的完备性。
参考资料
- Stephen A. Cook, “The Complexity of Theorem-Proving Procedures,” 1971.
- Leonid Levin, “Universal Sequential Search Problems,” 1973.
- Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach, §2.3.