Handbook of Satisfiability (2nd ed.), Chapter 4
CDCL SAT求解器将SAT问题的求解能力从90年代的几百个变量提升到目前的几百万个变量。
CDCL SAT求解器最关键的部分是冲突分析。
本章主要介绍现代CDCL SAT求解器普遍的组成部分。
CNF形式稍有改变：
变量需要的属性：
FUIP的学习子句：
局部最小化(Local Minimization)
自包含变量消除：
例：选择，得到：
递归最小化(Recursive Minimization)
文字块距离（LBD）：将子句变量按照决策等级分组，组的数量称为文字块距离。
LBD较小，倾向于保留；LDB较大，倾向于删除。
LBD较大，可以进行学习子句最小化的操作。
结论：FUIP得到子句的LDB不大于当次冲突分析中任意UIP得到子句的LDB。
保留当前学习到的子句，重新开始搜索。
目的：平衡探索和利用(Exploration and Exploitation)（强化学习的思想）
合适的重启策略
包括重启时机，重启频率，重启后的行为，是一系列的超参数
保证算法完备性
阶段节省(Phase Saving)：考虑变量的赋值偏好
分支：选择赋值变量。
变量状态独立衰减和(VSIDS)：
监视文字(Watched Literal)：
现代CDCL SAT求解器共同特点：
其他技术：