什么是约束满足问题？

约束满足问题由一组变量、每个变量可能取值的值域，以及限制哪些取值组合被允许的约束组成。解就是给每个变量赋一个值，使所有约束都成立。地图着色、数独、排课和产品配置都是标准的例子。

什么是 SAT 求解器？

SAT 求解器是一种程序，用来判定一个布尔公式（通常写成合取范式的子句）能否被满足。如果能，求解器返回一个满足赋值；如果不能，它报告不可满足，许多求解器还能输出这一结论的证明。

什么是 SMT 求解器？

SMT 求解器判定可满足性模理论问题：它处理把布尔逻辑与算术、位向量、数组等理论混合在一起的公式。它把负责逻辑结构的 CDCL SAT 求解器与专门的理论求解器结合起来。Z3 和 cvc5 是广泛使用的例子。

DPLL 和 CDCL 有什么区别？

1962 年的 DPLL 通过单元传播、在变量上分裂以及按时间顺序回溯来搜索。1996 年在 GRASP 求解器中提出的 CDCL 加入了冲突分析：每次冲突都产生一条学到的子句，防止在别处重犯同样的错误，并且求解器直接跳回导致冲突的那个决策。

什么是弧相容？

两个变量之间的一条弧是相容的，当且仅当第一个变量值域中的每个值在第二个变量的值域中至少有一个相容的值。Alan Mackworth 于 1977 年发表的 AC-3 算法不断删除没有支持的值，直到每条弧都相容或某个值域变空。

既然 SAT 是 NP 完全的，它为什么还重要？

NP 完全意味着没有已知算法能在每个公式上都快，但来自硬件、软件和规划的真实公式具有子句学习可以利用的结构。现代求解器常常能判定含数百万子句的工业实例；而且由于 NP 中的每个问题都能翻译成 SAT，一个好的求解器可以服务于许多应用。

SAT 和 SMT 求解器算人工智能吗？

算，属于符号意义上的人工智能。它们源自 AI 中的自动定理证明和约束满足研究，并在显式的逻辑约束上进行精确推理。与机器学习模型不同，它们不从数据中学习，而它们的答案可以被独立检查。

SAT 和 SMT 求解器今天用在哪里？

它们用于硬件与软件验证、测试生成、调度与排课、自动规划、云访问策略分析、DNF、zypper 和 conda 等工具中的软件包依赖解析，也用于数学研究，例如 2016 年对布尔毕达哥拉斯三元组问题的求解。

符号 AI 技术 · 约束满足、SAT 与 SMT

约束满足、SAT 求解器与 SMT 求解器

符号 AI 中的这一族方法把问题写成变量和规则，然后搜索一组不违反任何规则的取值，或者证明这样的取值根本不存在。本文依次讲解约束满足问题、回溯与弧相容、基于 DPLL 和冲突驱动子句学习的布尔可满足性，以及 Z3 等 SMT 求解器：每一种如何工作、配有完整的推导实例、今天在哪里运行，又在哪里止步。

Perslis Research · 2026-09-26

约束满足（constraint satisfaction）是一种符号 AI 方法：把问题表述为若干变量、每个变量可取的值，以及取值组合必须遵守的约束，然后搜索一个满足全部约束的赋值。SAT 求解器对真/假变量做这件事；SMT 求解器在此之上加入算术、数组等理论。

一段话说清

约束问题只说明解应当是什么样子，寻找解的工作交给求解器。它的核心循环自 20 世纪 60 年代以来一直没有变：猜一个值，把它的后果沿着约束传播出去，剪掉已经不可能成立的选项，出现矛盾就退回。弧相容（Mackworth，1977）让一般约束满足问题中的传播变得系统化。对布尔公式，Davis–Putnam–Logemann–Loveland 过程（1962）做了同样的事；冲突驱动子句学习（GRASP，1996；Chaff，2001）又把它变成了今天能判定含数百万子句的工业公式的引擎。SMT 求解器让这台引擎去驾驭整数算术等更丰富的理论。这些问题一般是 NP 完全的，所以没有哪个求解器对一切输入都快；它们提供的是一个可以检查的答案：任何人都能验证的满足赋值，或者（越来越常见的）一份可由独立检查器验证的不可满足性证明。正因如此，这一角落成了符号 AI 中最受工业界信任的部分。

1. 约束满足问题及其求解方法

1.1 约束满足问题（CSP）

约束满足问题是由变量、值域和约束构成的三元组。这一表述源于 20 世纪 70 年代初的场景分析研究：David Waltz 在 MIT 的博士论文（1972 年完成，1975 年发表）为三维场景线图中的线条打标签，方法是反复删除相邻交点无法接受的标签[3]；Ugo Montanari 1974 年的《约束网络》（Networks of constraints）给出了一般的代数处理[2]。

定义（CSP）。约束满足问题是一个三元组

P = (X, D, C), X = {x_{1}, \dots, x_{n}}, D = {D_{1}, \dots, D_{n}}, C = {C_{1}, \dots, C_{m}}

其中每个变量

x_{i}

在其值域

D_{i}

中取值；每个约束

C_{j} = (S_{j}, R_{j})

由一个作用域

S_{j} \subseteq X

和一个关系

R_{j}

组成，后者列出它允许的取值组合。一个解是给每个变量赋值的赋值

σ

，使得

\forall i σ (x_{i}) \in D_{i} 且 \forall j σ | S_{j} \in R_{j} .

标准的教学例子是给澳大利亚地图着色，使相邻的两个区域颜色不同[1]。变量是七个区域 WA、NT、SA、Q、NSW、V 和 T；每个值域都是 {红, 绿, 蓝}；每一段共同边界对应一个约束 $A \neq B$ （WA–NT、WA–SA、NT–SA、NT–Q、SA–Q、SA–NSW、SA–V、Q–NSW、NSW–V）。一个解是 WA = 红、NT = 绿、SA = 蓝、Q = 红、NSW = 绿、V = 红、T = 红。数独、排课、人员排班、产品配置和八皇后问题都具有完全相同的形状。这种形式化的要义在于分工：建模者写下什么必须成立，通用求解器决定如何找到它。

局限。判定一个有限值域的 CSP 是否有解，一般是 NP 完全的（三色地图着色本身就是），所以任何完备求解器都会在某些输入上花费指数时间。普通 CSP 也没有“更好”的概念：偏好需要约束优化或加权约束之类的扩展。

1.2 回溯搜索

回溯是基本的完备算法：逐个给变量赋值；每次赋值后，检查所有变量都已赋值的约束；一旦违反，就撤销最近的选择，尝试下一个值。Solomon Golomb 和 Leonard Baumert 在《回溯编程》（Backtrack Programming，《ACM 期刊》，1965）中为这种方法命名并加以分析[6]。它的最坏情况是所有值域的完整乘积 $\prod_{i = 1}^{n} | D_{i} |$ ，因此实用的求解器加入了三类智能：

变量排序。优先选择剩余取值最少的变量（“最少剩余值”，即先失败原则），平局时选择与未赋值变量约束最多的那个。在澳大利亚地图上，WA = 红之后，NT 和 SA 都只剩两种颜色；接着选 SA（它与五个区域相邻）能最早暴露矛盾。
值排序。先尝试给邻居排除选项最少的那个值。
前瞻。Robert Haralick 和 Gordon Elliott 的前向检查（1980）在每次赋值后，删除每个未赋值邻居中与之冲突的所有值，这样一旦某个值域变空就立刻发现死路，而不必等到轮到那个变量。他们的论文提出了后来所有求解器都遵循的两条原则：先试最可能失败的地方；记住已经做过的事，避免重犯同一个错误[7]。

今天。每个约束规划求解器的内核仍是回溯搜索，外面包着传播（§1.4）。局限。按时间顺序的回溯总是退回最近的选择，即使失败是更早的选择造成的；这种“颠簸”正是 SAT 求解器中的冲突分析（§2.3）要避免的。

1.3 弧相容与 AC-3

弧相容（arc consistency）是最常用的局部相容性：一种廉价的检验，在搜索之前或搜索之中删除不可能出现在任何解中的值。Alan Mackworth 1977 年的论文《关系网络中的相容性》（Consistency in networks of relations）把结点相容、弧相容和路径相容定义为统一的一族，并给出了 AC-3 算法[4]。

定义（弧相容）。对于

x_{i}

与

x_{j}

之间关系为

R_{i j}

的二元约束，弧

(x_{i}, x_{j})

是弧相容的，当且仅当

x_{i}

的每个值都在

x_{j}

中有支持值：

\forall a \in D_{i} \exists b \in D_{j} : (a, b) \in R_{i j} .

当每条弧在两个方向上都弧相容时，这个 CSP 就是弧相容的。

AC-3 维护一个弧队列。它依次取出每条弧并调用 REVISE，删除 $D_{i}$ 中所有没有支持的 $a$ ；每当 $D_{i}$ 缩小，所有指向 $x_{i}$ 的弧 $(x_{k}, x_{i})$ 都重新入队，因为它们的支持值可能已经消失。如果某个值域变空，问题就无解。

在三个值域均为 {1, 2, 3}、约束为 A < B 与 B < C 的变量上运行 AC-3。仅靠传播就解出了问题。
步骤	修订的弧	删除的值	该步之后的值域
1	(A, B)	A = 3（没有大于 3 的 B）	A {1, 2} · B {1, 2, 3} · C {1, 2, 3}
2	(B, A)	B = 1（没有小于 1 的 A）	A {1, 2} · B {2, 3} · C {1, 2, 3}
3	(B, C)	B = 3（没有大于 3 的 C）	A {1, 2} · B {2} · C {1, 2, 3}
4	(C, B)	C = 1、C = 2	A {1, 2} · B {2} · C {3}
5	(A, B)，因 B 缩小而重新入队	A = 2	A {1} · B {2} · C {3}

现在每个值域只剩一个值，A = 1、B = 2、C = 3 就是解，全程没有任何猜测。在更难的问题上，弧相容只负责剪枝，其余交给搜索。设有 $e$ 个二元约束、值域大小至多为 $d$ ，AC-3 的运行时间为 $O (e d^{3})$ ，这是 Mackworth 和 Eugene Freuder 在 1985 年证明的[5]；后来的算法（从 AC-4 起）把它降到 $O (e d^{2})$ 。局限。弧相容是局部的：一个问题可以弧相容却依然无解（三个变量、值域都是 {红, 绿}、两两不同，它弧相容，却无解）。

1.4 约束传播

约束传播是 §1.3 背后的一般思想：用每个约束去缩小其变量的值域，让每一次缩小都触发共享这些变量的约束，直到什么都不再变化（不动点）或某个值域变空。更强的相容性级别用更多的计算换取更多的剪枝。Montanari（1974）引入了考虑变量三元组的路径相容[2]；Freuder（1978）把这一阶梯推广为 k 相容，并说明足够的相容性可以让搜索完全不需回溯[8]。

实践中最有用的一步是全局约束：作用于许多变量、拥有专门传播器的约束。alldifferent(x₁, …, x_n) 是经典例子。把它拆成 $n (n - 1) / 2$ 个单独的不等式，会漏掉“三个变量不可能共用两个值”这样的鸽巢论证；Jean-Charles Régin 1994 年的过滤算法利用二部图匹配，删除所有不可能出现在任何全不同赋值中的值[9]。用于调度（累积资源）、路径规划和装箱的全局约束，是约束规划在工业调度中具有竞争力的原因。局限。传播在设计上就是不完备的：它缩小搜索，而不是取代搜索；为多少传播付出代价，至今仍是经验问题。

1.5 局部搜索：最小冲突、GSAT 与 WalkSAT

完备搜索用来证明；局部搜索只求尽快找到一个解。它从一个违反若干约束的完整赋值出发，反复修改一个变量以减少违反的数量。Steven Minton、Mark Johnston、Andrew Philips 和 Philip Laird 的最小冲突启发式（AAAI-90）源自哈勃空间望远镜的观测排程，从良好的初始赋值出发，大约 50 次修复就能解出百万皇后问题[10]。对 SAT，Bart Selman、Hector Levesque 和 David Mitchell 的 GSAT（1992）每次翻转能使最多子句得到满足的那个变量[16]，WalkSAT（Selman、Henry Kautz 和 Bram Cohen）则加入随机的“噪声”步来跳出局部极小。局限。局部搜索是不完备的：它能找到解，但如果解不存在，它永远不会这样说。它无法证明不可满足，而这恰恰是验证者需要的答案。

1.6 约束逻辑程序设计

约束逻辑程序设计（CLP）把约束求解放进逻辑程序设计语言。Joxan Jaffar 和 Jean-Louis Lassez 的 CLP(X) 框架（POPL 1987）推广了 Alain Colmerauer 在 Prolog II 中引入的特性：一种以约束域 X 为参数的类 Prolog 语言，其中一部分原子是普通子句，另一部分是交给求解器的约束[11]。CHIP 由欧洲计算机产业研究中心（ECRC）的 Mehmet Dincbas、Pascal Van Hentenryck 等人开发，1988 年发表，是第一个实现有限域约束规划 CLP(FD) 的语言，并引入了全局约束[12]。

上面 A < B < C 问题的一个小 CLP(FD) 程序，读起来几乎就是它的规格说明：

solve([A,B,C]) :-
    [A,B,C] ins 1..3,     % 值域
    A #< B, B #< C,       % 约束：一经提交即传播
    label([A,B,C]).       % 对传播留下的部分进行搜索

今天。SWI-Prolog、SICStus Prolog 和 ECLiPSe 都带有有限域约束库；与求解器无关的建模语言 MiniZinc（Nethercote、Stuckey 等，2007）让同一个模型可以运行在许多约束、混合整数规划和 SAT 后端上[13]。CLP 把本页与逻辑程序设计与定理证明联系起来。局限。性能在很大程度上取决于模型的写法，而这是一门手艺；两个逻辑上等价的模型，速度可能相差几个数量级。

2. SAT：布尔可满足性与 SAT 求解器

2.1 SAT 问题

布尔可满足性（SAT）是变量取真/假的 CSP。公式通常以合取范式（CNF）给出：若干子句的“与”，每个子句是若干文字（一个变量或其否定）的“或”。问题是：是否存在某个赋值让每个子句都为真。SAT 是第一个被证明为 NP 完全的问题，由 Stephen Cook 在 1971 年证明，Leonid Levin 独立证明[14]；Richard Karp 1972 年的 21 个 NP 完全问题就是从它出发的。因此 NP 中的每个问题都能翻译成 SAT，这使得快速的 SAT 求解器成为通用工具：规划、调度、硬件等价性和软件包依赖都可以编码成子句。一些特例很容易：2-SAT（每个子句两个文字）可在多项式时间内求解，Horn 子句仅靠单元传播即可判定。

在随机生成的 3-SAT 公式上，难度在子句数与变量数之比约为 4.26 附近陡然达到峰值，公式在这里从几乎总是可满足转变为几乎总是不可满足[17]。相比之下，工业公式具有现代求解器能够利用的结构，所以求解器常常能解出比它们能解的任何随机公式都大得多的工业实例。

2.2 DPLL

Martin Davis 和 Hilary Putnam 在 1960 年发表了一个检验可满足性的过程，作为一阶逻辑证明方法的一部分[15]。它的变量消去步骤占用内存过多，1962 年 Davis、George Logemann 和 Donald Loveland 用分裂与回溯取代了它[18]。结果就是 DPLL，它至今仍是完备 SAT 求解器的骨架。它反复执行三步：

单元传播。如果一个子句除一个未赋值文字外其余文字都为假，那个文字就必须为真。给它赋值，然后重复；这就是 SAT 形式的约束传播。
纯文字消去。如果某个变量只以一种符号出现，就把它设为能满足这些子句的值。
分裂。否则选一个未赋值变量，试一个值并递归；如果由此得到一个空子句（所有文字为假），就回溯并尝试另一个值。

在五个变量、六个子句上的一次完整推演：

F = \underset{c_{1}}{\underset{⏟}{(a \lor b)}} \land \underset{c_{2}}{\underset{⏟}{(\neg a \lor c)}} \land \underset{c_{3}}{\underset{⏟}{(\neg c \lor d)}} \land \underset{c_{4}}{\underset{⏟}{(\neg a \lor \neg d)}} \land \underset{c_{5}}{\underset{⏟}{(\neg b \lor e)}} \land \underset{c_{6}}{\underset{⏟}{(\neg e \lor b)}}

在 F 上运行 DPLL。开始时没有单元子句，每个变量都以两种符号出现，所以求解器必须分裂。
步骤	动作	原因	当前赋值
1	决策 $a = 1$	分裂（第一个未赋值变量）	$a$
2	单元 $c = 1$	$c_{2}$ 化简为 $(c)$	$a, c$
3	单元 $d = 0$	$c_{4}$ 化简为 $(\neg d)$	$a, c, \neg d$
4	冲突	$c_{3}$ $= (\neg c \lor d)$ 的所有文字均为假	回溯到第 1 步
5	翻转 $a = 0$	分裂的另一分支	$\neg a$
6	单元 $b = 1$	$c_{1}$ 化简为 $(b)$	$\neg a, b$
7	单元 $e = 1$	$c_{5}$ 化简为 $(e)$	$\neg a, b, e$
8	纯文字 $c = 0$	在未满足的子句中 $c$ 只以 $\neg c$ 出现（在 $c_{3}$ 中）	$\neg a, b, e, \neg c$
9	可满足	所有子句均已满足； $d$ 自由（取 0）	模型 $σ = {a \mapsto 0, b \mapsto 1, c \mapsto 0, d \mapsto 0, e \mapsto 1}$

任何人都能把子句扫一遍来检查这个模型；寻找与检查之间的这种不对称，正是 NP 在实践中的含义。局限。朴素 DPLL 按时间顺序回溯，并且忘记分支失败的原因，因此可能在搜索树的许多地方重新发现同一个矛盾。

2.3 冲突驱动子句学习（CDCL）

冲突驱动子句学习治好了 DPLL 的健忘。当传播遇到冲突时，求解器分析为什么，把原因写成一个新子句，并直接跳回真正导致冲突的那个决策。João Marques-Silva 和 Karem Sakallah 在 GRASP 求解器中提出了它（ICCAD 1996；《IEEE 计算机汇刊》，1999）[19]，Roberto Bayardo 和 Robert Schrag（1997）也做了相关的回看技术工作[20]。Chaff（Moskewicz、Madigan、Zhao、Zhang 和 Malik，DAC 2001）让它变快：每个子句的两个监视文字让单元传播变得廉价，VSIDS 启发式则优先在近期冲突中出现过的变量上分支[21]。MiniSat（Niklas Eén 和 Niklas Sörensson，2003）把这一设计封装成一个小巧、可读的求解器，成为研究的标准底座[22]。重启（放弃当前分支，但保留学到的子句）补全了现代的配方。

在上面的推演中，第 4 步的冲突来自决策 $a$ ，经由 $c_{2}$ 、 $c_{4}$ 和 $c_{3}$ 。冲突分析按传播的逆序，把被证伪的子句与其各文字的原因子句做归结：

\begin{array}{l} \underset{冲突 c_{3}}{\underset{⏟}{(\neg c \lor d)}}, \underset{\neg d 的原因}{\underset{⏟}{(\neg a \lor \neg d)}} ⊢ (\neg a \lor \neg c) \\ (\neg a \lor \neg c), \underset{c 的原因}{\underset{⏟}{(\neg a \lor c)}} ⊢ (\neg a) 学到的子句 \end{array}

学到的子句 $(\neg a)$ 是 $F$ 的逻辑后承：无论其他变量如何， $a$ 都必须为假。CDCL 求解器把它加入子句库，回跳到第 0 层，把 $a = 0$ 当作事实传播，于是在任何分支里都不会再去探索 $a = 1$ 。图 1 画出了冲突分析所走的蕴涵图。

图 1. 冲突背后的蕴涵图。通往冲突的每条路径都始于决策 a = 1，所以 a 是唯一蕴涵点，学到的子句是 (¬a)。

今天。几乎所有有竞争力的完备 SAT 求解器（MiniSat 的后继者、CaDiCaL、Kissat 等）都是 CDCL，每个 SMT 求解器的布尔内核也是。局限。VSIDS 之类的启发式和重启策略是凭经验调出来的，所以在一类新公式上的表现难以预测；而且存在一些公式（例如鸽巢原理的编码），任何基于归结的方法（包括 CDCL）在上面都需要指数时间。

3. SMT 求解器

3.1 可满足性模理论（SMT）

可满足性模理论（satisfiability modulo theories）针对其原子属于某个背景理论的公式提出 SAT 问题：线性整数或实数算术、位向量（机器整数）、数组、未解释函数、字符串。有两个想法让它变得实用。Greg Nelson 和 Derek Oppen（1979）展示了如何通过在共享变量之间交换等式来组合不同理论的判定过程[23]。Robert Nieuwenhuis、Albert Oliveras 和 Cesare Tinelli 形式化的 DPLL(T) 架构（《ACM 期刊》，2006）让 CDCL SAT 求解器处理布尔结构，由理论求解器检查所选原子是否相容；不相容时，理论求解器返回一个解释，它就变成一条学到的子句[24]。

一个整数上的完整例子：

\underset{p_{1}}{\underset{⏟}{(x + y > 10)}} \land \underset{p_{2}}{\underset{⏟}{(x < 3)}} \land (\underset{p_{3}}{\underset{⏟}{y < 8}} \lor \underset{p_{4}}{\underset{⏟}{x > 5}}) ⇝ p_{1} \land p_{2} \land (p_{3} \lor p_{4})

SAT 求解器只看到右边的布尔骨架，提出 $p_{1}, p_{2}, p_{3}$ 。
算术求解器检查 $x + y > 10$ 、 $x \leq 2$ 、 $y \leq 7$ ：后两者给出 $x + y \leq 9$ ，矛盾。它返回解释，SAT 求解器学到 $\neg p_{1} \lor \neg p_{2} \lor \neg p_{3}$ 。
单元传播随即迫使 $\neg p_{3}$ ，进而迫使 $p_{4}$ 。理论求解器发现 $x < 3$ 与 $x > 5$ 不相容，SAT 求解器学到 $\neg p_{2} \lor \neg p_{4}$ 。
由于 $p_{1}$ 和 $p_{2}$ 必须为真，两条学到的子句同时排除了 $p_{3}$ 和 $p_{4}$ ，子句 $p_{3} \lor p_{4}$ 为假：不可满足。去掉约束 $x < 3$ ，求解器则会返回一个模型，例如 $x = 6, y = 5$ 。

求解器与标准。微软研究院 Leonardo de Moura 和 Nikolaj Bjørner 的 Z3（TACAS 2008）使用最广[25]；CVC4 的继任者 cvc5（2022）是另一个主要的开源求解器[26]；Yices、MathSAT 和 Bitwuzla 也在其列。始于 2003 年的 SMT-LIB 计划定义了通用的输入语言和基准库，同一个问题可以发给其中任何一个求解器。今天。SMT 求解器是 Dafny 等程序验证器（它把证明义务交给 Z3）、KLEE 等符号执行工具以及有界模型检测器中的推理引擎；参见形式化验证与程序综合。局限。一旦出现量词或非线性整数算术，可满足性就变得不可判定，求解器只能依靠可能回答“未知”或超时的启发式。

4. 约束、SAT 与 SMT 求解器今天用在哪里

调度、排课与排班。约束规划和局部搜索用来生成含有大量硬性规则（不得重复预订、休息时间、容量）和软性偏好的时间表。最小冲突最初就是为哈勃空间望远镜排程而生的[10]。
硬件验证。有界模型检测（Biere、Cimatti、Clarke 和 Zhu，1999）把电路展开 $k$ 步，询问 SAT 求解器坏状态是否可达[27]；基于 SAT 的等价性检查确认优化后的电路仍计算同一个函数。
软件验证与测试。Dafny 等验证器和 KLEE 等符号执行引擎把程序路径变成公式，询问 SMT 求解器某个断言能否失败；一个满足赋值就是一个具体的失败输入。
云安全策略。亚马逊云服务（AWS）把访问控制策略翻译成 SMT 公式，用求解器回答诸如“账户之外的任何人能否读取这个存储桶？”之类的问题（Zelkova 系统，FMCAD 2018）[28]。
软件包管理器。判定一组软件包能否同时安装是 NP 完全的，EDOS 项目在 2006 年针对 Debian 式依赖证明了这一点[29]。openSUSE 的 zypper 和 Fedora 的 DNF 用基于 SAT 的求解器 libsolv 解析依赖；conda 在 23.10 版（2023）把默认求解器换成基于 libsolv 的 libmamba 求解器，取代了建立在 PicoSAT SAT 求解器之上的旧求解器[30]。
规划。SATPlan 式的规划器把“是否存在长度为 $k$ 的计划？”编码成 SAT 公式；参见 AI 规划。
数学。2016 年，Marijn Heule、Oliver Kullmann 和 Victor Marek 用 SAT 求解器证明：1 到 7825 的整数无法分成两部分而使任何一部分都不含毕达哥拉斯三元组（1 到 7824 则可以），并用一份近 200 TB 的 DRAT 证明验证了这一结果[31]。

5. 时间线

约束满足、SAT 与 SMT 的主要里程碑。每一项都在参考文献中有出处。
年份	里程碑	人物
1960	检验可满足性的 Davis–Putnam 过程	M. Davis、H. Putnam
1962	DPLL：以分裂与回溯取代变量消去	M. Davis、G. Logemann、D. Loveland
1965	《回溯编程》	S. Golomb、L. Baumert
1971	SAT 是 NP 完全的（Levin 于 1973 年独立证明）	S. Cook
1972–75	用约束传播为线图打标签	D. Waltz
1974	约束网络；路径相容	U. Montanari
1977	弧相容与 AC-3	A. Mackworth
1978	k 相容	E. Freuder
1979	组合判定过程	G. Nelson、D. Oppen
1980	前向检查	R. Haralick、G. Elliott
1987	约束逻辑程序设计 CLP(X)	J. Jaffar、J.-L. Lassez
1988	CHIP：Prolog 中的有限域约束	M. Dincbas、P. Van Hentenryck 等（ECRC）
1990	最小冲突启发式修复	S. Minton、M. Johnston、A. Philips、P. Laird
1992	GSAT 局部搜索	B. Selman、H. Levesque、D. Mitchell
1994	基于匹配的 alldifferent 过滤	J.-C. Régin
1996	GRASP：冲突驱动子句学习	J. Marques-Silva、K. Sakallah
1999	基于 SAT 的有界模型检测	A. Biere、A. Cimatti、E. Clarke、Y. Zhu
2001	Chaff：监视文字、VSIDS	M. Moskewicz 等
2003	MiniSat；SMT-LIB 计划启动	N. Eén、N. Sörensson；SMT-LIB
2006	DPLL(T) 形式化	R. Nieuwenhuis、A. Oliveras、C. Tinelli
2007	MiniZinc 建模语言	N. Nethercote、P. Stuckey 等
2008	Z3 SMT 求解器	L. de Moura、N. Bjørner
2014	DRAT-trim 证明检查	N. Wetzler、M. Heule、W. Hunt
2016	布尔毕达哥拉斯三元组问题被解决并验证	M. Heule、O. Kullmann、V. Marek
2022	cvc5	H. Barbosa、C. Barrett 等

6. 长处与局限

这一族求解器擅长什么，又在哪里止步。
长处	局限
声明式：写下规则，而不是算法	编码是一门技术；糟糕的模型可能比好的模型慢指数倍
完备求解器要么找到解，要么证明无解	一般是 NP 完全的：有些输入会花费指数时间，超时意味着“未知”
答案可以检查：模型可在线性时间内检查，不可满足证明可由独立检查器检查	证明认证的是公式，而不是编码；把现实问题翻译错了，就会得到一个错误问题的正确答案
一台通用引擎服务于规划、验证、调度和配置	没有扩展（MaxSAT、加权 CSP、优化）就没有不确定性或偏好的概念
添加一个约束是局部的、立即生效的	约束本身必须有来处：符号 AI 的知识获取瓶颈在这里同样存在

7. 求解器与失效安全模型

失效安全模型是这样一种 AI 模型：它的失败会终止于受控的安全状态；证据缺失时它弃权，学习可以收窄它的行为，却永远不能扩大它被允许做的事。SAT 和 SMT 求解器在小尺度上展示了实现这一点的工程模式。求解器是一个庞大、高度优化、因而会出错的程序；它的答案并不因为出自它而被信任。声称的解直接对照约束检查；声称的“不可满足”则可以附带一份子句证明，由 DRAT-trim 这样的小型检查器独立验证[32]。超时的求解器返回“未知”，构建良好的系统会把它当作未知，而不是当作“是”。

当语言模型位于符号层之前时，同样的分工依然适用：模型可以提议；只有地板能接纳一条事实。诚实的局限也随之而来。求解器认证的是交给它的公式；如果现实问题的编码是错的，证书就毫无价值。检查并不能让系统变得正确，它让系统的失败终止于“未证明”，而不是一个自信的错误。我们的论文 The Orchestration Gap 论证了链条级不变量为何需要这样一层。Perslis Research 的研究原型 Peel 正是按这一原则构建的；据我们所知，它是第一个失效安全模型（确切的主张与最接近的已有工作见什么是失效安全模型？）。做决定的回路里没有神经网络，它的知识是有类型、有来源的卡片。

其他各族技术见符号 AI 技术指南；求解器在更长的故事中处于什么位置，见符号 AI 的历史。

8. 常见问题

什么是约束满足问题？: 约束满足问题由一组变量、每个变量可能取值的值域，以及限制哪些取值组合被允许的约束组成。解就是给每个变量赋一个值，使所有约束都成立。地图着色、数独、排课和产品配置都是标准的例子。
什么是 SAT 求解器？: SAT 求解器是一种程序，用来判定一个布尔公式（通常写成合取范式的子句）能否被满足。如果能，求解器返回一个满足赋值；如果不能，它报告不可满足，许多求解器还能输出这一结论的证明。
什么是 SMT 求解器？: SMT 求解器判定可满足性模理论问题：它处理把布尔逻辑与算术、位向量、数组等理论混合在一起的公式。它把负责逻辑结构的 CDCL SAT 求解器与专门的理论求解器结合起来。Z3 和 cvc5 是广泛使用的例子。
DPLL 和 CDCL 有什么区别？: 1962 年的 DPLL 通过单元传播、在变量上分裂以及按时间顺序回溯来搜索。1996 年在 GRASP 求解器中提出的 CDCL 加入了冲突分析：每次冲突都产生一条学到的子句，防止在别处重犯同样的错误，并且求解器直接跳回导致冲突的那个决策。
什么是弧相容？: 两个变量之间的一条弧是相容的，当且仅当第一个变量值域中的每个值在第二个变量的值域中至少有一个相容的值。Alan Mackworth 于 1977 年发表的 AC-3 算法不断删除没有支持的值，直到每条弧都相容或某个值域变空。
既然 SAT 是 NP 完全的，它为什么还重要？: NP 完全意味着没有已知算法能在每个公式上都快，但来自硬件、软件和规划的真实公式具有子句学习可以利用的结构。现代求解器常常能判定含数百万子句的工业实例；而且由于 NP 中的每个问题都能翻译成 SAT，一个好的求解器可以服务于许多应用。
SAT 和 SMT 求解器算人工智能吗？: 算，属于符号意义上的人工智能。它们源自 AI 中的自动定理证明和约束满足研究，并在显式的逻辑约束上进行精确推理。与机器学习模型不同，它们不从数据中学习，而它们的答案可以被独立检查。
SAT 和 SMT 求解器今天用在哪里？: 它们用于硬件与软件验证、测试生成、调度与排课、自动规划、云访问策略分析、DNF、zypper 和 conda 等工具中的软件包依赖解析，也用于数学研究，例如 2016 年对布尔毕达哥拉斯三元组问题的求解。

9. 参考文献

S. Russell, P. Norvig. Artificial Intelligence: A Modern Approach, 4th ed. Pearson, 2020.（约束满足问题一章。）
U. Montanari. Networks of Constraints: Fundamental Properties and Applications to Picture Processing. Information Sciences 7:95–132, 1974. doi:10.1016/0020-0255(74)90008-5
D. Waltz. Understanding Line Drawings of Scenes with Shadows. In P. H. Winston (ed.), The Psychology of Computer Vision. McGraw-Hill, 1975.
A. K. Mackworth. Consistency in Networks of Relations. Artificial Intelligence 8(1):99–118, 1977. doi:10.1016/0004-3702(77)90007-8
A. K. Mackworth, E. C. Freuder. The Complexity of Some Polynomial Network Consistency Algorithms for Constraint Satisfaction Problems. Artificial Intelligence 25(1):65–74, 1985. doi:10.1016/0004-3702(85)90041-4
S. W. Golomb, L. D. Baumert. Backtrack Programming. Journal of the ACM 12(4):516–524, 1965. doi:10.1145/321296.321300
R. M. Haralick, G. L. Elliott. Increasing Tree Search Efficiency for Constraint Satisfaction Problems. Artificial Intelligence 14:263–313, 1980.
E. C. Freuder. Synthesizing Constraint Expressions. Communications of the ACM 21(11):958–966, 1978. doi:10.1145/359642.359654
J.-C. Régin. A Filtering Algorithm for Constraints of Difference in CSPs. Proceedings of AAAI-94, 1994.
S. Minton, M. D. Johnston, A. B. Philips, P. Laird. Solving Large-Scale Constraint Satisfaction and Scheduling Problems Using a Heuristic Repair Method. Proceedings of AAAI-90, 17–24, 1990.
J. Jaffar, J.-L. Lassez. Constraint Logic Programming. Proceedings of the 14th ACM Symposium on Principles of Programming Languages (POPL), 1987. doi:10.1145/41625.41635
M. Dincbas, P. Van Hentenryck, H. Simonis, A. Aggoun, T. Graf, F. Berthier. The Constraint Logic Programming Language CHIP. Proceedings of FGCS-88, Tokyo, 1988.
N. Nethercote, P. J. Stuckey, R. Becket, S. Brand, G. J. Duck, G. Tack. MiniZinc: Towards a Standard CP Modelling Language. Principles and Practice of Constraint Programming (CP), 2007.
S. A. Cook. The Complexity of Theorem-Proving Procedures. Proceedings of the 3rd ACM Symposium on Theory of Computing (STOC), 151–158, 1971. doi:10.1145/800157.805047
M. Davis, H. Putnam. A Computing Procedure for Quantification Theory. Journal of the ACM 7(3):201–215, 1960. doi:10.1145/321033.321034
B. Selman, H. Levesque, D. Mitchell. A New Method for Solving Hard Satisfiability Problems. Proceedings of AAAI-92, 1992.
B. Selman, D. G. Mitchell, H. J. Levesque. Generating Hard Satisfiability Problems. Artificial Intelligence 81(1–2):17–29, 1996. doi:10.1016/0004-3702(95)00045-3
M. Davis, G. Logemann, D. Loveland. A Machine Program for Theorem-Proving. Communications of the ACM 5(7):394–397, 1962. doi:10.1145/368273.368557
J. P. Marques-Silva, K. A. Sakallah. GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers 48(5):506–521, 1999. First presented at ICCAD 1996.
R. J. Bayardo, R. C. Schrag. Using CSP Look-Back Techniques to Solve Real-World SAT Instances. Proceedings of AAAI-97, 1997.
M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Engineering an Efficient SAT Solver. Proceedings of the 38th Design Automation Conference (DAC), 530–535, 2001. doi:10.1145/378239.379017
N. Eén, N. Sörensson. An Extensible SAT-solver. SAT 2003, LNCS 2919, 502–518, 2004. doi:10.1007/978-3-540-24605-3_37
G. Nelson, D. C. Oppen. Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems 1(2):245–257, 1979. doi:10.1145/357073.357079
R. Nieuwenhuis, A. Oliveras, C. Tinelli. Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T). Journal of the ACM 53(6):937–977, 2006. doi:10.1145/1217856.1217859
L. de Moura, N. Bjørner. Z3: An Efficient SMT Solver. TACAS 2008, LNCS 4963. doi:10.1007/978-3-540-78800-3_24
H. Barbosa, C. Barrett, M. Brain, et al. cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS 2022, 415–442. doi:10.1007/978-3-030-99524-9_24
A. Biere, A. Cimatti, E. Clarke, Y. Zhu. Symbolic Model Checking without BDDs. TACAS 1999, 193–207. doi:10.1007/3-540-49059-0_14
J. Backes, P. Bolignano, B. Cook, C. Dodge, A. Gacek, K. Luckow, N. Rungta, O. Tkachuk, C. Varming. Semantic-based Automated Reasoning for AWS Access Policies using SMT. FMCAD 2018. doi:10.23919/FMCAD.2018.8602994
F. Mancinelli, J. Boender, R. Di Cosmo, J. Vouillon, B. Durak, X. Leroy, R. Treinen. Managing the Complexity of Large Free and Open Source Package-Based Software Distributions. ASE 2006, 199–208. doi:10.1109/ASE.2006.49
conda project. Conda 23.10.0 release: libmamba is now the default solver. conda.org blog, 6 November 2023. conda.org
M. J. H. Heule, O. Kullmann, V. W. Marek. Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. SAT 2016. arXiv:1605.00723
N. Wetzler, M. J. H. Heule, W. A. Hunt Jr. DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. SAT 2014, 422–429. doi:10.1007/978-3-319-09284-3_31