给定一组布尔变量和若干由这些变量构成的子句，是否存在一种赋值方案，让所有子句同时为真？这就是经典的SAT（Satisfiability，布尔可满足性）问题。它是第一个被证明为NP完全的问题，理论上至今没有多项式时间解法，但在工程实践中，DPLL、CDCL等算法配合各种启发式策略，已经能高效处理数万甚至百万变量规模的工业实例。本文将用Node.js从零实现一个基于DPLL算法的SAT求解器，逐步讲解数据结构设计、单元传播、纯文字消除和递归搜索的完整流程。
一、SAT问题的数学表达与数据结构设计
标准的SAT输入采用CNF（合取范式）形式：整个公式是若干子句的合取（AND），每个子句是若干文字的析取（OR），每个文字是一个变量本身或其否定。例如公式 (x1 ∨ ¬x2) ∧ (x2 ∨ x3) ∧ (¬x1 ∨ ¬x3)，只要每个子句中至少有一个文字为真，整个公式就满足。
在编程实现中，最直观的做法是用整数编码变量：正数n表示变量xn为真，负数-n表示xn为假。于是上面这个公式在JS里就是一个二维数组。这种编码的好处是取反操作只需乘以-1，判断某个文字是否被当前赋值满足也非常直接。
// CNF公式：(x1 | ~x2) & (x2 | x3) & (~x1 | ~x3) // 用整数编码：正数代表变量取true，负数代表取false const formula = [ [1, -2], // 子句1：x1 为真，或者 x2 为假 [2, 3], // 子句2：x2 为真，或者 x3 为真 [-1, -3] // 子句3：x1 为假，或者 x3 为假 ]; // 当前赋值表：0表示未赋值，1表示true，-1表示false let assignment = new Map();
数据结构选择上还有一点值得注意：如果需要频繁做单元传播，可以为每个变量维护一个「出现位置索引」，记录它出现在哪些子句中，避免每轮传播都全量扫描公式。对于本文的教学实现，公式规模不大，直接扫描即可，但理解索引优化的思路对后续阅读MiniSat等工业求解器源码很有帮助。
二、DPLL算法的核心机制
DPLL算法由Davis、Putnam、Logemann和Loveland在1960年代提出，是现代SAT求解器的基石。它的基本框架是「简化—传播—分支—回溯」：每次迭代先对公式做化简，如果推出矛盾就回溯，如果所有子句都被满足就返回成功，否则挑一个未赋值的变量，分别尝试赋真和赋假两个分支递归求解。
第一项关键技术是单元传播（Unit Propagation）。如果某个子句只剩一个未赋值的文字，其他文字都被赋值为假，那么这个文字必须为真，否则子句就违反了约束。传播这个赋值后，可能又让其他子句变成单元子句，从而形成链式反应，快速缩小搜索空间。比如子句 (x1 ∨ ¬x2 ∨ x3) 中，假设x1已被赋假、x3也已被赋假，那么x2必须为假，这个结论是强制的，不需要分支。
第二项是纯文字消除（Pure Literal Elimination）。如果变量xn在公式中只以一种极性出现（只有xn或只有¬xn），那么把它赋成使所有这些子句为真的值即可，这些子句全部被满足，可以直接移除。这一步在很多实际公式上能显著削减规模，不过在含冲突学习的现代求解器中常被省略，因为维护极性信息的开销可能超过收益。
下面是评估函数的实现，它整合了单元传播和终止判断：
// 对公式执行一次评估与单元传播
// 返回值：'SAT'（可满足）、'UNSAT'（矛盾）、'UNKNOWN'（需要继续分支）
function propagate(formula, assignment) {
let changed = true;
while (changed) {
changed = false;
for (const clause of formula) {
// 跳过已满足的子句
let satisfied = false;
let unassigned = [];
for (const lit of clause) {
const val = assignment.get(Math.abs(lit)) || 0;
if ((val === 1 && lit > 0) || (val === -1 && lit < 0)) {
satisfied = true;
break;
}
if (val === 0) unassigned.push(lit);
}
if (satisfied) continue;
if (unassigned.length === 0) return 'UNSAT'; // 空子句，矛盾
if (unassigned.length === 1) {
// 单元子句：强制赋值并触发新一轮传播
const lit = unassigned[0];
assignment.set(Math.abs(lit), lit > 0 ? 1 : -1);
changed = true;
}
}
}
return 'UNKNOWN';
}这段代码的逻辑是反复扫描子句，直到某一轮没有任何新的强制赋值产生。注意这里我们直接往assignment这个Map里写入推断结果，因此递归回溯时必须撤销这些改动，一种简单做法是每次递归前深拷贝赋值表，教学实现可以接受，性能敏感场景则应记录推理轨迹做增量回退。
三、完整的递归求解器实现
有了传播函数，主求解函数就清晰了：先传播判断状态，再挑一个变量分支递归。变量选择策略用最朴素的「取第一个未赋值变量」，实际求解器会采用DLIS、Jeroslow-Wang或VSIDS等启发式，优先选择出现次数多或近期参与冲突的变量，分支顺序的好坏可能让搜索树规模相差几个数量级。
// DPLL主函数：返回满足赋值的Map，或null表示不可满足
function dpll(formula, assignment) {
const result = propagate(formula, assignment);
if (result === 'UNSAT') return null;
// 找第一个未赋值的变量
let pickVar = null;
for (const clause of formula) {
for (const lit of clause) {
if (!(assignment.get(Math.abs(lit)) || 0)) {
pickVar = Math.abs(lit);
break;
}
}
if (pickVar) break;
}
// 所有变量都已赋值且无矛盾，找到解
if (pickVar === null) return assignment;
// 分支一：尝试赋为true
const branchTrue = new Map(assignment);
branchTrue.set(pickVar, 1);
const r1 = dpll(formula, branchTrue);
if (r1) return r1;
// 分支二：尝试赋为false
const branchFalse = new Map(assignment);
branchFalse.set(pickVar, -1);
return dpll(formula, branchFalse);
}
// 测试
const solution = dpll(formula, new Map());
if (solution) {
console.log('SAT，一组满足赋值为：');
for (const [v, val] of solution) {
console.log('x' + v + ' = ' + (val === 1 ? 'true' : 'false'));
}
} else {
console.log('UNSAT，公式不可满足');
}对于开头的示例公式，程序会输出类似x2 = true、x3 = true的一组解，可以手动代入验证每个子句都为真。而如果把公式换成 (x1) ∧ (¬x1)，单元传播会立即让两个子句分别强制x1为真和为假，第二轮传播产生矛盾，直接返回UNSAT，全程没有任何分支搜索，这就是传播机制的威力。
四、性能瓶颈与进阶优化方向
上面的实现在教学层面完整可用，但遇到几千个变量以上的公式就会力不从心。瓶颈主要有三处：一是每轮传播全量扫描公式，复杂度为O(子句数×子句长度)，引入观察表（watched literals）可以把单轮传播降到接近常数因子；二是深拷贝赋值表的开销，应改为记录赋值栈按层回退；三是纯粹的时序回溯，一旦深入错误分支，可能重复撞上同样的冲突。
现代求解器如MiniSat、Glucose采用CDCL（冲突驱动子句学习）框架：每当检测到矛盾，就分析冲突成因，学习一条新的子句加入公式，避免相同冲突再次出现，同时依据学习子句回跳多个决策层，而不是只退一层。这套机制配合VSIDS变量活动度启发式和重启策略，是工业级求解能力的核心来源。如果想在JS生态里使用现成能力，可以关注通过WebAssembly编译的SatJS或minisat绑定，它们在Node.js中可以直接调用。
另一个实用方向是把SAT求解当作工具解决实际问题，比如数独求解、排课冲突检测、依赖解析等，核心工作是把业务约束编码成CNF。编码能力往往比求解器本身的速度更能决定整个方案是否可行，Tseitin变换就是将任意布尔公式转为等价CNF的标准手段，值得在动手写编码器之前先了解清楚。
总结一下，本文实现了一个约百行的DPLL求解器，涵盖了SAT问题的基本表达、单元传播、纯文字消除和分支回溯四个要素。理解了这些基础，再去阅读CDCL求解器的源码或论文就会顺利很多。建议读者动手运行示例代码后，尝试改造变量选择策略，观察不同启发式在随机生成的公式上的表现差异，这种实验比读十遍理论更能建立直觉。