基于DPLL的SAT求解器

SAT问题

什么是SAT问题？

  SAT问题即命题逻辑公式的可满足性问题（satisfiability problem），是计算机科学与人工智能基本问题，是一个典型的NP完全问题。
对于任一布尔变元x，x与其非“¬x”称为文字(literal)。对于多个布尔变元，若干个文字的或运算l1∨l2∨…∨lk称为子句(clause)。只含一个文字的子句称为单子句。不含任何文字的子句称为空子句，常用符号□表示。子句所含文字越多，越易满足，空子句不可满足。
SAT问题一般可描述为：给定布尔变元集合{x1, x2, ..., xn}以及相应的子句集合{c1, c2, ..., cm}，对于合取范式（CNF范式）：F = c1∧c2∧...∧cm，判定是否存在对每个布尔变元的一组真值赋值使F为真，当为真时（问题是可满足的，SAT），输出对应的变元赋值（一组解）结果。

CNF公式及.cnf文件
一个CNF公式也可以表示为一个合取式。
例如，由三个布尔变元a,b,c所形成的一个CNF公式（¬a∨b）∧（¬b∨c）,可用集合表示为{¬a∨b,¬b∨c}，该公式是满足的，a=0, b=0,c=1是其一组解。
一个CNF SAT公式或算例的具体信息通常存储在一个.cnf文件中，下图是算例problem1.cnf文件前若干行的截图。

CNF文件中，由‘c’开头的是若干注释说明行；
‘p’开头的行说明公式的总体信息，包括：范式为CNF；公式有200个布尔变元，由1到200的整数表示；320个子句。
之后每行对应一个子句，0为结束标记。46表示第46号变元，且为正文字；-46则是对应的负文字，文字之间以空格分隔

DPLL算法基本思想

DPLL算法是基于树/二叉树的回溯搜索算法。其中涉及到的一些对CNF公式的化简策略如下：

单子句规则

如果子句集S中有一个单子句L,那么L一定取真值，于是可以从S中删除所有包含L的子句（包括单子句本身），得到子句集S1，如果它是空集，则S可满足。否则对S1中的每个子句，如果它包含文字¬L,则从该子句中去掉这个文字，这样可得到子句集合S2。S可满足当且仅当S2可满足。单子句传播策略就是反复利用单子句规则化简S的过程。

分裂策略

按某种策略选取一个文字L.如果L取真值，则根据单子句传播策略，可将S化成S2；若L取假值（即¬L成立）时，S可化成S1. 交错使用上述两种策略可不断地对公式化简，并最终达到终止状态，其执行过程可表示为一棵二叉搜索树,

纯文字规则

在一个合取范式中，若一个命题变量要么以全是正文字的形式出现，要么以全是负文字的形式出现，那么该文字就称为纯文字。消除这种所有出现即为正或出现即为负的原子公式所在子句的规则就称为纯文字规则.

消除原子公式规则

假设给定的合取范式或一部分子式可以表示为以下这种形式：
其中， P 、 Q 、 R 都是析取子式， u 和 u 不在其它子句中出现，且 P 、 Q 、 R都与原子公式 u 无关，那么该公式可以消减为不含原子公式 u 的形式：

重言子句规则

如果一个子句是重言子句（一般是子句中存在互补的文字），那么就可以将它从合取范式中删除。

包含规则

如果A1,A2 是合取范式 B 的两个子句，且A 1 ⊆ A2，则求合取范式 B 的可满足性问题时可以直接将子句A1 删去。

分裂规则

设 CNF 公式的子句集为：
DPLL算法是经典的SAT完备型求解算法，对给定的一个SAT问题实例，理论上可判定其是否满足，满足时可给出对应的一组解。

DPLL算法基本实现过程
对 CNF 公式中的文字进行真值赋值所得出的搜索空间可以用一棵二叉树来表示。树中的每个节点对应一个布尔变元，取值只能为 1 和 0 ，左右子树表示该变量取真值和假值的分支，从二叉树中根节点到叶子节点的一条路径就表示 CNF 公式中的一组变量赋值序列。

基于 DPLL 的算法都是对这棵二叉树从根节点开始进行深度优先搜索 (DFS) 遍历所有的通路，以找到使问题可满足解。

容易知道，一课二叉树的叶子节点只能有两种：

子句集取真值，该问题是可满足的。
子句集中含有一个或多个空子句，该问题不可满足。

绝大部分回溯搜索算法都是建立在原有的 DPLL 算法框架之上的。它们的求解过程基本上都是分为以下 3 个阶段：

变量决策阶段（即 DECIDE 过程）：在搜索过程的每一分支阶段，选择未赋值的一个变量为其赋值为 0 或 1 ，该变量称为决策变量，决策变量在赋值时所处的二叉树中的高度称为它的决策层。
推理阶段（也称为 BCP 过程）：每一次已选择变量赋值之后，识别该赋值所导致的必要的赋值或者根据已有的变量赋值对子句进行化简，即进行布尔约束传播过程。
回溯阶段（ BACKTRACK ）：推理过程中发生冲突时，进行冲突分析和子句学习，并实现算法的回溯，使搜索过程从较深的变量决策层返回至较浅的决策层。冲突即指 BCP 过程中，至少出现了一个子句不可满足的情况。

下图是DPLL算法实现的一个基本流程图：

接下来就是关于具体的DPLL实现过程：DPLL实现所需要的数据结构，数据预处理过程，加速搜索的启发式策略（如何快速地选择决策变量赋值），以及在搜索赋值过程中遇到冲突时的解决办法，以及基本回溯方法等等。

原文部分内容来自《陈稳. 基于DPLL的SAT算法的研究与应用.硕士学位论文，电子科技大学，2011》