定理已证明
库克–列文定理
命题陈述
布尔可满足性问题（SAT）是NP完全的：SAT属于NP类，且NP中的每一种语言都可以在多项式时间内归约到SAT。因此，若SAT能在多项式时间内求解，则 P = NP。
为什么成立?
NP问题正是那些候选解可以被快速验证、即便找到它们可能很难的问题。SAT——判定一个布尔公式是否可被满足——看起来只是众多具体谜题中的一个，但事实证明它是一台『万能翻译机』：任何多项式时间验证器对任何NP问题的任何候选解所做的计算，都可以逐步编码为一个布尔公式，该公式可满足当且仅当存在有效解。因此SAT至少和NP中的每个问题一样难。
证明思路
对任意语言 ，固定其多项式时间验证器对应的图灵机及运行时间的多项式界。将该机器在长度为 的输入上的整个计算过程编码为一个大型布尔变量网格，记录每个时间步、每个带格上所写的符号、读写头位置及机器状态。子句强制：每个格/步恰好一个符号/状态、初始构型正确、相邻时间步之间的转移规则正确、以及最终到达接受状态。这些子句的合取当且仅当存在一个接受计算——即当且仅当输入属于 ——时可满足，其规模是 的多项式，由此给出从 到SAT的多项式时间归约。
提出者
用到此定理的主题
相关定理
分步证明
该定理暂无分步证明。
参考文献
- Stephen A. Cook (1971). The complexity of theorem-proving procedures
- Michael R. Garey, David S. Johnson (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness