2.1.3 命题可满足性求解方法
当命题知识库表示为 CNF 公式时，目前高效的 SAT 求解能较好 地解决一致性判定这一问题，在某些情况下甚至可在较短的时间内判 定出多达上百万个变量的知识库的一致性。对于其他命题推理任务中，除模型计数、模型枚举以及计算最小度外，也可通过调用一次或线性 次 SAT 求解器进行求解。例如，对于子句蕴含问题，蕴含当且仅 当 可满足。又如，对于知识库间蕴含问题，蕴含当且仅当对 于任意 都有蕴含。SAT 问题是第一个被证明为 NP 完全的问 题，Cook 也因此获得了图灵奖。
SAT 求解方法主要可分为完备和非完备两类，前者能判断出可满 足性并对于可满足的问题能给出解，后者对于不可满足的问题无法给 出判断。完备的求解方法中使用最广的为 DPLL 算法[5] [23] ，最早由 Davis 和 Putnam 于 1960 年提出，并在 1962 年由 Davis、Logemann、 Loveland 进行进一步的优化，这是一种搜索树上的深度优先搜索算法，
它结合了单文字规则、纯文字规则等缩小搜索空间，主要思想是在公 式的所有部分赋值的空间中进行回溯搜索。在 DPLL 框架下，研究人 员通过嵌入多种优化技术实现了多个高效的求解器，最著名优化技术 为 1996 年 Silva 和 Sakallah[24] 在求解器 GRASP 中提出的冲突学习 技术，后续的完备的求解器都使用到了这项技术，该技术通过对冲突 进行分析学习新子句缩减搜索空间，极大的提高了 DPLL 方法的效 率，现代的 SAT 求解都使用到了这项技术，对应的求解器也被称为 基于冲突的子句学习（Conflict-driven clause learning，CDCL）求解器。最经典的 CDCL 求解器是 MiniSAT[25] ， 后续的很多求解器 PrecoSAT[26] 、CryptoMiniSat[27] 、Kissat[28] 等都是在 MiniSAT 的源 代码基础上改进的。非完备求解方法多基于局部搜索，包括 GSAT[29] 、 Walksat[30] 、调查传播（survey propagation）[31] 、格局检测[32] 等。自 2002 开始，SAT 领域内每年举办一次 SAT 竞赛，也极大地推动了 SAT 问题求解效率的提高。
国内对于 SAT 问题也取得了很多研究成果，早在 2000 年，中科院软件所张健研究员出版了一部关于可满足性求解器的专著，中科院软件所蔡少伟和华中科技大学何琨等研究组在 SAT 竞赛中多次获得冠亚军，吉林大学欧阳丹彤团队在基于扩展规则的 SAT 求解方面发表了一系列的成果。