DPLL 1962 — 把"逻辑判定"从内存爆炸救成栈式回溯

是什么

DPLL（Davis-Logemann-Loveland）是 1962 年三个人在 CACM 发的一篇 4 页论文，把两年前 Davis-Putnam（DP）那个会内存爆炸的 SAT 算法，改成了栈式回溯版本。

一句话说清楚改动：

DP 用”消变量”——把含 p 和含 ¬p 的子句两两组合（叫归结），子句数量可能平方级膨胀，几十个变量就把 1960 年代的内存吃光。 DPLL 改成”猜一边 + 错了回退”——选一个变量 v，先假设 v=真，沿着推进；矛盾就退回来改成 v=假。整条搜索路径只占一个栈的空间。

这个改动看着像微小工程优化，但它是今天每一个工业 SAT 求解器（MiniSat / Glucose / CaDiCaL / Z3 内核）的骨架。1962 年那 4 页画的回溯流程图，2026 年的求解器主循环只是它的”加学习子句、加启发式”版本。

为什么重要

不理解 DPLL 的回溯结构，下面这些事都说不清：

为什么 cargo build 解决依赖冲突有时跑很久——DPLL 风格的回溯在最坏情况下指数
为什么 MiniSat 600 行就能教学——主循环就是 DPLL，剩下都是工程包装
为什么 CDCL（1996）说自己是”DPLL + 学习” 而不是另起炉灶——它真的只在 DPLL 上加了一个动作
为什么 Z3 验证一行代码可能秒过、可能跑半小时——DPLL 树的形状对实际输入极敏感

核心要点

DPLL 的伪代码可以缩到 6 行：

DPLL(F):
  F = unit_propagate(F)
  F = pure_literal_eliminate(F)
  if F 已空 → 可满足
  if F 含空子句 → 不可满足
  选一个未赋值变量 v
  return DPLL(F ∧ v) or DPLL(F ∧ ¬v)

三个动作：

单元传播（Unit Propagation）：某子句只剩一个文字 p，那 p 必须为真——立刻赋值，把所有含 p 的子句删掉（已满足），所有含 ¬p 的子句里把 ¬p 划掉（继续推下一轮）。
纯文字消除（Pure Literal）：变量 q 在剩下子句里只以正面出现（或只以负面），直接令它取那个方向，相关子句全删掉。
分裂（Split / Decide）：上面两步都不动了，挑一个变量 v，先递归 v=T；这一支返回”不可满足”就回溯改试 v=F。

注意：第三步的 or 是短路——左边一旦说”可满足”就立刻返回，不管右边。

回溯本身不需要重新存一份 F：在 1962 年的实现里，赋值变化用一个栈记录，回退就是 pop 到上一个决策点。这是和 DP 最关键的差别——空间从指数变成线性。

实践案例

案例 1：手算一题，看回溯发生

(a ∨ b) ∧ (¬a ∨ c) ∧ (¬b ∨ ¬c) ∧ (¬a ∨ ¬c)

逐步走：

没有单元也没有纯文字 → 进入分裂
选 a，先试 a=T
单元传播：(¬a ∨ c) 变 (c) → c=T；(¬a ∨ ¬c) 变 (¬c) → 矛盾 ✗
回溯：撤销 a=T、c=T，改试 a=F
单元传播：(a ∨ b) 变 (b) → b=T；(¬b ∨ ¬c) 变 (¬c) → c=F
全部子句已满足 → 可满足：a=F, b=T, c=F

整个过程从一次错误猜测里只回退一步就找到答案。这就是 DPLL 比 DP 高效的关键——失败局部化，不污染整个状态。

案例 2：DP 和 DPLL 的真实差异（不是同一个算法）

很多教材把两者并称”DPLL”，但 1960 年 DP 和 1962 年 DPLL 的内部行为完全不一样：

项	DP 1960	DPLL 1962
消变量手段	归结（resolution）	分裂 + 回溯
空间复杂度	子句数最坏指数	决策栈线性
1960 年代实战上限	~20 变量	~200 变量
现代后裔	几乎无（归结只在预处理）	MiniSat / CaDiCaL 全家桶

CDCL（1996）就是 DPLL 加一条：“冲突时不只是回退，还学一条新子句记下这个区域不能再去”。

案例 3：为什么单元传播是最重要的优化

研究测出现代 SAT 求解器90% CPU 时间花在单元传播上——不是分裂，不是学习，就是这个最朴素的步骤。

原因：每次决策一个变量，往往会触发链式单元传播——一个变量定下来，几个子句变成单元，再定下几个，再触发更多。一个分裂可能瞬间确定几百个变量。

工程优化（watched literals, Moskewicz 2001）让单元传播的均摊代价是 O(1)。这是 SAT 求解器从”几千变量”跳到”百万变量”的真正功臣，而不是更聪明的启发式。

案例 4：在你电脑里 DPLL 在哪儿

cargo build / npm install：版本约束 → SAT → DPLL/CDCL 求解（PubGrub 是它的优化变体）
Z3 验证 assert(x + 1 > x)：把溢出条件编成 SAT，DPLL 内核搜索反例
Intel/AMD 芯片设计：每条 RTL 用 BMC（Biere 1999）展开成 SAT，调 DPLL 检查
KLEE 符号执行：每条路径约束送 SAT 求解器决定可达性
Sudoku 数独应用：内部就是把 729 个 0/1 变量编成 SAT 求解

每次你按回车，背后都有一个 DPLL 的曾孙在跑回溯。

踩过的坑

变量选择顺序决定生死：朴素 DPLL 按字典序选变量，一个不好的顺序会让搜索树膨胀 100 倍。zChaff 2001 引入 VSIDS 启发式（按变量在最近冲突里出现频率打分），是 DPLL 走向工业的关键。
纯文字规则在工业 SAT 里几乎不用：维护”某变量只以正面出现”需要扫所有子句，开销大于收益。教材还在讲，CaDiCaL 这类 SOTA 已经只在预处理时用一次。
没有学习的 DPLL 会反复掉进同一个坑：纯回溯不记录”这条路死过”——同一个矛盾会在搜索树不同位置触发。CDCL 加的”冲突子句学习”正是补这个。
递归实现栈会爆：变量数超几千的实例不能用真递归，要写显式决策栈 + 迭代。这是早期实现的常见翻车点。
不要把 DP 和 DPLL 混为一谈：面试题里问”DP 算法”经常被答成”DPLL”——它们是两个不同的算法，1960 那篇用归结，1962 这篇才是回溯。

适用 vs 不适用场景

适用：

命题可满足性（SAT）—— DPLL/CDCL 是黄金路径
离散组合搜索（数独、调度、依赖解析、图着色）
SMT 求解器的布尔骨架层（Z3 / CVC5）

不适用：

一阶逻辑带量词的完全判定 → 半判定问题，需 Herbrand 展开 + DPLL 当子程序
实数 / 非线性约束 → SAT-modulo-Theories 的 Theory 层（DPLL 只管布尔骨架）
优化问题（找最优而不是判定可满足） → MaxSAT / MIP
概率推理 → DPLL 不擅长，用 #SAT / Bayesian 方法

历史小故事（可跳过）

1960：Davis-Putnam JACM 论文，归结消变量。理论漂亮，工程不行。
1962：Davis 找 NYU 学生 Logemann、Loveland，写了一个实际能在 IBM 704 上跑的版本——这就是 DPLL，CACM 4 页。
1971：Cook 证明 SAT 是 NP-完全——给 DPLL 的最坏指数复杂度盖了帽。
1996：Marques-Silva 在 GRASP 求解器引入 CDCL——DPLL 历史最大升级。
2001：Moskewicz 等人写出 zChaff/Chaff——VSIDS + watched literals，第一次跑 100 万变量级。
2003：Eén & Sörensson 写 MiniSat，600 行，成为后来所有教材的参考实现。
2017+：CaDiCaL（Biere）成为新 SOTA，仍是 DPLL 主干。

从 1962 年那 4 页 CACM，到 2026 年百万行的 SMT 求解器，栈式回溯这个核心从未改变。

学到什么

算法演化常常不是”换思路”，而是”换数据结构”：DP → DPLL 没换问题，没换规则，只把”消变量”换成”决策栈”，立刻把空间从指数压成线性。
简单算法 + 工程打磨 > 复杂算法：DPLL 主循环 4 行；让它快的所有工作（VSIDS / watched literals / 学习子句 / 重启策略）都是外围工程，主干没动。
理论可判定 ≠ 工程可解：SAT 是 NP-完全，最坏指数；但工业上 1000 万变量也跑得动——靠的是输入结构友好 + 学习剪枝。
一篇 4 页论文可以管 60 年：DPLL 1962 的回溯结构，今天的 CaDiCaL / Z3 还在用。

关联

davis-putnam-1960 —— DP 是 DPLL 的前身；DPLL 把归结换成回溯
biere-bmc-1999 —— BMC 把硬件设计展开成 SAT 让 DPLL 跑
clarke-cegar-2003 —— CEGAR 抽象细化在每轮调一次 SAT 求解器
cook-levin —— 证明 SAT 是 NP-完全，给 DPLL 复杂度盖帽
hoare-logic —— 程序验证目标；条件常被翻成 SAT 由 DPLL 后裔自动处理

反向链接

biere-bmc-1999 —— Bounded Model Checking — 把硬件验证翻译成一道 SAT 题
chaff-2001 —— Chaff 2001 — 把 CDCL 工程化的两个杀手锏
clarke-cegar-2003 —— CEGAR — 用反例自动改进抽象，让大软件能被验证
cook-levin —— Cook-Levin 定理 — NP-完全性的诞生
davis-putnam-1960 —— Davis-Putnam 1960 — 让机器自动判断一堆逻辑式能不能同时成立
hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
marques-silva-grasp-1996 —— GRASP 1996 — 让 SAT 求解器从冲突里学到东西
minisat-2003 —— MiniSat 2003 — 600 行 C++ 把 CDCL 写成教科书
nelson-oppen-1979 —— Nelson-Oppen 1979 — 让多个判定程序坐下来交换”我刚发现 a=b”
nieuwenhuis-dpll-t-2006 —— Nieuwenhuis-Oliveras-Tinelli 2006 — 给 SMT 求解器写一套数学规则书