库克-莱文定理或库克定理

在计算复杂性理论中，库克-莱文定理，也称为库克定理，指出布尔可满足性问题是 NP 完全的。也就是说，它在 NP 中，并且 NP 中的任何问题都可以通过确定性图灵机在多项式时间内简化为布尔可满足性问题。

Stephen Arthur Cook 和 LA Levin 在 1973 年独立证明了可满足性问题（SAT）是 NP 完全的。斯蒂芬库克在 1971 年发表了一篇题为“定理证明程序的复杂性”的重要论文，其中他概述了通过将 NP 完全问题简化为SAT来获得证明的方法。他证明了Circuit-SAT和3CNF-SAT问题与SAT一样难。同样，列昂尼德·莱文在当时的苏联独立研究了这个问题。由于这两位科学家的努力， SAT是 NP-complete 的证据得到了证明。后来，Karp 将 21 个优化问题，例如 Hamiltonian tour、vertexcover和 clique 简化为SAT ，并证明这些问题是 NP 完全的。

因此，一个 SAT是一个重要的问题，可以表述如下：

给定一个布尔表达式F具有n 个变量x ₁ ,x ₂ ,....,x _n和布尔运算符，是否可以对变量进行赋值 true 或 false 使得二进制表达式F为 true？

这个问题也被称为公式 - SAT 。 SAT（公式-SAT 或简单的 SAT）采用布尔表达式 F 并检查给定的表达式（或公式）是否可满足。如果评估结果为真，则认为布尔表达式对于一些有效的变量赋值是令人满意的。在讨论 SAT 的细节之前，让我们现在讨论一些布尔表达式的重要术语。

布尔变量：一个变量，比如x ，只能有两个值，真或假，称为布尔变量
字面量量：字面量量可以是一个逻辑变量，比如x ，或者它的否定，即x或x̄ ； x称为正字面量量， x̄称为负字面量量
子句：可以由逻辑OR运算符分隔的变量序列（x ₁ ,x ₂ ,….,x _n ）称为子句。例如， (x ₁ V x ₂ V x ₃ )是三个字面字面量的子句。
表达式：可以使用布尔运算符组合前面的所有子句以形成表达式。
CNF 形式：如果子句集由AND (^), 运算符分隔，而字面量由OR (v) 运算符连接，则表达式为 CNF 形式（合取范式）。以下是 CNF 形式的表达式示例：
- f = (x ₁ V x̄ ₂ V x ₃₎ ∧ (x ₁ V x̄ ₃ V x ₂ )
3 – CNF：如果表达式是合取范式，并且每个子句都具有精确的三个字面字面量，则称该表达式为 3-CNF。

因此， SAT是最棘手的问题之一，因为除了蛮力方法之外没有其他已知算法。蛮力算法将是指数时间算法，如2 ⁿ需要尝试可能的分配来检查给定的布尔表达式是否为真。 Stephen Cook 和 Leonid Levin 证明了SAT是 NP 完全的。

库克展示了 SAT 考试中其他难题的减少。 Karp 提供了 21 个重要问题的证明，例如 Hamiltonian tour、顶点覆盖和 clique，通过使用 Karp 约简将其简化为 SAT。

让我们简要介绍三种类型的 SAT。它们如下：

电路SAT：电路 SAT 可以表述如下：给定一个布尔电路，它是与、或和非等门的集合，以及n 个输入，是否存在布尔变量的任何输入分配，使得输出给定的电路是真的吗？同样，这些问题的困难在于电路的n 个输入。 2^个应检查可能的输出。因此，这种蛮力算法是指数算法，因此这是一个难题。
CNF-SAT：这个问题是SAT的一个受限问题，其中表达式应该是合取范式。如果所有子句都由布尔AND运算符连接，则称表达式为连词形式。就像SAT的情况一样，这是关于将真值分配给 n 个变量，以使表达式的输出为 true 。
3-CNF-SAT(3-SAT)：这个问题是另一个变体，其中额外的限制是表达式是合取范式，并且每个子句都应该包含三个字面字面量。这个问题也是关于将n个真值赋值给布尔表达式的n 个变量，使得表达式的输出为真。简单来说，给定 3-CNF 中的表达式，3-SAT 问题就是检查给定的表达式是否可满足。

这些问题可以用来证明一些重要问题的NP完全性。