SAT 求解

1971 年，斯蒂芬·库克（Stephen Cook）证明了布尔可满足性问题（SAT）是 NP 完全的——这是计算机科学最重要的定理之一，为整个 NP 完全理论奠定了基础（库克因此获得 1982 年图灵奖）。SAT 的 NP 完全性意味着：如果 SAT 有多项式时间算法，则所有 NP 问题都有多项式时间算法，即 P = NP。

然而，2000 年代以来，工程意义上的 SAT 求解器（SAT Solver）在实际问题上取得了令人惊叹的成功。现代 SAT 求解器能在秒级内求解包含数百万个变量的工业级实例——尽管最坏情况下的复杂度依然是指数级。

问题定义#

布尔可满足性问题（Boolean Satisfiability Problem, SAT）：

给定一个布尔公式（由变量、AND、OR、NOT 构成），是否存在一组变量赋值使公式为真？

合取范式（CNF）：SAT 的标准输入形式。公式是多个子句（Clause）的合取（AND），每个子句是多个文字（Literal）的析取（OR），文字是变量或变量的否定。

例：$(x_1 \vee \neg x_2) \wedge (\neg x_1 \vee x_3) \wedge (x_2 \vee \neg x_3)$

库克-里文定理（Cook-Levin Theorem）证明了 3-SAT（每个子句恰好 3 个文字的 CNF SAT）是 NP 完全的，且所有 NP 问题都可以多项式归约到 SAT。

DPLL 算法：现代 SAT 求解器的基础#

1960-1962 年，戴维斯（Davis）、普特南（Putnam）、洛格曼（Logemann）和洛夫兰（Loveland）提出了 DPLL 算法：

DPLL(公式 F, 赋值 α)：
  单元传播：若某子句只剩一个文字，强制赋值该文字
  纯文字消去：若某变量只以正（或负）形式出现，直接赋值
  若 F 已满足：返回 SAT
  若 F 含空子句（矛盾）：返回 UNSAT
  选择未赋值变量 x
  return DPLL(F[x=true], α ∪ {x=T}) or DPLL(F[x=false], α ∪ {x=F})
```

DPLL 是带剪枝的回溯搜索。单元传播（Unit Propagation）是其核心加速：当一个子句只剩一个文字时，该文字的值被强制确定，可以触发连锁传播，大幅减少搜索空间。

CDCL：现代工业级 SAT 求解器#

2000 年代，冲突驱动的子句学习（Conflict-Driven Clause Learning, CDCL）将 DPLL 提升为工业级求解器。关键创新：

冲突分析与子句学习：当搜索遇到矛盾时，分析冲突原因，从冲突中提取一个新的约束子句（Learned Clause），添加到公式中，避免以后再遇到相同的冲突。

非时序回跳（Non-Chronological Backtracking）：传统 DPLL 按顺序回溯；CDCL 根据冲突分析跳回引发冲突的决策点（可能跨越多个层次），大幅减少无效搜索。

启发式变量选择（VSIDS）：优先选择近期冲突中频繁出现的变量，统计实践表明这显著加速求解。

冲突分析的机制：CDCL 在传播过程中维护一张蕴含图（implication graph）：节点是变量赋值，边记录"哪个子句触发了这次传播"，按决策层（decision level）分层。冲突发生时，从冲突点沿图回溯，找到离冲突最近的唯一蕴含点（UIP，Unique Implication Point）——当前决策层上所有通往冲突的路径都经过它。沿 UIP 切开蕴含图，切口另一侧的文字组合起来就构成一个学习子句：它是原公式的逻辑推论（可由已有子句归结推出），加入公式不改变可满足性，却精确排除了刚踩过的那片搜索空间。学习子句还必须是断言子句（asserting）：回跳之后它立刻成为单元子句，强制传播出该 UIP 的反向赋值——这正是"非时序回跳"落点的由来。

为什么说学习是质变：DPLL 的失败记忆只存在于递归栈里，回退即遗忘；CDCL 把每次失败固化成一条全局有效的约束，搜索树的所有后续分支都受益。芯片验证这类实例会反复撞上结构相同的局部冲突，学到的子句把它们逐一排雷，搜索空间随学习过程持续收缩。

代表性求解器：MiniSat（Eén & Sörensson, 2003）、Glucose、Z3（微软研究院）、CaDiCaL。

SAT 的应用版图#

芯片制造是 SAT 最重要的工业应用之一。一块现代芯片包含数百亿个晶体管，验证其功能正确性不可能靠人工审查——SAT 求解器（以及与之结合的二元决策图 BDD、SMT 求解器）是形式化验证的核心工具。

SMT：超越 SAT#

可满足性模理论（Satisfiability Modulo Theories, SMT）将 SAT 扩展到更丰富的逻辑域：不只是布尔变量，还支持整数、实数、数组、位向量等，并将 SAT 求解器与各专用决策过程结合。

主流架构是惰性（lazy）的 DPLL(T)：把公式里的理论原子（如 $x + y \leq 3$）先当成普通布尔变量，交给 SAT 求解器求布尔骨架的赋值；理论求解器再检查这组赋值在理论内部是否自洽。若冲突，理论求解器返回一条小小的"理论引理"子句，SAT 求解器把它当作学习子句继续搜索。布尔推理与理论推理各做擅长的事，通过子句学习这门公共语言交换信息——CDCL 的架构红利再一次被复用。

SMT 求解器（如 Z3、CVC5）是程序验证、符号执行、软件分析的基础工具，也是 Lean、Coq 等定理证明器的底层引擎之一。

DPLL 到 CDCL 的历史演化#

1960 年代的 DPLL 算法在当时的计算机上能处理几十个变量的实例。随后三十年，SAT 研究基本停滞——理论上是 NP 完全的，似乎没有工程突破的空间。

转折点是 1990 年代末。GRASP（Marques-Silva & Sakallah, 1996）首次在完整求解器中实现了非时序回跳和子句学习的组合，展示了在工业基准上的巨大性能提升。随后的 Chaff 求解器（Moskewicz et al., 2001）引入了 VSIDS 启发式和两文字监视（Two-Watched Literals）数据结构，将单位传播的代价从 $O(n)$ 降至接近 $O(1)$ 的摊销代价。

两文字监视（Two-Watched Literals）是现代求解器中最重要的工程细节：对每个子句只监视其中两个文字。只要还有一个被监视的文字未赋值或为真，这个子句就不可能触发传播，求解器什么都不用做。只有当某个被监视的文字被赋假时才检查该子句：能找到另一个未赋值的文字，就换它顶替监视位；找不到，说明子句已单元化（触发传播）或已冲突。

这个结构最精妙的一点是回溯时零开销：撤销赋值不需要恢复任何监视状态——监视文字只朝"未赋值"方向移动，回退后原来的监视关系依然合法。相比之下，早期实现（给每个文字维护出现位置链表）在每次回溯时都要回滚大量指针。在每秒传播数百万次的求解器里，这个差别就是数量级的性能差距（Chaff，2001）。

SAT 求解的工程奇迹#

现代 CDCL 求解器能处理工业级实例（数百万变量和子句），这在 1990 年代几乎不可想象。核心进展来自多个方向的协同：

子句学习的力量：一次冲突学习的子句可以被未来的搜索重复使用——求解器在搜索树的不同分支中"积累智识"，对同类型问题越来越熟练。对于结构化问题（如芯片验证），学习到的子句是全局有效约束，大幅压缩搜索空间。

随机重启（Random Restart）：若当前搜索没有进展，放弃并以不同随机决策顺序重新开始，保留已学习的子句（智识不清空）但改变探索方向。这打破了搜索路径的局部陷阱，实验证明大幅提升平均性能。

现代 SAT 竞赛：每年举行的 SAT 竞赛（SAT Competition）是推动求解器发展的关键机制——来自学术界和工业界的团队在标准测试集上竞技，持续推动状态最优（State of the Art）边界前进。Glucose、CaDiCaL 等求解器在竞赛中崛起，随后被工业界采用。

为什么工业实例大多可解：结构的胜利#

理论上 SAT 是 NP 完全的，实践中百万变量的实例却常被秒解。调和这两个事实的关键是：工业实例不是随机实例。

2012 年，Ansótegui、Giráldez-Cru 与 Levy 用复杂网络的工具分析工业 SAT 实例的变量关联图，发现它们具有显著的社区结构（community structure）：变量聚成若干内部紧密、之间稀疏的模块——这正是芯片电路按模块设计、软件按函数组织在公式上的投影。CDCL 的两大引擎恰好都在利用这种结构：VSIDS 把搜索集中在冲突密集的少数社区内；学到的子句大多是社区内部的局部约束，短小且可复用。随机公式没有任何模块可寻，VSIDS 与子句学习的威力随之失效——这解释了为什么相变点附近的随机 3-SAT 至今能难倒最好的求解器。

学习子句也不是越多越好——无限囤积会拖慢传播。Glucose 求解器（Audemard 与 Simon，2009）提出用 LBD（Literals Blocks Distance，子句中不同决策层的个数）度量学习子句的质量：跨越决策层越少的子句越"通用"，LBD ≤ 2 的所谓"胶水子句"被永久保留，其余定期清理。这个简单的启发式显著提升了求解器在工业基准上的表现，此后成为主流求解器的标配。

代价与争议#

最坏情况指数：工程上的成功不改变理论困难性。精心构造的随机 3-SAT 实例（相变临界点附近的实例）即使现代求解器也无法在合理时间内求解。

相变现象：随机 3-SAT 存在"相变"——子句数与变量数之比约为 4.267 时，问题从"几乎总是可满足"跳变到"几乎总是不可满足"，且相变点附近的实例最难求解。这个现象连接了统计物理与计算复杂度，是理论计算机科学的活跃研究方向。

P vs NP：SAT 的 NP 完全性意味着它是 P vs NP 这一千禧年大奖难题的核心（见 computational-complexity）。证明 SAT 没有多项式时间算法，就证明了 P ≠ NP。目前两个方向（P = NP 或 P ≠ NP）都没有被证明。

跨域连接#

• 计算复杂性：SAT 的 NP 完全性意味着最坏情况指数，而工业实例常在秒级解决，这两件事不矛盾。结论只能是：真实实例不是最坏实例——它们带有大量结构，子句学习正是把这些结构提炼成可复用的约束。复杂度谈的是分布上的上确界，不是你手里的那个输入。
• 自旋玻璃：随机实例的难度随子句与变量之比变化，在某个比值附近从几乎总可满足跳到几乎总不可满足，最难的实例聚在这条临界带上。统计物理由此给出了"难在哪里"的坐标，也提醒了基准构造者：比值取偏，生成的测试就太容易。
• 逻辑：冲突分析学到的每条子句都是从已有子句归结出来的，所以搜索过程同时在构造一份证明：不可满足的输出可以附带一份可独立检查的反驳。这把求解器从黑箱变成了可审计的推理器，也是它敢被用在安全论证里的原因。
• 形式化方法与验证：有界模型检验把"电路或程序在若干步内是否违反规约"整体编码成一个巨大的布尔公式，交给通用求解器。这条路线的价值在于分工：领域专家只负责把问题编码成子句，求解器的进步自动惠及所有领域。
• 基因测序：把生物学约束写成子句，单倍型推断这类组合问题也可以交给通用求解器，而不必为它单独写一套专用算法。这体现了归约的实际收益：一旦某个问题能被翻译成 SAT，它就自动接上了数十年积累的工程优化。

参考文献#

• Cook, S. A. The Complexity of Theorem-Proving Procedures. STOC 1971, pp. 151–158.
• Davis, M., Logemann, G. & Loveland, D. A Machine Program for Theorem-Proving. CACM 5(7), 394–397 (1962).
• Marques-Silva, J. & Sakallah, K. GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers 48(5) (1999): 506–521.
• Moskewicz, M. et al. Chaff: Engineering an Efficient SAT Solver. DAC 2001. （VSIDS 与两文字监视的出处）
• Audemard, G. & Simon, L. Predicting Learnt Clauses Quality in Modern SAT Solvers. IJCAI 2009: 399–404. （LBD 的出处）
• Ansótegui, C., Giráldez-Cru, J. & Levy, J. The Community Structure of SAT Formulas. SAT 2012, LNCS 7317: 410–423.
• Eén, N. & Sörensson, N. An Extensible SAT-Solver. SAT 2003. LNCS 2919, 502–518.
• Biere, A. et al. (eds.) Handbook of Satisfiability. 2nd ed. IOS Press, 2021.