前言#

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

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

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

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

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

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

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

子句学习#

假定在上文的例子中，我们的部分赋值为，通过一次 BCP 传播，我们可以得到部分赋值，此时我们发现子句为假，说明我们遇到了冲突

回顾该内容未公开或不可用，我们的做法是撤销的赋值，然后尝试，继续做 BCP

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

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

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

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

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

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

在上图中，决策节点只有两个与

给定两个子句：

C_1 = C \lor x, C_2 = C^\prime \lor \neg x

我们可以归结得到：

C_3 = C_1 \lor C_2 = C \lor C^\prime

归结是 SAT 推理的理论基础

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

假定初始的冲突子句为

此时，学习子句中只有一个是来自于当前决策层的变量，我们就找到了 First-UIP，也得到了学习子句

其思路如下：

首先学习子句设置为空，冲突子句设置为，计数器 open 设置为，我们从冲突子句开始，对子句中的每个文字进行分析：

此时，我们分析完了冲突子句，开始寻找 First-UIP，假定当前的 trail 为，我们后向前进行遍历

第一个被标记为seen且在当前层级的变量是，我们设置 uip 为，将 open 减，并获取的原因子句，并对原因子句进行分析（不分析当前 uip）：
1. 对于，其决策层相同，因此我们不加入学习子句，只是将其标记为 seen 并增加 open 计数（增加）
第二个被标记为seen且在当前层级的变量是，我们设置 uip 为，将 open 减，并获取的原因子句，并对原因子句进行分析（不分析当前 uip）：
1. 这里三个变量都已经被 seen，直接省略
第二个被标记为seen且在当前层级的变量是，此时，open 已经为，我们就找到了 First-UIP，我们将这个文字加入到学习子句中

于是我们得到了学习子句为：

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