第4章 SAT求解器入门

第4章 SAT求解器入门：布尔可满足性问题、DPLL算法、CDCL算法、MiniSAT使用实战、SAT在验证中的应用

4.1 布尔可满足性问题：到底在解决什么？

SAT问题，说白了就是问：给定一个布尔公式，能不能找到一组变量的赋值，让整个公式为真？

我刚开始接触这个领域时，觉得这问题太简单了。不就是给变量赋0或1吗？但后来发现，当变量数量达到几百甚至上万个时，暴力枚举根本行不通。2的n次方种可能，n=100时就已经是天文数字了。

SAT问题的标准形式是CNF（合取范式）。举个例子：

(x1 ∨ ¬x2) ∧ (x2 ∨ x3) ∧ (¬x1 ∨ ¬x3 ∨ x4)

每个括号叫一个子句，里面的变量叫文字。整个公式为真，意味着每个子句都要为真。每个子句为真，意味着至少有一个文字为真。

核心要点：SAT求解器就是用来判断这样的CNF公式是否有解。如果有，它还能给出一个具体的赋值。

你想想看，验证一个电路设计是否正确，本质上就是在问：是否存在一组输入，让电路输出错误的结果？这不就是个SAT问题吗？

4.2 DPLL算法：回溯搜索的鼻祖

DPLL算法是SAT求解的基石。它的核心思想其实很简单：

决策：选一个未赋值的变量，给它赋个值（0或1）
传播：看看这个赋值能不能推导出其他变量的值
冲突检测：如果发现矛盾，就回溯到上一个决策点
回溯：换个方向继续尝试

我记得第一次手动模拟DPLL算法时，花了整整一下午。但弄明白后，感觉就像解数独一样——试错、回溯、再试。

DPLL有两个关键优化：

单位传播：如果一个子句只剩一个未赋值的文字，那这个文字必须为真
纯文字规则：如果一个变量只以同一种极性出现，直接给它赋值

我的经验：单位传播是DPLL最核心的加速手段。实际项目中，90%以上的变量赋值都是通过单位传播推导出来的，而不是靠决策猜出来的。

4.3 CDCL算法：现代SAT求解器的核心

CDCL（冲突驱动子句学习）是DPLL的进化版。它解决了一个关键问题：DPLL遇到冲突只会回溯，但不会从冲突中学习。

CDCL的做法是：每次冲突发生时，分析冲突的原因，生成一个冲突子句，加到公式中。这个新子句能避免将来再走同样的弯路。

我曾在项目中遇到过这样一个场景：一个公式有5000个变量，DPLL跑了3小时没出结果。换成CDCL求解器，不到10秒就搞定了。差别就在于CDCL学会了「哪些路径是死路」。

CDCL的核心流程：

决策 + 传播（和DPLL一样）
冲突发生时，用冲突分析找出原因
生成冲突子句，加入公式
根据冲突分析结果，非时序回溯到合适的位置
继续搜索

注意：冲突子句的数量会快速增长。如果不加控制，内存会爆炸。现代求解器会定期清理「不活跃」的冲突子句。我曾经因为没做这个优化，导致求解器在运行20分钟后内存耗尽——教训深刻。

4.4 MiniSAT使用实战

MiniSAT是SAT求解器中的「Hello World」。代码量小、性能不错、接口清晰。我建议初学者从它入手。

安装很简单：

git clone https://github.com/niklasso/minisat.git
cd minisat
make

MiniSAT的输入格式是DIMACS CNF。举个例子：

c 这是一个注释
c 变量数: 3, 子句数: 4
p cnf 3 4
1 -2 0
2 3 0
-1 -3 4 0
-4 0

每行末尾的0表示子句结束。正数表示变量取真，负数表示取假。

运行求解器：

./minisat input.cnf output.txt

输出文件会告诉你SAT还是UNSAT。如果是SAT，还会给出一个满足的赋值。

实战技巧：我习惯用Python生成DIMACS文件。写个脚本把问题转换成CNF，然后调MiniSAT求解。这样比手写CNF快得多。

下面是一个简单的Python生成器示例：

def generate_cnf(vars, clauses):
    with open('problem.cnf', 'w') as f:
        f.write(f'p cnf {vars} {len(clauses)}\n')
        for clause in clauses:
            f.write(' '.join(map(str, clause)) + ' 0\n')

4.5 SAT在验证中的应用

SAT在形式化验证中无处不在。我总结了几种常见场景：

应用场景	核心思路	典型工具
等价性检查	将两个电路异或，检查是否存在输入使输出为1	SAT求解器 + 电路编码
有界模型检验	将系统展开k步，检查是否存在违反性质的路径	CBMC、NuSMV
测试生成	将覆盖目标编码为SAT，求解得到测试向量	自定义工具
自动测试模式生成	将故障效应传播到输出端，求解输入向量	ATPG工具

举个例子，等价性检查怎么做？假设你有两个电路实现F和G，你想验证它们是否等价。构造一个公式：F ⊕ G = 1。如果这个公式SAT，说明存在输入让F和G输出不同——不等价。如果UNSAT，说明对所有输入，F和G输出相同——等价。

关键洞察：SAT求解器本质上是一个「反例搜索器」。你告诉它「什么情况是错的」，它帮你找「是否存在这种情况」。找不到，就说明系统是对的。

我在实际项目中用SAT做过寄存器传输级（RTL）代码的验证。把Verilog代码翻译成CNF，然后用MiniSAT检查某些性质。虽然翻译过程有点麻烦，但一旦跑起来，效果出奇的好。

嗯，这里要注意一点：SAT求解器处理的是布尔逻辑，而实际验证中经常需要处理整数、数组等复杂数据类型。这时候就需要用位向量编码，或者用SMT求解器（下一章会讲）。

最后分享一个我踩过的坑：曾经有个项目，SAT求解器跑了一整天没出结果。后来发现是CNF编码出了问题——把一些约束编码成了指数级大小的公式。换了个编码方式，求解时间从一天降到了3秒。所以说，编码方式往往比求解器本身更重要。

📚 课程目录