CDCL Algorithm

1 Conflict-Driven Clause Learning(CDCL) Algorithm

SAT 求解器可以被分为两类, 一类是基于冲突驱动的子句学习框架的算法或者组合算法; 一类是基于随机搜索(stochastic search)的算法. 根据经验来看, 基于 CDCL 的算法在大多数情况下, 针对 CNF 公式的求解性能要优于随机搜索. 所以着重学习一下 CDCL 和 DPLL 对 SAT 求解问题会有更加深入的了解.

CDCL-SAT算法

\[ \begin{aligned} &\mathbf{Algorithm\ 1.}\ \rm{CDCL\mbox{-}SAT}\\ &\mathbf{Input:}\ \rm{A\ propositional\ CNF\ formula}\ \mathcal{B}\\ &\mathbf{Output:}\ \rm{''Satisfiable''\ if\ the\ formula\ is\ satisfiable\ and\ ''Unsatisfiable''\ otherwise}\\ &\\ &1.\hspace{2mm}\mathbf{function}\ \rm{CDCL}\\ &2.\hspace{10mm}\mathbf{while}\ \rm{(TRUE)}\ \mathbf{do}\\ &3.\hspace{18mm}\mathbf{while}\ \rm{(BCP()\ =\ ''CONFLICT'')}\ \mathbf{do}\\ &4.\hspace{25mm}backtrack\mbox{-}level:= \rm{ANALYZE\mbox{-}CONFLICT()};\\ &5.\hspace{25mm}\mathbf{if}\ backtrack\mbox{-}level\lt 0 \mathbf{then\ return}\ \rm{''Unsatisfiable''};\\ &6.\hspace{25mm}{\rm BackTrack}(backtrack\mbox{-}level);\\ &7.\hspace{18mm}\mathbf{if}\ \neg{\rm DECIDE()}\ \mathbf{then\ return}\ {\rm ''Satisfiable''}; \end{aligned} \]

如算法1 所示, CDCL 求解器接受一个 CNF 合取范式公式 \(\mathcal{B}\) 作为输入, 输出为该公式是否为可满足的. 算法执行到循环体内, 当通过执行布尔约束传播(BCP)函数得到冲突结果时, 算法进入第二层循环. 在分析冲突子句(conflict clause)之后, ANALYZE-CONFLICT() 函数返回一个回溯层(backtrack-level)的值并且生成一组新的冲突子句. 此时, 如果要回溯的决策层的值小于零, 那么说明此 CNF 公式不可满足(因为如果回溯结果小于零, 就说明不存在一组赋值使得 CNF 公式整体为真); 反之, 执行回溯函数 BackTrack(), 并回溯到决策层 backtrack-level(). 如果没有侦测到冲突, 那么执行 DECIDE() 函数, 判断是否还有未被赋值的文字, 如果都被赋值了, 那么公式 \(\mathcal{B}\) 是可满足的, 否则循环继续.

以上是 CDCL 框架的整体思路, 但是这里存在两个问题需要进行深究: 1) 如何对冲突子句进行分析, 也就是函数ANALYZE-CONFLICT() 是如何工作的. 2) 函数DECIDE() 如何能够快速且高效地判断已赋值和未赋值的变量, 并赋真值给尚未赋值的变量.

2 ANALYZE-CONFLICT 算法

先说明第一个问题. ANALYZE-CONFLICT() 负责从先前得出的冲突子句和冲突蕴涵图推导出新的冲突子句并计算出 CDCL 算法所要回溯的决策层. ANALYZE-CONFLICT() 在冲突蕴涵图上从冲突节点回溯, 并通过一系列步骤生成新的冲突子句. 以下对该算法进行说明.

\[ \begin{aligned} &\mathbf{Algorithm\ 2.}\ \rm{ANALYZE\mbox{-}CONFLICT}\\ &\mathbf{Input:}\\ &\mathbf{Output:}\ \rm{Backtracking\ decision\ level\ +\ a\ new\ conflict\ clause}\\ &\\ &1.\hspace{2mm}\mathbf{if}\ current\mbox{-}decision\mbox{-}level=0\ \mathbf{then\ return}\ -1;\\ &2.\hspace{2mm}cl:=current\mbox{-}conflicting\mbox{-}clause;\\ &3.\hspace{2mm}\mathbf{while}\ ({\rm \neg STOP\mbox{-}CRITERION\mbox{-}MET}(cl))\ \mathbf{do}\\ &4.\hspace{10mm}lit:={\rm LAST\mbox{-}ASSIGNED\mbox{-}LITERAL}(cl);\\ &5.\hspace{10mm}var:={\rm VARIABLE\mbox{-}OF\mbox{-}LITERAL}(lit);\\ &6.\hspace{10mm}ante:={\rm ANTECEDENT}(lit);\\ &7.\hspace{10mm}cl:={\rm RESOLVE}(cl,\ ante,\ var);\\ &8.\hspace{2mm}{\rm add\mbox{-}clause\mbox{-}to\mbox{-}database}(cl);\\ &9.\hspace{2mm}\mathbf{return}\ {\rm clause\mbox{-}asserting\mbox{-}level}(cl);\hspace{15mm} \triangleright\ {\rm 2nd\ highest\ decision\ level\ in\ } cl \end{aligned} \]

如算法2 所示, ANALYZE-CONFLICT 算法的输出正如前文所述, 即回溯决策层并产生一组新的冲突子句(断言子句). 如果当前的决策层的值为0, 那么返回-1, 随之的结果就是在 CDCL 求解器中判定公式 \(\mathcal{B}\) 不可满足. 否则, 变量 \(cl\) 记为当前冲突子句, 并进入循环体. 循环的判断条件 STOP-CRITERION-MET(cl), 一个比较好的策略是, 在当前决策层, 当且仅当 \(cl\) 包含第一个唯一蕴涵节点(UIP)的否定, 结果就返回"真". 循环体内部, 将当前冲突子句的最后一个赋值文字赋值给变量 \(lit\). 将 \(lit\) 中的变量(即没有逻辑连接符\(\neg\)的文字)赋值给 \(var\). \(lit\) 的前件赋值给 \(ante\), 所谓前件就是仅由 \(lit\) 决定真值的子句(clause). 循环体最后, 更新当前冲突子句 \(cl\) 的值, 这个更新策略为 RESOLVE(\(cl\), \(ante\), \(var\)). 循环结束之后, 更新数据库, 并返回决策层级.先说明策略 RESOLVE 的作用. 该策略涉及到一个概念, 即二元解析(Binary Resolution). 考虑如下推导规则:

\[ \begin{aligned} \frac{(a_1 \lor\ ...\ a_n\lor\ \beta)\ (b_1\lor\ ...\ b_n\lor\ \neg\beta)}{(a_1\lor...\lor a_n\lor b_1 ...\lor b_n)} \end{aligned} \] 其中, \(a_1,...,a_n,b_1,...b_n\) b 表示文字, \(\beta\) 表示变量. 变量 \(\beta\) 被称作解析变量(resolution variable). 两个子句 \((a_1 \lor\ ...\ a_n\lor\ \beta)\ \) 和 \((b_1\lor\ ...\ b_n\lor\ \neg\beta)\) 是待解析子句, 最终结果 \((a_1\lor...\lor a_n\lor b_1 ...\lor b_n)\) 是已解析子句. 显而易见, 二元解析的作用是将两个含有同一个变量 \(\beta\) 的析取子句合并成不含公共变量的析取子句. 由此, 基于二元解析规则的演绎推理系统是可靠且完备的. 换句话说, 当且仅当存在一个以空子句结束的有限二元解析步骤的序列时, 这样一个 CNF 公式是不可满足的. 用一个简单的例子说明二元解析和 RESOLVE 策略.

图1 RESOLVE策略

如图1 所示的冲突蕴涵子图, 整个 ANALYZE-CONFLICT 算法的作用就是从图中的冲突节点 \(\mathcal{k}\) 开始从右向左回溯, 以产生新的冲突子句. 该蕴涵图的结果是产生一个当前的冲突子句 \(c_5 := (x_{10}\lor x_2\lor \neg x_4)\). ANALYZE-CONFLICT 从冲突子句 \(c_4\) 处回溯整个蕴涵图, 回溯过程如下表1所示.

表1. 回溯过程

\(\rm Name\)	\(cl\)	\(lit\)	\(var\)	\(ante\)
\(c_4\)	\((\neg x_6\lor x_7)\)	\(x_7\)	\(x_7\)	\(c_3\)
	\((\neg x_5\lor\neg x_6)\)	\(\neg x_6\)	\(x_6\)	\(c_2\)
	\((\neg x_4\lor x_{10}\lor \neg x_5)\)	\(\neg x_5\)	\(x_5\)	\(c_1\)
\(c_5\)	\((\neg x_4\lor x_2\lor x_{10})\)

子句 \(c_5\) 是一个断言子句, 在这个子句中，第一个 UIP(\(x_4\)) 的否定是来自当前决策层的唯一文字.

3 DECIDE策略

第二个问题, DECIDE 策略的选择. 在 SAT 求解过程中最重要的部分就是选择变量并给已选变量赋值的策略, 这个策略就是 SAT 求解器的启发式判定(decision heuristic)策略. 先介绍几个常见的启发式判定策略.

3.1 Jeroslow-Wang

其实最容易想到的就是 Jeroslow-Wang 策略, 只要找到在每一个子句中出现次数最多的那个文字就行了. 对于给定的CNF公式 \(\mathcal{B}\), 计算每一个文字 \(l\) \[ J(l)\ = \Sigma_{\omega \in \mathcal{B}, l\in\omega}2^{-|\omega|} \] 其中 \(\omega\) 代表一个子句, 相应地, \(|\omega|\) 表示该子句的长度. 选择出一个使得 \(J(l)\) 值最大的文字 \(l\), 也就是尚未被赋值的那个文字. 这个策略给予在短子句中出现频率最高的文字较高的优先等级, 可以被静态或者动态实现. 显然, 动态实现方法在每个决策点会导致很大的性能开销.

3.2 动态最大单项和(Dynamic Largest Individual Sum, DLIS)

在每一个决策层, 选择满足当前为满足子句数量最多的尚未赋值的文字. 实现这种启发式方法的常见方法是将每个文字的指针指向它所出现的子句列表中. 在每个决策层, 求解器计算包含这个文字但尚未满足的子句数量, 并将这个数字分配给该文字. 随后, 选择计数最多的文字. 同样, DLIS 也导致很大的开销, 因为做出决策的复杂度与子句的数量成正比.

3.3 变量状态下的独立衰减和(Variable State Independent Decaying Sum, VSIDS)

这是 SAT 求解器 Chaff 中引入的一种策略. 首先, 在计算每个文字出现的子句数量时, 不考虑该子句是否已经满足的问题. 这意味着, 对每一个决策的质量都会受到影响, 但是做出决策的复杂度会更好: 假设我们把文字保存在一个列表中, 按照各自的分数排序, 做出判定只需要需要常数时间. 其次, 定期将所有分数除以 2.

该决策的思路是使启发式决策基于冲突驱动, 意思就是说它试图首先解决最近发现的冲突. 为此, 它需要给近期冲突中所涉及到的变量更高的分数. 每一次冲突都会产生一个冲突子句. 一个新的冲突子句, 和其他子句一样, 每出现一个文字就加1分. 这个子句被添加后时间越长, 这些文字的分数被 2 整除的次数就越多. 因此, 变量在新的冲突子句中就变得更有影响力. 引入了 VSIDS 的 SAT 求解器 Chaff, 允许人们通过控制分数的被除频率和除数来调整这一策略. 针对不同 CNF 公式的解法最好是要有不同的参数.

还有另外一个基于冲突驱动的启发式方法. 比如说, MINISAT 求解器所采用的策略. MINISAT 为每一个变量保存一个双精度浮点型的活动分数(activity score), 用来衡量每一个变量推导出新子句的参与度. 如果一个子句 \(c\) 可以从其他子句 \(c_1,...,c_n\) 推导得出, 那么在子句 \(c_1,..c_n\) 中的每一个实例的变量 \(v\) 都会以常量 \(inc\) 的方式增加. \(inc\) 初始值设为 1, 在每次侦测到冲突之后就会被乘以 1.05, 因此会给那些参与到最近冲突子句中的变量较高的分数. 为了防止溢出, 如果某些变量的活动分数比 \(10^{100}\) 高, 那么所有的变量分数包括常量 \(inc\) 都乘以 \(10^{-100}\). 有着最高分数的变量将被选定. 被选定的变量的值, 要么是 \(\rm FALSE\) , 要么随机, 或者, 将先前的赋值重新赋给该变量. MINISAT 的成功之处在于, 并没有尝试猜测变量的正确赋值, 重要的是基于学习的本地搜索, 而不是去猜测当前分支的正确性. 因为, 即使是在可满足公式中的大多数分支中, 也不能推出一组使得公式可满足的赋值.

感兴趣的读者可以进一步学习 CDCL 算法相关的内容: CSE442-17f, CS-E3220.