Davis-Putnam 1960 — 让机器自动判断一堆逻辑式能不能同时成立

是什么

Davis-Putnam（DP）是史上第一个真正能在计算机上跑的”逻辑判定算法”。它解决一个看起来很学术、但其实每天发生在你电脑里的问题：

给我一堆”或”和”非”拼起来的命题（比如 (a ∨ ¬b) ∧ (b ∨ c)），有没有一组真假赋值能让它们全部同时为真？

这个问题叫 SAT（可满足性问题）。日常类比：你有 30 条互相冲突的”必须”和”不能”约束，问是否存在一种安排满足所有人。

DP 1960 给出了一个机械化、不靠灵感的判定流程。它后来演化出 DPLL（1962）、CDCL（1996）、现代 MiniSat / CaDiCaL / Z3——也就是说，今天每一个 SAT/SMT 引擎都是它的曾曾孙。

为什么重要

不理解 DP，下面这些事都不对劲：

为什么 Z3 能秒证某个智能合约不会溢出——它内核是 SAT 求解器
为什么 Cargo 解决依赖冲突有时几毫秒、有时跑半天——遇到的就是 SAT 难例
为什么 Intel 芯片每条指令都被验证过没 bug——靠 BMC（Biere 1999）+ SAT
为什么 TypeScript 类型推不出来有时报”too complex”——背后是 SAT 风格搜索

DP 是这条 65 年技术链的起点。

核心要点

DP 处理的是合取范式（CNF）——一堆”子句”用 ∧ 串起来，每个子句是一堆”文字”用 ∨ 串起来。文字 = 变量或它的否定。例：

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

DP 把上面这堆反复施三条规则化简，直到要么得出”显然可满足”要么”显然矛盾”：

重言式规则（Tautology）：某子句里同时出现 p 和 ¬p，那它永远为真——直接划掉这条子句。
单元规则（One-Literal / 单元传播）：某子句里只剩一个文字 p，那 p 必须为真——把所有含 p 的子句删掉（已满足），把所有含 ¬p 的子句里的 ¬p 划掉（永远为假，留下其他文字）。
纯文字规则（Pure Literal）：某变量在整个式子里只以正面出现（或只以负面出现），直接赋成对应的真假，把含它的子句全删掉。

三条规则都不动了？选一个变量做”消去”——原版 DP 用归结（resolution）枚举出 p = true 和 p = false 两个分支再合并。这一步是后来内存爆炸的根源。

实践案例

案例 1：用三条规则手算一题

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

逐步推：

第三条 (a) 是单元 → a 必须真
单元规则化简：含 a 的子句删掉，剩 (c) ∧ (¬c ∨ d)
(c) 是单元 → c 真，化简成 (d)
(d) 是单元 → d 真
全部子句消失 → 可满足，赋值 a=T, c=T, d=T，b 任意

整个过程没猜任何东西，纯机械传播。这就是单元传播为什么是现代 SAT 求解器90% 时间在做的事。

案例 2：DP 跟 DPLL 的关系

很多人把 “DP” 和 “DPLL” 混为一谈，其实不一样：

DP 1960：消变量用归结（resolution）——把含 p 的子句和含 ¬p 的子句两两组合。问题：子句数量可能指数爆炸。
DPLL 1962（Davis-Logemann-Loveland）：把”消变量”换成”猜一边 + 错了回溯”。内存可控。今天工业 SAT 全用 DPLL 路线。

所以你在工程里碰到的”DPLL”，本质是 DP 的剪枝版本。

案例 3：你电脑里它在哪里

cargo build 解决版本冲突 → 转化成 SAT
Z3 验证 assert(x + 1 > x) 不会溢出 → 内核 SAT
Biere 的 BMC 把”程序在 k 步内不会崩”翻译成 SAT
调度算法 / 课表生成 / 数独 → 全都是 SAT 实例

每次你按下回车，背后大概率有一个 DP 的曾孙在干活。

案例 4：为什么纯文字规则常常划掉一大片

考虑：

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

变量 a 在每个子句里都是正面出现，从来没出现 ¬a——这就是”纯文字”。直接令 a = T，三条子句全部满足，剩下一个空集 → 可满足。直觉是：没有反对意见的变量，让它顺它的方向就行，没必要”猜两边”。

踩过的坑

DP 的归结消变量真的会内存爆炸：1960 年代纸带机上跑不了几个变量。这是 1962 年改成 DPLL 的直接动机。
“Quantification Theory” 不是命题逻辑：论文标题是”一阶逻辑判定”，DP 先用 Herbrand 展开把一阶逻辑（带 ∀∃）展成命题序列，再 SAT。但 Herbrand 可能展无穷——所以 DP 对一阶逻辑只是半判定（semi-decidable），不是完全判定。只有纯命题片段保证终止。
三条规则的顺序不影响正确性，但严重影响速度：现代实现优先单元传播（最便宜），然后才考虑分裂。
纯文字规则在现代 CDCL 里很少用：维护”某变量只以正面出现”的开销大于收益。教科书还在讲它，工业代码已经不用了。

适用 vs 不适用场景

适用：

命题可满足性（SAT）—— DP/DPLL 是黄金路径
一阶逻辑的”无量词片段” + 等式 —— 经 SMT 求解器扩展
离散组合搜索（数独、调度、依赖解析）

不适用：

含实数、积分、超越函数的连续约束 → 用数值方法 / 区间分析
需要构造性证明的高阶逻辑 → Coq / Lean
优化问题（不是判定，要找最优解）→ MIP / SAT-MaxSAT 扩展
概率推理 → Bayesian 网络 / MCMC

历史小故事（可跳过）

1960 年：Martin Davis 和 Hilary Putnam（哲学家！）在 JACM 发表 DP 算法。当时计算机内存只有几 KB，他们用 IBM 704 跑了几道题。
1962 年：Davis 找学生 Logemann、Loveland 改进，把归结换成回溯分裂——这就是后来全行业用的 DPLL。
1996 年：Marques-Silva 引入 CDCL（冲突驱动子句学习）——求解器从冲突中”学”新约束，不再走重复的死路。
2001 年：Chaff/zChaff 横空出世，处理 百万变量级 SAT 实例，催生现代硬件验证产业。
2010s：SMT 求解器 Z3 把 SAT 包成核心，套上整数、数组、字符串理论，成为程序验证的瑞士军刀。

从 1960 那篇 12 页论文到今天 GitHub 上 5 万行的 CaDiCaL，主干思路没变。

学到什么

SAT 是离散问题里的”通用语”——任何离散判定都能编码成 SAT，所以一个好 SAT 求解器解决一大类问题
单元传播是核心引擎：占现代 SAT 求解器 90% 运行时间，论文里就是 One-Literal Rule
理论可判定 ≠ 工程可解：SAT 是 NP-完全（Cook-Levin 1971 证明），最坏指数；但工程上 1000 万变量也跑得动——靠的是结构利用 + 学习
算法演化是”换数据结构”的故事：DP → DPLL（换搜索结构）→ CDCL（加学习子句）→ Watched Literals（换传播表示）

关联

biere-bmc-1999 —— BMC 是 DP/DPLL 在硬件验证的核心应用
cook-levin —— Cook-Levin 1971 证明 SAT 是 NP-完全，为 DP 的”为啥可能慢”给了理论上限
hoare-logic —— 程序验证的另一条路；DP/SAT 是它的自动化引擎
lamport-tla-1994 —— TLA+ 用 SAT/SMT 检查时序规范
hindley-milner —— 类型推导内核也是 SAT 风格的约束求解

反向链接

biere-bmc-1999 —— Bounded Model Checking — 把硬件验证翻译成一道 SAT 题
chaff-2001 —— Chaff 2001 — 把 CDCL 工程化的两个杀手锏
cook-levin —— Cook-Levin 定理 — NP-完全性的诞生
dpll-1962 —— DPLL 1962 — 把”逻辑判定”从内存爆炸救成栈式回溯
hindley-milner —— Hindley-Milner — 编译器自己猜变量类型
hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
lamport-tla-1994 —— TLA — 把状态机和时序逻辑捏成一个公式
li-t-closeness-2007 —— t-Closeness — 用”分布距离”堵住匿名化的最后漏洞
marques-silva-grasp-1996 —— GRASP 1996 — 让 SAT 求解器从冲突里学到东西
minisat-2003 —— MiniSat 2003 — 600 行 C++ 把 CDCL 写成教科书
proverif-2001 —— ProVerif — 把密码协议翻成 Prolog 规则让计算机自己证安全