1. 概述
布尔可满足性问题（SAT）是第一个被证明是 NP-Complete 的问题。本文中我们将深入探讨 SAT 问题，并介绍 Cook-Levin 定理。
我们还将讨论 3-SAT 问题，并展示如何通过将其归约到 SAT 问题来证明它也是 NP-Complete。
2. SAT 问题简介
SAT 的核心问题是：给定一个布尔表达式，是否存在一组变量的真假赋值，使得该表达式为真？
举个例子：
| a | b | c | (a ∧ b) ∨ c | (a ∧ ¬a) ∨ (c ∧ ¬c) |
|---|---|---|---|---|
| 1 | 1 | 1 | 1 | 0 |
| 1 | 1 | 0 | 1 | 0 |
| 1 | 0 | 0 | 0 | 0 |
| 0 | 0 | 1 | 1 | 0 |
| 0 | 0 | 0 | 0 | 0 |
第一种表达式 (a ∧ b) ∨ c 有 5 种赋值使其为真，因此是可满足的；
第二种表达式 (a ∧ ¬a) ∨ (c ∧ ¬c) 对于所有赋值都为假，因此是不可满足的。
使用真值表法验证所有可能的变量组合，时间复杂度为 O(2ⁿ)，当变量数量较多时效率非常低。
3. 合取范式（CNF）
在讨论 SAT 问题时，合取范式（CNF） 是一个核心概念。
一个布尔表达式如果可以表示为多个子句的合取（AND），每个子句又是一个或多个文字（变量或其否定）的析取（OR），则称其为 CNF。
例如：
(a ∨ ¬b) ∧ (¬a ∨ b ∨ c)
其中每个子句如 (a ∨ ¬b) 是析取形式，整体是合取形式。
所有布尔表达式都可以通过 德摩根律、双重否定律 和 分配律 转换为 CNF 形式。
4. SAT 的变种
4.1. 2-SAT
每个子句最多包含两个文字的 SAT 问题。它可以在多项式时间内解决。
解决方法通常是通过构造有向图并寻找强连通分量（SCC），适用于如图的二分图判定、标签自动布局等场景。
4.2. 加权 2-SAT
给定一个每个子句含两个文字的 CNF，以及一个整数 k，判断是否存在最多 k 个变量为真的赋值使整个表达式满足。
这个问题是 NP-Complete，常用于顶点覆盖问题（Vertex Cover）建模。
4.3. 3-SAT
每个子句最多包含三个文字的 SAT 问题，是 NP-Complete。
它是 Karp 的 21 个 NP-Complete 问题之一，常用于归约证明其他问题的复杂度。
4.4. 精确 3-SAT（Exactly One 3-SAT）
要求每个子句中恰好一个文字为真，其余为假。该问题同样是 NP-Complete，常用于归约证明。
5. Cook-Levin 定理
Cook-Levin 定理指出：布尔可满足性问题是 NP-Complete。
换句话说：
✅ SAT ∈ NP
✅ 所有 NP 问题都可以在多项式时间内归约到 SAT
因此 SAT 是 NP-Complete。
5.1. 证明思路
- 任何 NP 问题都可以由一个非确定型图灵机在多项式时间内解决。
- 给定一个输入，可以构造一个布尔电路来模拟该图灵机的执行过程。
- 电路输出为真 ⇔ 存在一个输入使问题为“是”。
- 电路可以转换为 CNF 形式，等价于 SAT 问题。
逻辑门的 CNF 表达
AND 门
(a ∧ b) → x的 CNF：(¬x ∨ a) ∧ (¬x ∨ b) ∧ (¬a ∨ ¬b ∨ x)OR 门
(a ∨ b) → x的 CNF：(¬x ∨ a ∨ b) ∧ (¬a ∨ ¬b ∨ x)NOT 门
x ↔ ¬a的 CNF：(a ∨ x) ∧ (¬a ∨ ¬x)
通过这些转换，可以将任意电路转换为 CNF，从而归约到 SAT。
6. 3-SAT 简介
3-SAT 是 SAT 的一个特例：每个子句最多包含三个文字，判断是否存在满足赋值。
虽然比 SAT 更受限，但目前仍没有多项式时间算法能解决它。
示例
原始 SAT 表达式：
φ = (x1 ∨ x2 ∨ ¬x4 ∨ ¬x5) ∧ (¬x1 ∨ x4 ∨ x5 ∨ ¬x6) ∧ (x6 ∨ x7) ∧ (¬x2 ∨ x3)
满足赋值为：
x1=1, x2=0, x3=0, x4=1, x5=0, x6=0, x7=1
将其转换为 3-SAT 形式：
φ' = (x1 ∨ x2 ∨ y1) ∧ (¬y1 ∨ ¬x4 ∨ ¬x5) ∧ (¬x1 ∨ x4 ∨ y2) ∧ (¬y2 ∨ x5 ∨ ¬x6) ∧ (x6 ∨ x7) ∧ (¬x2 ∨ x3)
引入新变量 y1, y2，使每个子句变为最多三个文字，结果仍可满足。
7. 3-SAT 的 NP-Complete 性质证明
要证明 3-SAT 是 NP-Complete，我们需要：
✅ 3-SAT ∈ NP
✅ 所有 NP 问题可以归约到 3-SAT
我们知道 SAT 是 NP-Complete，而 SAT 可以在多项式时间内归约到 3-SAT。
归约过程
假设一个子句有 m > 3 个文字：
C_r = a1 ∨ a2 ∨ a3 ∨ ... ∨ am
我们引入新变量 y，将其拆分为两个子句：
C'_r = (a1 ∨ a2 ∨ y) ∧ (¬y ∨ a3 ∨ ... ∨ am)
递归应用该过程，直到所有子句都变成最多三个文字。
等价性证明
我们证明 C'_r 和 C_r 是等价可满足的：
- 如果
C'_r满足，那么C_r也满足 - 如果
C_r满足，那么存在 y 的赋值使C'_r满足
因此，我们可以在多项式时间内将任意 SAT 归约到 3-SAT。
✅ SAT ∈ NP-Complete
✅ SAT ≤p 3-SAT
➡️ 3-SAT ∈ NP-Complete
8. 小结
- SAT 是最早被证明为 NP-Complete 的问题。
- Cook-Levin 定理是其理论基础。
- 3-SAT 是 SAT 的一个受限版本，也是 NP-Complete。
- 通过归约方法，我们可以将 SAT 转换为 3-SAT，并保留其可满足性。
这些理论是理解复杂度类 NP 和 NP-Complete 的基石，也为许多实际问题的难度分析提供了依据。