浅谈 SAT 问题与 SAT-Solver

通过 Hackergame 比赛滑水知道了有 SAT-Solver 这个东西（其实是先知道了 SMT-Solver 然后再知道了 SAT-Solver），遂花了点时间去研究了一下。

这篇文章的前半部分是 SAT 相关的一些常识的回顾，后半部分开始介绍求解一般 SAT 问题的算法。

笔者计划在24春系统学习形式化方法入门内容，在那之后会进一步整理更多内容。

SAT 备件简述

SAT 问题与 CNF 格式

SAT 问题即可满足性问题 (Satisfiability Problem)：一般被定义为布尔可满足行问题或命题可满足性问题，即：

布尔可满足性问题 (Boolean Satisfiability Problem) ：给定布尔表达式 (由 AND, OR, NOT, 变量, 和括号构成), 是否存在对变量 TRUE 或 FALSE 的赋值, 使得整个表达式真。例如
$(x + y\neg z)(x + y + z)(\neg y + \neg z)$

以及：

命题可满足性问题 (Propositional satisfiability problem) :给定命题逻辑公式, 命题是否可满足。
$(\neg(x_1 \to \neg x_2) \to x_3) \to (x_1 \to (x_2 \to x_3))$

任意布尔表达式和命题逻辑公式都可以等价转换为合取范式（或析取范式，一般研究中采用前者）。

合取范式 (Conjunctive normal form) ：一个合取范式形如： ,子句 (Clause) 形如： ,其中，称为文字 (Literal) ，为某一布尔变量或该布尔变量的非。例如：
$(\lnot a_1\lor a_2)\land(\lnot a_1\lor a_3\lor a_4)\land(a_1\lor\lnot a_2\lor a_3\lor\lnot a_4)$

SAT 与复杂性理论

-SAT 问题指的是在 CNF 格式下的 SAT 问题中限定每个子句的最大文字数为，这样的问题被称为 -SAT 问题。

3-SAT 以及以上的问题已经被证明是问题，暂时没有多项式时间复杂度的算法。而 2-SAT 问题则已经有多项式时间复杂度的解法。

2-SAT 问题

这是算法竞赛中熟知的结论，是一个已经得到解决了的问题。这里简单介绍一下该问题的解决方式。

SAT-Solver

现在开始介绍一般的 SAT 问题求解器的原理，当前的 SAT-Solver 主要有两种不同的实现思路：

Davis-Putnam-Logemann-Loveland 算法及其各种优化
随机局部搜索算法

这里我们只介绍其中的第一种 DPLL 及衍生算法，也是最主流的实现思路。

BCP 布尔约束传播

BCP 即布尔约束传播 (Boolean Constraint Propagation) 。这是一种及其简单的想法，如果一个子句中只有一个文字则我们称这个子句为单位子句 (Unit Clause) 。那么为了使合式成立即该子句成立这个文字必须复制为真。例如：

$\phi = (p\lor\lnot q\lor\lnot s\lor t)\land(q\lor\lnot r\lor\lnot s\lor\lnot t)\land(r\lor p)\land t$

该式子中是单位字句，那么我们有

$\begin{aligned} \phi &= (p\lor\lnot q\lor\lnot s\lor t)\land(q\lor\lnot r\lor\lnot s\lor\lnot t)\land(r\lor p)\land t \\ &=(q\lor\lnot r\lor\lnot s)\land(r\lor p)\land t\\ \end{aligned}$

这里利用到了简单的逻辑公式（实际上也是 CNF 格式对任何文字赋值的响应方式）：

$\begin{aligned} (\phi \lor p)\land p &= p\\ (\phi \lor\lnot p)\land p &= \phi\land p\\ \end{aligned}$

也就是：

移除所有包含文字的字句
在所有字句中文字被移除

在 BCP 的结尾我们判断如下两件事：

如果有子句为空，这意味着其中原有的文字全部被赋值为假，则合式假
若合式为空，这意味着其中原有的子句全部为真，则合式真

朴素 DPLL 算法

DPLL 算法实际上是应用了 BCP 的朴素搜索算法，也就是在每一步递归中我们分别枚举一个文字为真或者假来不断降低合式中的字句和文字数量，然后递归地判断此时的可行性，并且在每一次枚举之前都应用一次 BCP 算法。我们有伪代码如下：

DPLL(phi)
  phi := BCP(phi)
  if G is empty : 
    return true
  if G contains empty clause : 
    return false
  l := choose-literal(phi)
  return DPLL(assign(l, phi)) || DPLL(assign(l, -phi))

算法本身没有太多值得说的，然而值得注意的是该算法中的 choose-literal 函数，这个函数直接决定了 DPLL 算法的运行效率。

一个朴素的策略是我们每次选取当前在所有子句中出现次数最多的那个文字，然后如果他的极性（正出现的次数减去负出现的次数）为正那么优先将赋值为正，通过这样简单的启发式 (Heuristic) 策略来优化程序。

对初学者来说 DPLL 算法的 cpp 实现可以参考 github 上的 SAT-Solver-DPLL 这个项目。为了避免篇幅过长，DPLL算法的具体实现我会在另一篇文章中详述。

CDCL 冲突驱动子句学习

CDCL 算法相比于 DPLL 算法改进的最大一点在于他将 BCP 过程中遇到的冲突的信息进行记录和学习，并整理为一条新的子句。

参考资料

课件：
SAT问题简介 - 吉建民 | USTC
Conflict Driven Clause Learning - CSE 442 | UWash
A Modern SAT Solver - CSE 507 | UWash

项目：
SAT-Solver-DPLL - sukrutrao | github