冲突分析与子句学习

前言

当 BCP 完成后，如果在这个过程中发现了冲突（有一个子句的文字全部为假），那么我们认为发生了冲突，需要撤销赋值并回溯。

在 DPLL 中，我们的做法十分简单，由于在 trail 中记录了已被赋值的文字，且每个变量是通过决策赋值 $x_i^d$ 还是传播赋值 $x_i^p$ 也被记录

因此我们只需要撤销这次决策后传播的所有变量的赋值，并将决策的变量换一个 相位 进行赋值（类似于 DFS），如果这个决策变量两个相位都被尝试了，那么我们考虑回溯到更早的决策变量，然后尝试新的相位。

Attention

注意，发生冲突并不是坏事，就像 VSIDS 启发式 中说的，想成功先失败，越早的发生冲突意味着我们能越早的剪枝，从而减小搜索空间

在 CDCL 中，我们通过冲突分析与子句学习技术，使得 CDCL 能够进行非时序回溯（也就是回跳），且学习到 CNF 中一些隐含的信息，我们称为学习子句

我们回顾 SAT 问题简介 中提到的实例：

1
p cnf 7 8
2
-5 7 0
3
-1 -5 6 0
4
-1 -6 -7 0
5
-1 -2 5 0
6
-1 -3 5 0
7
-1 -4 5 0
8
-2 -3 -4 5 0
9
-1 2 3 4 5 -6 0

通过这个实例来解释这一节的内容

子句学习

假定在上文的例子中，我们的部分赋值为 $(x_1@1,x_2@2)$，通过一次 BCP 传播，我们可以得到部分赋值 $(x_1@1,x_2@2,x_5@2,x_6@2,x_7@2)$，此时我们发现子句 $(\neg x_1\vee \neg x_6\vee \neg x_7)$ 为假，说明我们遇到了冲突

回顾 DPLL ，我们的做法是撤销 $2,5,6,7$ 的赋值，然后尝试 $(x_1@1,\neg x_2@2)$，继续做 BCP

然而，我们在 CDCL 中可以通过冲突分析，学习到一个 CNF 中蕴含的约束：$\neg x_1\vee \neg x_5$，也就是说 $1,5$ 最多只能有一个为真，有了这样优质的约束，我们就能够快速 BCP 出其他变量的赋值（信息越多，我们能做出的决策就更好）

为了做到子句学习，我们首先引入一些概念

蕴含图 (Implication Graph)

蕴含图记录变量赋值决策和推导关系的有向无环图，例如上文的例子，其蕴含图如下所示：

可以发现我们在第三条子句发生了冲突

唯一蕴含点 (UIP)

在当前的决策层中，如果一个节点满足：从当前决策节点到冲突节点的所有路径都必须经过该节点，则称为 UIP。

第一唯一蕴含点（First-UIP）就是离冲突节点最近的 UIP。

在上图中，决策节点只有两个 $x_1@1$ 与 $x_2@2$

归结（Resolution）

给定两个子句：

$$C_1=C\vee x,C_2=C^{\prime }\vee \neg x$$

我们可以归结得到：

$$C_3=C_1\vee C_2=C\vee C^{\prime }$$

归结是 SAT 推理的理论基础

具体流程

构建学习子句的过程本质就是找到 First-UIP 的过程，以上文为例子，我们的做法是：

假定初始的冲突子句为 $\bar{1}\bar{6}\bar{7}$

1. 忽略 $\bar{1}$，因为是决策得到的

2. $\bar{6}$ 是通过子句 $\bar{1}\bar{5}6$ 得到，我们将冲突子句与原因子句归结，得到 $\bar{1}\bar{5}\bar{7}$

3. $\bar{7}$ 通过子句 $\bar{5}7$ 得到，归结后得到 $\bar{1}\bar{5}$

此时，学习子句中只有一个 $\bar{5}$ 是来自于当前决策层的变量，我们就找到了 First-UIP，也得到了学习子句 $(\neg x_1\vee \neg x_5)$

代码层面的实现

其思路如下：

首先学习子句设置为空，冲突子句设置为 $\bar{1}\bar{6}\bar{7}$ ，计数器 open 设置为 $0$，我们从冲突子句开始，对子句中的每个文字进行分析：

1. 对于 $\bar{1}$，由于我们在第一层进行决策，其决策层小于当前层级，于是我们将其加入学习子句中 $\bar{1}$ ，并将此变量标记为 seen，防止重复添加
2. 对于 $\bar{6}$，决策层级相同，我们不加入学习子句中，但将其标记为 seen 并增加 open 计数（增加 $1$）
3. 对于 $\bar{7}$ ，我们的做法与上一步一样

此时，我们分析完了冲突子句，开始寻找 First-UIP，假定当前的 trail 为 $(x_1@1,x_2@2,x_5@2,x_6@2,x_7@2)$，我们后向前进行遍历

1. 第一个被标记为seen且在当前层级的变量是 $7$，我们设置 uip 为 $7$，将 open 减 $1$，并获取 $7$ 的原因子句 $\bar{5}7$，并对原因子句进行分析（不分析当前 uip）：

   2. 对于 $\bar{5}$，其决策层相同，因此我们不加入学习子句，只是将其标记为 seen 并增加 open 计数（增加 $1$）

2. 第二个被标记为seen且在当前层级的变量是 $6$，我们设置 uip 为 $6$，将 open 减 $1$，并获取 $6$ 的原因子句 $\bar{1}\bar{5}6$，并对原因子句进行分析（不分析当前 uip）：

   4. 这里三个变量都已经被 seen，直接省略

3. 第二个被标记为seen且在当前层级的变量是 $5$，此时，open 已经为 $0$，我们就找到了 First-UIP，我们将 $\bar{5}$ 这个文字加入到学习子句中

于是我们得到了学习子句为：$\neg x_1\vee \neg x_5$

回跳

Tip

在构建完成后，我们会对当前学习子句的文字做一次排序，按照赋值的顺序来排序，那么学习子句会变为 $\neg x_5\vee \neg x_1$

CDCL 找到 First-UIP 后，我们回跳到学习子句第二个文字所在的决策层级，然后撤销 trail 中大于该层级的所有赋值，然后 BCP 或翻转 UIP 的赋值（如果 UIP 是被决策的话）