文章目录

一、前置知识
二、单位传播（Unit Propagation）
三、DPLL（Davis-Putnam-Logemann-Loveland）算法
四、CDCL（Conflict-Driven Clause Learning）算法
- 1. 迹（Trail）与决策层
- 2. 蕴含图（Implication Graph）、子句学习和回溯
参考文献

一、前置知识

文字（literal）：布尔变量变量或其否定称为文字。例如，对于变量ppp，ppp和¬p\neg p¬p都是文字。（其实我也不知道怎么翻译literal qwq）

子句（clause）/简单析取式：仅由有限个文字构成的析取式称为子句或简单析取式。例如对于变量p,q,r,sp,q,r,sp,q,r,s，¬p∨q∨¬r∨s\neg p\lor q\lor\neg r\lor s¬p∨q∨¬r∨s就是一个简单析取式。

合取范式（Conjunctive Normal Form, CNF）：仅由有限个简单析取式构成的合取式称为合取范式。例如对于变量p,q,r,sp,q,r,sp,q,r,s，(p∨¬q)∧(¬p∨r∨s)∧¬r∧(s∨¬s)(p\lor \neg q)\land(\neg p\lor r\lor s)\land \neg r\land(s\lor\neg s)(p∨¬q)∧(¬p∨r∨s)∧¬r∧(s∨¬s)就是一个合取范式。这里为方便起见，可以将合取范式记为集合的形式，例如该范式就可记为{{p,¬q},{¬p,r,s},{¬r},{s,¬s}}\{\{p,\neg q\},\{\neg p,r,s\},\{\neg r\},\{s,\neg s\}\}{{p,¬q},{¬p,r,s},{¬r},{s,¬s}}。

CDCL（Conflict Driven Clause Learning）的目标就是判断一个合取范式是不是可满足的。显然，一个合取范式是可满足的，当且仅当它的每一个子句都是可满足的。而要满足一个子句，只需要使该子句中的某一个文字取真即可。

目前，CDCL是求解这个问题最高效的算法之一。

二、单位传播（Unit Propagation）

单位传播（Unit Propagation, UP）或布尔约束传播（Boolean Constraint Propagation, BCP）或单一文字规则（One-Literal Rule, OLR）是一个能够简化合取范式的方法。

定义单位子句（unit clause）为只有一个文字的子句，例如ppp和¬q\neg q¬q。因为它是在一个合取范式里面的，那么要满足该合取范式，这个单位子句必须为真；而单位子句又只有一个文字，所以这个文字也必须为真。如果一个合取范式包含一个单位子句lll，那么该CNF中的其他子句就可以被lll化简。具体做法如下：

如果某个子句中含有lll，那么就把这个子句移除。

例如，单位子句l=al=al=a，CNF为(a∨¬b∨c)∧a∧(¬d∨e)(a\lor\neg b\lor c)\land a\land(\neg d\lor e)(a∨¬b∨c)∧a∧(¬d∨e)，可以看出该CNF有一个子句是单位子句lll，那么要满足该CNF，就必须满足aaa，即a=1a=1a=1必须成立；而a=1a=1a=1了，那么子句a∨¬b∨ca\lor\neg b\lor ca∨¬b∨c也肯定为真，所以该子句可在CNF中可以被剔除。

也可以用等值演算的方式理解：(a∨¬b∨c)∧a⟺(a∨(¬b∨c))∧a⟺a(a\lor\neg b\lor c)\land a\Longleftrightarrow(a\lor(\neg b\lor c))\land a\Longleftrightarrow a(a∨¬b∨c)∧a⟺(a∨(¬b∨c))∧a⟺a（使用了吸收率）。
如果某个子句中含有¬l\neg l¬l，那就在这个子句中把¬l\neg l¬l移除。

例如，单位子句l=¬al=\neg al=¬a，其否定¬l=a\neg l=a¬l=a；CNF为¬a∧(a∨b∨¬c)∧(d∨¬e∨f)\neg a\land(a\lor b\lor\neg c)\land (d\lor\neg e\lor f)¬a∧(a∨b∨¬c)∧(d∨¬e∨f)，可以看出该CNF有一个子句是单位子句lll，另一个子句a∨b∨¬ca\lor b\lor\neg ca∨b∨¬c中含有¬l=a\neg l=a¬l=a。要满足该CNF，lll必须为真，aaa必须为假；既然aaa为假，a∨b∨¬ca\lor b\lor\neg ca∨b∨¬c就是0∨b∨c0\lor b\lor c0∨b∨c，也就是b∨cb\lor cb∨c，因此可以把aaa也就是¬l\neg l¬l去掉。

用等值演算的方式理解：¬a∧(a∨b∨¬c)⟺(¬a∧a)∨(¬a∧(b∨¬c))⟺0∨(¬a∧(b∨¬c))⟺¬a∧(b∨¬c)\neg a\land(a\lor b\lor\neg c)\Longleftrightarrow(\neg a\land a)\lor(\neg a\land(b\lor\neg c))\Longleftrightarrow0\lor(\neg a\land(b\lor\neg c))\Longleftrightarrow\neg a\land(b\lor\neg c)¬a∧(a∨b∨¬c)⟺(¬a∧a)∨(¬a∧(b∨¬c))⟺0∨(¬a∧(b∨¬c))⟺¬a∧(b∨¬c)。

一个综合的例子：设CNF为(a∨b)∧(¬a∨c)∧(¬c∨d)∧a(a\lor b)\land(\neg a\lor c)\land(\neg c\lor d)\land a(a∨b)∧(¬a∨c)∧(¬c∨d)∧a，那么用aaa把前两个子句处理得到c∧(¬c∨d)∧ac\land(\neg c\lor d)\land ac∧(¬c∨d)∧a。此时还可以用ccc继续处理，得到c∧d∧ac\land d\land ac∧d∧a。

当然，实际应用中会出现单位子句的情况是很少的。不过，我们仍然可以创造条件来应用单位传播方法。对于一个含有多个文字的子句，我们可以令其中一个文字为真，其他文字均为假，就可以把它变成一个单位子句。例如对于CNF：(a∨¬b∨c)∧(¬b∨¬c∨d)(a\lor\neg b\lor c)\land(\neg b\lor\neg c\lor d)(a∨¬b∨c)∧(¬b∨¬c∨d)，令a=0,b=1a=0,b=1a=0,b=1，则由于第一个子句为真，要求ccc必须为真。此时就可以应用单位传播方法，将第二个子句化为¬b∨d\neg b\lor d¬b∨d。

再令a=0,c=0a=0,c=0a=0,c=0，则必有b=0b=0b=0，此时可以把第二个子句直接剔除。

也可以用等值演算理解：(a∨¬b∨c)∧(¬b∨¬c∨d)⟺(a∧¬b)∨(a∧¬c)∨(a∧¬d)∨(¬b∧¬b)∨(¬b∧¬c)∨(¬b∧¬d)∨(c∧¬b)∨(c∧¬c)∨(c∧¬d)⟺(a∧¬b)∨(a∧¬c)∨(a∧¬d)∨¬b∨(¬b∧¬c)∨(¬b∧¬d)∨(c∧¬b)∨(c∧¬d)⟺(a∧¬b)∨(a∧¬c)∨(a∧¬d)∨¬b∨(c∧¬d)\begin{aligned}(a\lor\neg b\lor c)\land(\neg b\lor\neg c\lor d)&\Longleftrightarrow(a\land\neg b)\lor(a\land\neg c)\lor(a\land\neg d)\lor(\neg b\land\neg b)\lor(\neg b\land\neg c)\lor(\neg b\land\neg d)\lor(c\land\neg b)\lor(c\land\neg c)\lor(c\land\neg d)\\&\Longleftrightarrow(a\land\neg b)\lor(a\land\neg c)\lor(a\land\neg d)\lor\neg b\lor(\neg b\land\neg c)\lor(\neg b\land\neg d)\lor(c\land\neg b)\lor(c\land\neg d)\\&\Longleftrightarrow(a\land\neg b)\lor(a\land\neg c)\lor(a\land\neg d)\lor\neg b\lor(c\land\neg d)\end{aligned}(a∨¬b∨c)∧(¬b∨¬c∨d)⟺(a∧¬b)∨(a∧¬c)∨(a∧¬d)∨(¬b∧¬b)∨(¬b∧¬c)∨(¬b∧¬d)∨(c∧¬b)∨(c∧¬c)∨(c∧¬d)⟺(a∧¬b)∨(a∧¬c)∨(a∧¬d)∨¬b∨(¬b∧¬c)∨(¬b∧¬d)∨(c∧¬b)∨(c∧¬d)⟺(a∧¬b)∨(a∧¬c)∨(a∧¬d)∨¬b∨(c∧¬d)其中，a=0,b=1,c=1a=0,b=1,c=1a=0,b=1,c=1对应式中的c∧¬dc\land\neg dc∧¬d项，a=0,c=0,b=0a=0,c=0,b=0a=0,c=0,b=0对应式中的¬b\neg b¬b项。

有时对某个单位子句应用单位传播可能会导致另一个子句成为单位子句（例如我们上面举的综合例子），因此算法会不断地应用单位传播方法，直到化到最简为止。

三、DPLL（Davis-Putnam-Logemann-Loveland）算法

要讲CDCL，就不得不提到DPLL，因为CDCL是DPLL的进化版。

DPLL是一种基于回溯的算法，它的核心步骤就是单位传播（CDCL也是一样）。一个朴素的回溯算法可能会尝试每种可能的赋值，直到找到一组成真赋值为止。而DPLL可以利用单位传播来进行“更聪明”的猜测，从而减小搜索树的大小（可以将单位传播看成一种剪枝策略）。

在求解的过程中，如果我们发现某个子句的真值为真，就删除这个子句；如果发现某个文字的真值为假，就在子句中删除这个变量。这样，最后发现CNF为空，就说明所有子句都满足了，即该CNF是可满足的；如果发现CNF中有一个子句为空而该子句没有被删除，说明这个子句的所有文字取值都为假，于是这个子句不能满足，此次赋值尝试是失败的。

我们先看一下朴素算法的伪代码：

朴素算法(CNF):找到CNF中下一个没有被赋值的变量;if 找到了:return 朴素算法(CNF中这个变量为真) || 朴素算法(CNF中这个变量为假);else: // 没找到，说明所有变量均已赋值return CNF在该组赋值下的真值;

再看一下DPLL的伪代码：

DPLL(CNF):while CNF含有单位子句:对该CNF使用单位传播;if CNF为空:return true;else if CNF有空子句:return false;else: // 仍不能确定CNF的值，需要对更多的变量赋值找到CNF中下一个没有被赋值的变量（或文字）;return DPLL(CNF中这个变量为真) || DPLL(CNF中这个变量为假);

可以在Conflict Driven Clause Learning (cse442-17f.github.io)看一个交互式的例子，对理解这个算法很有帮助。

下面给出DPLL的Python代码，使用sympy库：

from sympy import Symbol
from sympy.logic.boolalg import Not
from typing import *
from copy import deepcopyLiteral = Union[Symbol, Not]class ConjunctiveNormalForm: # 合取范式类def __init__(self, l: List[Set[Literal]]):# l: 集合的列表，里面的集合是子句，外面的列表是CNFself.cnf = lself.preprocess()def preprocess(self):for clause in list(self.cnf):for literal in clause:if ~literal in clause:self.cnf.remove(clause) # x | ~x等价于1，删除该子句breakdef find_unit_clause(self): # 找到单位子句for clause in self.cnf:if len(clause) == 1:return list(clause)[0] # 返回单位子句含有的文字return None # 找不到，返回Nonedef unit_propagation(self, literal: Literal):# 以文字literal对cnf进行单位传播for clause in list(self.cnf): # 需要拷贝self.cnfif literal in clause: # 含有literal的子句直接删除self.cnf.remove(clause)for clause in self.cnf:if ~literal in clause:clause.remove(~literal) # 删除literal的否定def evaluate(self): # 对CNF求值if len(self.cnf) == 0: # CNF为空，可满足return Trueelif set() in self.cnf: # CNF含有空子句，不满足（出现矛盾）return Falsereturn None # 无法确定，返回Nonedef find_next_unvaluated_literal(self): # 找到下一个没有被赋值的文字return list(self.cnf[0])[0] # 直接返回第一个子句的第一个文字def DPLL(c: ConjunctiveNormalForm):literal = Nonewhile True: # 不断使用单位传播，直到没有单位子句为止literal = c.find_unit_clause() # 找到单位子句包含的文字if literal == None: # 无单位子句，退出循环breakc.unit_propagation(literal) # 执行单位传播v = c.evaluate() # 求值if v == True:return Trueelif v == False:return Falseelse: # 仍不能确定CNF的值，向下递归literal = c.find_next_unvaluated_literal()# 找到下一个没有被赋值的文字c1 = ConjunctiveNormalForm(deepcopy(c.cnf))c1.unit_propagation(literal) # 让这个文字取真if DPLL(c1):return Truec2 = ConjunctiveNormalForm(deepcopy(c.cnf))c2.unit_propagation(~literal) # 让这个文字取假if DPLL(c2):return Truereturn False

示例：对合取范式(¬c)∧(¬b)∧(d∨e)∧(¬a)∧(a∨c)(\neg c)\land(\neg b)\land(d\lor e)\land(\neg a)\land(a\lor c)(¬c)∧(¬b)∧(d∨e)∧(¬a)∧(a∨c)进行DPLL：

from sympy import symbols
a, b, c, d, e = symbols('a b c d e')
l = [[~c], [~b], [d, e], [~a], [a, c]]
print(DPLL(ConjunctiveNormalForm(l))) # 输出True

DPLL是一个很简单的算法，不过就是朴素算法加上单位传播而已（当然也可以采用其他改进策略进一步优化，比如采用“纯文字”（pure literal）法等）。它的最坏复杂度仍然是指数级别的。

四、CDCL（Conflict-Driven Clause Learning）算法

Conflict-Driven Clause Learning，直译过来是“冲突驱动的子句学习”，也就是从冲突中吸取教训，做出更合理的猜测。所谓冲突，就是出现某个子句的所有文字都为false，使得该子句不可能被满足。出现这种情况时，我们可以从中总结出关于文字取值的一些限制，根据这些限制进行决策，进而提升算法效率。CDCL相比于DPLL最大的特点是“non-chronological back-jumping”，即“非时序性回溯”，换言之就是回溯时不一定回到上一层，而可能回到上几层。

从冲突中吸取教训的过程称为子句学习。当冲突发生时，我们分析冲突发生的原因，学习一个新的子句并加入CNF中，该子句可以使得这个冲突被避免，并且其他类似的冲突也可能被避免。完成子句学习后，我们进行回溯，回溯到哪一层取决于刚才分析的结果。

下面给出CDCL的伪代码。因为使用递归不容易实现回溯到上面几层的过程，所有我们使用非递归写法，并引入“决策层”（Decision Level）的概念。

CDCL(CNF):副本 = CNF // 创建CNF的副本，不更改原CNFwhile true:while 副本含有单位子句:对副本使用单位传播;if 副本中含有取值为假的子句: // 发现冲突if 现在的决策层是0:return false; // 不能满足C = 子句学习(CNF, 副本) // 吸取教训根据C回到一个更早的决策层; // 调整策略else:if 所有变量都被赋值:return true; // 可满足else: // 进行一次决策（决策就是一次尝试，令某个文字为真，撞大运）开始一个新的决策层;找到一个未赋值的文字l;副本 = 副本∧{l}// 给l赋值为真// 加入l构成的单位子句，使得副本要满足就是l要满足，变相地要求l为真// 对于变量x，若给x赋值为真，就令l = x；若给x赋值为假，就令l = ¬x

那么下面我们就细致地实现这个算法。

1. 迹（Trail）与决策层

要分析冲突出现的原因，我们需要记得在当前采用的赋值下为什么某个文字会取一个特定的值，这样才能不断地调整策略。这个实现记忆功能的结构就是迹。迹是一串连在一起的文字，里面出现的每个文字代表这个文字赋值为真；同时我们要记录为什么这个文字赋值为真，于是在文字的右上角标注原因。当文字是因为一次决策取真时，我们就标“决策”；当文字因为副本中的某个子句而被迫取真时，我们就标注这个子句。例如：x1决策⋅x2(¬x1∨x2)⋅¬x3(¬x1∨¬x3)⋅¬x4(¬x1∨¬x2∨¬x4)x_1^{\text{决策}}\cdot x_2^{(\neg x_1\lor x_2)}\cdot\neg x_3^{(\neg x_1\lor \neg x_3)}\cdot\neg x_4^{(\neg x_1\lor\neg x_2\lor \neg x_4)}x1决策⋅x2(¬x1∨x2)⋅¬x3(¬x1∨¬x3)⋅¬x4(¬x1∨¬x2∨¬x4)代表如下含义：首先x1x_1x1在一次决策中被赋值为真；CNF中有子句¬x1∨x2\neg x_1\lor x_2¬x1∨x2，要满足这个子句，因为¬x1\neg x_1¬x1为假，所以x2x_2x2必为真；又根据子句¬x1∨¬x3\neg x_1\lor\neg x_3¬x1∨¬x3，可知¬x3\neg x_3¬x3必为真，即x3x_3x3必为假；而在子句¬x1∨¬x2∨¬x4\neg x_1\lor\neg x_2\lor \neg x_4¬x1∨¬x2∨¬x4中，¬x1\neg x_1¬x1和¬x2\neg x_2¬x2都为假，那么¬x4\neg x_4¬x4只能取真。

如何动态地维护迹呢？我们采用如下规则：

如果算法做出决策使文字lll为真，那么在迹的末尾添加l决策l^{\text{决策}}l决策；
如果算法在子句C={l1∨l2∨⋯∨lk∨l}C=\{l_1\lor l_2\lor\cdots\lor l_k\lor l\}C={l1∨l2∨⋯∨lk∨l}上实施单位传播，而l1,l2,⋯,lkl_1,l_2,\cdots,l_kl1,l2,⋯,lk都赋值为假，这使得lll只能取真，那么就在迹的末尾添加lCl^ClC；
如果算法回溯了，那么某些元素将被从迹的末尾被移除。

这样，现在的赋值就可以从迹中清楚地看出来。我们定义迹中一个文字的决策层是迹中该文字前面（包含它自己）决策文字（即右上角标注为“决策”）的个数。换言之，决策层就是目前有多少个变量是由决策而赋值的。例如，在迹x1决策⋅¬x2(¬x1∨¬x2)⋅x3决策⋅x4(¬x1∨¬x3∨x4)x_1^{\text{决策}}\cdot\neg x_2^{(\neg x_1\lor\neg x_2)}\cdot x_3^{\text{决策}}\cdot x_4^{(\neg x_1\lor\neg x_3\lor x_4)}x1决策⋅¬x2(¬x1∨¬x2)⋅x3决策⋅x4(¬x1∨¬x3∨x4)中，x1x_1x1、x2x_2x2的决策层是111，x3x_3x3、x4x_4x4的决策层是222。

2. 蕴含图（Implication Graph）、子句学习和回溯

前面介绍的迹是一个线性结构，但如果我们把推导的关系也考虑进来，那么我们将会看到它变成一个有向无环图。事实上，算法不会真的去构建这样一张图，而是会直接使用迹来进行运算。

考虑CNF为(¬x1∨¬x2)∧(¬x1∨x3)∧(¬x3∨¬x4)∧(x2∨x4∨x5)∧(¬x5∨x6∨¬x7)∧(x2∨x7∨x8)∧(¬x8∨¬x9)∧(¬x8∨x10)∧(x9∨¬x10∨x11)∧(¬x10∨¬x12)∧(¬x11∨x12)\begin{aligned}(\neg{x_1} \lor \neg{x_2}) \land(\neg{x_1} \lor x_3) \land(\neg{x_3} \lor \neg{x_4}) \land(x_2 \lor x_4 \lor x_5) \land(\neg{x_5} \lor x_6 \lor \neg{x_7}) \land(x_2 \lor x_7 \lor x_8) \land(\neg{x_8} \lor \neg{x_9})\\\land(\neg{x_8} \lor x_{10}) \land(x_9 \lor \neg{x_{10}} \lor x_{11}) \land(\neg{x_{10}} \lor \neg{x_{12}}) \land (\neg{x_{11}} \lor x_{12})\end{aligned}(¬x1∨¬x2)∧(¬x1∨x3)∧(¬x3∨¬x4)∧(x2∨x4∨x5)∧(¬x5∨x6∨¬x7)∧(x2∨x7∨x8)∧(¬x8∨¬x9)∧(¬x8∨x10)∧(x9∨¬x10∨x11)∧(¬x10∨¬x12)∧(¬x11∨x12)首先我们决定令x1x_1x1为真，那么经过单位传播后得出迹为x1决策⋅¬x2(¬x1∨¬x2)⋅x3(¬x1∨x3)⋅¬x4(¬x3∨¬x4)⋅x5(x2∨x4∨x5)x_1^{\text{决策}}\cdot\neg x_2^{(\neg x_1\lor\neg x_2)}\cdot x_3^{(\neg x_1\lor x_3)}\cdot\neg x_4^{(\neg x_3\lor\neg x_4)}\cdot x_5^{(x_2\lor x_4\lor x_5)}x1决策⋅¬x2(¬x1∨¬x2)⋅x3(¬x1∨x3)⋅¬x4(¬x3∨¬x4)⋅x5(x2∨x4∨x5)。我们可以总结出变量之间的蕴含关系：

已知x1x_1x1为真，根据子句(¬x1∨¬x2)(\neg{x_1} \lor \neg{x_2})(¬x1∨¬x2)有¬x2\neg x_2¬x2，故x1⊨¬x2x_1\models\neg x_2x1⊨¬x2；
已知x1x_1x1为真，根据子句(¬x1∨x3)(\neg{x_1} \lor {x_3})(¬x1∨x3)有x3x_3x3，故x1⊨x3x_1\models x_3x1⊨x3；
已知x3x_3x3为真，根据子句(¬x3∨¬x4)(\neg x_3\lor\neg x_4)(¬x3∨¬x4)有¬x4\neg x_4¬x4，故x3⊨¬x4x_3\models\neg x_4x3⊨¬x4；
已知x2x_2x2为假、x4x_4x4为假，根据子句(x2∨x4∨x5)(x_2\lor x_4\lor x_5)(x2∨x4∨x5)有x5x_5x5，故¬x2,¬x4⊨x5\neg x_2,\neg x_4\models x_5¬x2,¬x4⊨x5。

由此，我们可以把变量之间的蕴含关系画成一张图：

其中x2‾\overline{x_2}x2表示¬x2\neg x_2¬x2，左下角的数字是决策层。要继续运算，就必须再做出一次决策，决定x6x_6x6的值。我们决定x6x_6x6为假（此时开启了新的决策层），那么迹就变成了：x1决策⋅¬x2(¬x1∨¬x2)⋅x3(¬x1∨x3)⋅¬x4(¬x3∨¬x4)⋅x5(x2∨x4∨x5)⋅¬x6决策⋅¬x7(¬x5∨x6∨¬x7)⋅x8(x2∨x7∨x8)⋅¬x9(¬x8∨¬x9)⋅x10(¬x8∨x10)⋅x11(x9∨¬x10∨x11)⋅¬x12(¬x10∨¬x12)\begin{aligned}x_1^{\text{决策}}\cdot\neg x_2^{(\neg x_1\lor\neg x_2)}\cdot x_3^{(\neg x_1\lor x_3)}\cdot\neg x_4^{(\neg x_3\lor\neg x_4)}\cdot x_5^{(x_2\lor x_4\lor x_5)}\cdot\\\neg x_6^{\text{决策}}\cdot\neg x_7^{(\neg x_5\lor x_6\lor\neg x_7)}\cdot x_8^{(x_2\lor x_7\lor x_8)}\cdot\neg x_9^{(\neg x_8\lor\neg x_9)}\cdot x_{10}^{(\neg x_8\lor x_{10})}\cdot x_{11}^{(x_9\lor\neg x_{10}\lor x_{11})}\cdot\neg x_{12}^{(\neg x_{10}\lor\neg x_{12})}\end{aligned}x1决策⋅¬x2(¬x1∨¬x2)⋅x3(¬x1∨x3)⋅¬x4(¬x3∨¬x4)⋅x5(x2∨x4∨x5)⋅¬x6决策⋅¬x7(¬x5∨x6∨¬x7)⋅x8(x2∨x7∨x8)⋅¬x9(¬x8∨¬x9)⋅x10(¬x8∨x10)⋅x11(x9∨¬x10∨x11)⋅¬x12(¬x10∨¬x12)对应的蕴含图如下：

CNF中还有一个子句(¬x11∨x12)(\neg x_{11}\lor x_{12})(¬x11∨x12)，但x11x_{11}x11为真、x12x_{12}x12为假，所以这个子句不能被满足，也就是说我们发现了矛盾，用⊥\perp⊥表示。该⊥\perp⊥节点的入边是由造成冲突的子句(¬x11∨x12)(\neg x_{11}\lor x_{12})(¬x11∨x12)产生的。

现在我们在数学上给出蕴含图的定义：

设有迹π\piπ。一个对应的蕴含图GπG_\piGπ是一个有向无环图(V,E)(V,E)(V,E)，其中点集V={l∣lr∈π}V=\left\{l|l^r\in\pi\right\}V={l∣lr∈π}（也就是π\piπ中出现的文字集）。边集EEE的构造方式如下：对于CNF中的每个子句C=(l1∨l2∨⋯∨lk∨l)C=(l_1\lor l_2\lor\cdots\lor l_k\lor l)C=(l1∨l2∨⋯∨lk∨l)，若lC∈πl^C\in\pilC∈π，则EEE含有边(¬li,l)(\neg l_i,l)(¬li,l)，1≤i≤k1\le i\le k1≤i≤k。此外，如果π\piπ的赋值使得子句C=(l1∨l2∨⋯∨lk)C=(l_1\lor l_2\lor\cdots\lor l_k)C=(l1∨l2∨⋯∨lk)不可满足，则VVV还含有一个特殊的冲突节点⊥\perp⊥，EEE还含有边(¬li,⊥)(\neg l_i,\perp)(¬li,⊥)，1≤i≤k1\le i\le k1≤i≤k。

显然，蕴含图是有向无环图，且决策文字的节点（包含xj决策x_j^{决策}xj决策的节点）入度为000（上图中的x1x_1x1和x6‾\overline{x_6}x6）。迹就是蕴含图的一个拓扑序。

有了蕴含图，我们就可以分析冲突出现的原因。在上例中，为什么子句(¬x11∨x12)(\neg x_{11}\lor x_{12})(¬x11∨x12)不能满足呢？因为x11x_{11}x11为真且x12x_{12}x12为假。为什么x11x_{11}x11为真且x12x_{12}x12为假呢？因为x9x_9x9为假且x10x_{10}x10为真。为什么x9x_9x9为假且x10x_{10}x10为真呢？因为x8x_8x8为真。为什么x8x_8x8为真呢？因为x2x_2x2为假且x7x_7x7为假。……依此类推，最终推出原因是x1x_1x1为真且¬x6\neg x_6¬x6为假。为了吸取教训、不让冲突再次发生，我们可以在CNF中加入一个子句来约束决策的过程。比如可以加入(x9∨¬x10)(x_9\lor\neg x_{10})(x9∨¬x10)、¬x8\neg x_8¬x8、(¬x1∨x6)(\neg x_1\lor x_6)(¬x1∨x6)等。有了这个子句约束，下次决策时就不会得到相同的冲突了。这个用于约束的子句就是我们学习到的子句。

要对学到的子句进行数学上的描述，就需要用到点割集的概念。设蕴含图Gπ=(V,E)G_\pi=(V,E)Gπ=(V,E)，它的一个冲突切割（conflict cut）就是点集VVV的一个分割W=(A,B)W=(A,B)W=(A,B)，使得：

所有决策文字的节点属于AAA；
冲突节点属于BBB；
A∩B=∅A\cap B=\emptysetA∩B=∅；
A∪B=VA\cup B=VA∪B=V。

令R={l∈A∣∃l′∈B,(l,l′)∈E}R=\{l\in A|\exists l'\in B,(l,l')\in E\}R={l∈A∣∃l′∈B,(l,l′)∈E}称为该冲突切割的原因集（reason set），它包含的是AAA中有连到BBB的边的节点的集合，它是GπG_\piGπ的一个点割集。

那么，该冲突切割对应的学到的子句就是⋁l∈R¬l\bigvee\limits_{l\in R}\neg ll∈R⋁¬l。

接下来，我们对刚才的例子考察冲突切割：

在下面的切割中，A={x1,¬x6}A=\{x_1,\neg x_6\}A={x1,¬x6}，R={x1,¬x6}R=\{x_1,\neg x_6\}R={x1,¬x6}，学到的子句是¬x1∨x6\neg x_1\lor x_6¬x1∨x6。
在下面的切割中，A={x1,¬x2,x3,¬x4,x5,¬x6}A=\{x_1,\neg x_2,x_3,\neg x_4,x_5,\neg x_6\}A={x1,¬x2,x3,¬x4,x5,¬x6}，R={¬x2,x5,¬x6}R=\{\neg x_2,x_5,\neg x_6\}R={¬x2,x5,¬x6}，学到的子句是x2∨¬x5∨x6x_2\lor\neg x_5\lor x_6x2∨¬x5∨x6。
在下面的切割中，A={x1,¬x2,x3,¬x4,x5,¬x6,¬x7,x8}A=\{x_1,\neg x_2,x_3,\neg x_4,x_5,\neg x_6,\neg x_7,x_8\}A={x1,¬x2,x3,¬x4,x5,¬x6,¬x7,x8}，R={x8}R=\{x_8\}R={x8}，学到的子句是¬x8\neg x_8¬x8。
A={x1,¬x2,x3,¬x4,x5,¬x6,x10}A=\{x_1,\neg x_2,x_3,\neg x_4,x_5,\neg x_6,x_{10}\}A={x1,¬x2,x3,¬x4,x5,¬x6,x10}，R={¬x2,x5,¬x6,x10}R=\{\neg x_2,x_5,\neg x_6,x_{10}\}R={¬x2,x5,¬x6,x10}，学到的子句是x2∨¬x5∨x6∨¬x10x_2\lor\neg x_5\lor x_6\lor\neg x_{10}x2∨¬x5∨x6∨¬x10。

冲突切割有很多，那到底选哪一个进行学习呢？实践中，我们只关心具有某些特性的冲突切割。我们希望学到的子句最好能引发新的单位传播过程。

唯一蕴含点（unique implication point, UIP）：如果蕴含图GπG_\piGπ中的某个节点lll是唯一蕴含点，那么设ddd是最近一次做决策的节点（即包含决策层最深的决策文字的节点），ddd到冲突节点的所有路径都必须经过lll。例如上图中d=x6‾d=\overline{x_6}d=x6，冲突节点为⊥\perp⊥，lll可以是x6‾\overline{x_6}x6，x7‾\overline{x_7}x7或x8x_8x8。

如果lll是一个唯一蕴含点，那么对应的唯一蕴含冲突切割（UIP cut）是(A,B)(A,B)(A,B)，其中BBB包含了所有是lll的后继、并且有到冲突节点的路径的节点。AAA则包含了剩下的节点。

注意：唯一蕴含冲突切割的原因集并不一定只包含唯一蕴含点。

注意到唯一蕴含点是必然存在的，因为最近一次做决策的节点就是唯一蕴含点。特别地，我们使用第一个唯一蕴含冲突切割（first UIP cut）：使集合AAA尽可能大的唯一蕴含冲突切割（这是为了减少回溯的层数，充分利用前面的计算结果）。

再次考察下面的蕴含图。它的最近一次做决策的节点是x6‾\overline{x_6}x6，因为它的决策层最深，是222。它有三个蕴含点：x6‾,x7‾,x8\overline{x_6},\overline{x_7},x_8x6,x7,x8。

下图所示的冲突切割不是唯一蕴含冲突切割，因为集合BBB含有除唯一蕴含点x6‾\overline{x_6}x6的后继以外的节点x1x_1x1。
下图是唯一蕴含冲突切割，但不是第一个唯一蕴含冲突切割。
下图也是唯一蕴含冲突切割，但也不是第一个唯一蕴含冲突切割。
下图就是第一个唯一蕴含冲突切割。

假设我们从唯一蕴含冲突切割中学到的子句是CCC，那么CCC其实是CNF的一个逻辑上的结果，不满足CCC就不满足CNF。

经过学习之后，CDCL算法现在进行非时序性回溯：

令mmm是CCC的文字中第二深的决策层（如果CCC中的文字全部都是一个决策层，则m=0m=0m=0）；
从迹中删除所有决策层大于mmm的文字。

这样的回溯策略可以撤销最近一次决策，并在上一个决策层应用我们学到的子句进而运行单位传播，以此来更快地决定某些变量的值。

论断 CCC中有且仅有一个文字属于最近的一个决策层。

证明：设CCC是由唯一蕴含冲突切割(A,B)(A,B)(A,B)中学到的，我们令该切割中的唯一蕴含点为lll，那么从最近一次决策的点ddd到冲突节点⊥\perp⊥的所有路径都经过lll。显然lll属于原因集RRR，因此lll在CCC中出现。若有另一个节点uuu也在CCC中出现且uuu和ddd在一个决策层，那么uuu是ddd的后继，而且u∈Ru\in Ru∈R。于是∃u′∈B\exists u'\in B∃u′∈B使得(u,u′)∈E(u,u')\in E(u,u′)∈E。设所有从ddd出发经过uuu和u′u'u′到⊥\perp⊥的路径集合为PPP，我们证明一定存在p∈Pp\in Pp∈P使得ppp不经过lll。

首先，若p=d→u→u′→⊥p=d\to u\to u'\to\perpp=d→u→u′→⊥经过lll，那么lll一定不在u→u′u\to u'u→u′和u′→⊥u'\to\perpu′→⊥段，因为l∈Al\in Al∈A。于是lll只能在d→ud\to ud→u上出现。那么所有从ddd到uuu的路径都经过lll吗？如果是这样，则uuu是lll的后继，而uuu又有到⊥\perp⊥的路径，因此根据唯一蕴含冲突切割的定义，应有u∈Bu\in Bu∈B，这与u∈R⊆Au\in R\subseteq Au∈R⊆A矛盾。因此这样的uuu不存在，论断得证。

推论若CCC中的文字全部都是一个决策层，则CCC只含有一个文字。

在CCC只含有一个文字lll的情况下，lll取真是冲突发生的全部原因；换言之，只要lll取真，那么冲突一定会发生，与前面做了什么决策无关。因此¬l\neg l¬l是CNF的直接推论，它应该在决策层为000时就得到应用。此时我们回溯到m=0m=0m=0层。

还是考察上面的例子。唯一蕴含点为x8x_8x8，C=¬x8C=\neg x_8C=¬x8，得到这个子句后算法回到第000层并以¬x8\neg x_8¬x8进行单位传播。最后得到的迹为¬x8(¬x8)\color{green}\neg x_8^{(\neg x_8)}¬x8(¬x8)。

再给出一个回溯到第一层的例子。如果我们采用下图所示的唯一蕴含冲突切割：

C=x2∨¬x5∨x6C=x_2\lor\neg x_5\lor x_6C=x2∨¬x5∨x6，m=1m=1m=1，在迹中删除决策层大于111的文字后应用CCC进行单位传播，得到的新迹是x1决策⋅¬x2(¬x1∨¬x2)⋅x3(¬x1∨x3)⋅¬x4(¬x3∨¬x4)⋅x5(x2∨x4∨x5)⋅x6(x2∨¬x5∨x6)x_1^{\text{决策}}\cdot\neg x_2^{(\neg x_1\lor\neg x_2)}\cdot x_3^{(\neg x_1\lor x_3)}\cdot\neg x_4^{(\neg x_3\lor\neg x_4)}\cdot x_5^{(x_2\lor x_4\lor x_5)}\cdot\color{green}x_6^{(x_2\lor\neg x_5\lor x_6)}x1决策⋅¬x2(¬x1∨¬x2)⋅x3(¬x1∨x3)⋅¬x4(¬x3∨¬x4)⋅x5(x2∨x4∨x5)⋅x6(x2∨¬x5∨x6)。

总的来说，

对于可满足的CNF，CDCL算法最终找到一个成真赋值，赋值方式存储在迹中。
对于不可满足的CNF，CDCL算法最终会返回“不可满足”（false）。这是因为每次冲突都会产生一个新的子句，而只存在有限个可能的子句，因此在某一时刻算法会产生足够多的单位子句，进而在决策层000产生一个冲突，这表示CNF是不可满足的。或者也可以这样理解：在学到的子句的约束下，同一组赋值一定不会出现第二次，而赋值可能的组数是有限的，所以算法一定会在有限步内停止。

下面给出一个CDCL在一个例子上的具体工作流程：

设CNF为(a∨b∨c)∧(a∨b∨¬c)∧(¬b∨d)∧(a∨¬b∨¬d)∧(¬a∨e∨f)∧(¬a∨e∨¬f)∧(¬e∨¬f)∧(¬a∨¬e∨f)(a\lor b\lor c)\land(a\lor b\lor\neg c)\land(\neg b\lor d)\land(a\lor\neg b\lor\neg d)\land(\neg a\lor e\lor f)\land(\neg a\lor e\lor\neg f)\land(\neg e\lor\neg f)\land(\neg a\lor\neg e\lor f)(a∨b∨c)∧(a∨b∨¬c)∧(¬b∨d)∧(a∨¬b∨¬d)∧(¬a∨e∨f)∧(¬a∨e∨¬f)∧(¬e∨¬f)∧(¬a∨¬e∨f)。那么CDCL可以按照如下的步骤运作：

该CNF不含单位子句，因此在决策层000我们不做任何事。
在决策层111，我们做出一次决策：令aaa为假。单位传播不做任何事，因此迹为¬a决策\neg a^{\text{决策}}¬a决策。
在决策层222，我们再做一次决策：令bbb为假。对子句(a∨b∨c)(a\lor b\lor c)(a∨b∨c)进行单位传播，得到ccc为真，因此迹为¬a决策⋅¬b决策⋅c(a∨b∨c)\neg a^{\text{决策}}\cdot\neg b^{\text{决策}}\cdot c^{(a\lor b\lor c)}¬a决策⋅¬b决策⋅c(a∨b∨c)。此时我们发现：子句(a∨b∨¬c)(a\lor b\lor\neg c)(a∨b∨¬c)为假，我们得到了一个冲突。

最近一次做决策的节点是b‾\overline bb，它同时也是唯一蕴含点。A={a‾,b‾}A=\{\overline a,\overline b\}A={a,b}，B={c,⊥}B=\{c,\perp\}B={c,⊥}，原因集R={a‾,b‾}R=\{\overline a,\overline b\}R={a,b}，学习到的子句C=(a∨b)C=(a\lor b)C=(a∨b)。其中a‾\overline aa的决策层是111，b‾\overline bb的决策层是222，因此m=1m=1m=1，回到决策层111。
在决策层111，首先利用学到的子句(a∨b)(a\lor b)(a∨b)进行单位传播，推出bbb为真，然后根据(¬b∨d)(\neg b\lor d)(¬b∨d)推出ddd为真。现在的迹是¬a决策⋅b(a∨b)⋅d(¬b∨d)\neg a^{\text{决策}}\cdot b^{(a\lor b)}\cdot d^{(\neg b\lor d)}¬a决策⋅b(a∨b)⋅d(¬b∨d)。然而，我们又发现了冲突：子句(a∨¬b∨¬d)(a\lor\neg b\lor\neg d)(a∨¬b∨¬d)不能满足。

最近一次做决策的节点是a‾\overline aa，它同时也是唯一蕴含点。A={a‾}A=\{\overline a\}A={a}，B={b,d,⊥}B=\{b,d,\perp\}B={b,d,⊥}，原因集R={a‾}R=\{\overline a\}R={a}，学到的子句C=(a)C=(a)C=(a)，仅含有一个文字，故算法回溯到第000层。
在决策层000，利用学到的子句(a)(a)(a)进行单位传播，没有推测出其它变量的值。现在的迹是a(a)a^{(a)}a(a)。
在决策层111，我们做出一次决策：令eee为假。进行单位传播：根据子句(¬a∨e∨f)(\neg a\lor e\lor f)(¬a∨e∨f)，得知fff为真。现在的迹是a(a)⋅¬e决策⋅f(¬a∨e∨f)a^{(a)}\cdot\neg e^{\text{决策}}\cdot f^{(\neg a\lor e\lor f)}a(a)⋅¬e决策⋅f(¬a∨e∨f)。此时我们发现子句(¬a∨e∨¬f)(\neg a\lor e\lor\neg f)(¬a∨e∨¬f)不能满足。

最近一次做决策的节点是e‾\overline ee，它同时也是唯一蕴含点。A={a,e‾}A=\{a,\overline e\}A={a,e}，B={f,⊥}B=\{f,\perp\}B={f,⊥}，原因集R={a,e‾}R=\{a,\overline e\}R={a,e}，学到的子句C=(¬a∨e)C=(\neg a\lor e)C=(¬a∨e)，其中aaa在第000层，e‾\overline ee在第111层，m=1m=1m=1，回溯到第000层。
在决策层000，利用子句(a)(a)(a)进行对学到的子句C=(¬a∨e)C=(\neg a\lor e)C=(¬a∨e)单位传播，得到(e)(e)(e)。再进行单位传播，根据子句(¬e∨¬f)(\neg e\lor\neg f)(¬e∨¬f)知道fff为假，此时迹为a(a)⋅e(¬a∨e)⋅¬f(¬e∨¬f)a^{(a)}\cdot e^{(\neg a\lor e)}\cdot\neg f^{(\neg e\lor\neg f)}a(a)⋅e(¬a∨e)⋅¬f(¬e∨¬f)。而CNF中的最后一个子句是(¬a∨¬e∨f)(\neg a\lor\neg e\lor f)(¬a∨¬e∨f)，得不到满足，所以我们在决策层000发现了矛盾，这意味着该CNF是不可满足的。

CDCL还有很多优化策略，比如采用启发式决策（Decision Heuristics）、利用数据结构加速单位传播过程、在遇到困难时重启等，这里就不再赘述了。

下面给出一个CDCL的Python实现：

from sympy import Symbol
from sympy.logic.boolalg import Not
from typing import *
from copy import deepcopyLiteral = Union[Symbol, Not]class Clause: # 子句类def __init__(self, c: Set[Literal], i: int):self.clause = cself.index = i # 该子句是CNF的第几个子句self.value = None # 目前该子句的赋值def __repr__(self):return f'[Clause {self.clause} index={self.index} ' + \f'value={self.value}]'def __eq__(self, o):if hasattr(o, 'clause'):return self.clause == o.clauseelse:return Falseclass CDCLSolver: # 基于CDCL算法的合取范式可满足性问题求解器class Trail: # 迹类class DecisionLevel: # 按决策层分开class Node: # 节点类def __init__(self, lit: Union[Literal, None], dl: int,rs: Union[Clause, None]):self.literal = lit # 文字self.dl = dl # 决策层self.reason = rs # 赋值原因（None=决策）def __repr__(self):return f'<({self.dl}) {self.literal} {self.reason}>'def __eq__(self, o):return self.literal == o.literal and self.dl == o.dl \and self.reason == o.reasondef __hash__(self):return hash((self.literal, self.dl))def __init__(self, dl: int):self.dl = dlself.nodes = [] # List[Node]def __repr__(self):return str(self.nodes)def __init__(self):self.levels = [self.DecisionLevel(0)]def append_level(self, dl: int):self.levels.append(self.DecisionLevel(dl))def append_node_to_current_level(self,lit: Literal, rs: Union[Clause, None]):self.levels[-1].nodes.append(self.DecisionLevel.Node(lit, self.levels[-1].dl, rs))def __repr__(self):return str(self.levels)def __init__(self, l: List[Set[Literal]]):# CDCLSolver的构造函数self.cnf = []i = 0for clause in l:self.cnf.append(Clause(clause, i))i += 1self.trail = self.Trail() # 迹self.assignments = dict() # 当前赋值for clause in l:for literal in clause:if literal not in self.assignments and \~literal not in self.assignments:self.assignments[literal] = None# 所有变量赋值均为None，即未赋值def get_value(self, l: Literal) -> Union[bool, None]:# 获取文字l的赋值if l in self.assignments:return self.assignments[l]if ~l in self.assignments:r = self.assignments[~l]if r == None:return Noneelse:return not rdef set_value(self, l: Literal):# 设置文字l的赋值为True，或者设置~l的赋值为Falseif l in self.assignments:self.assignments[l] = Trueif ~l in self.assignments:self.assignments[~l] = Falsedef clear_value(self, l: Literal):# 让文字l回到未赋值的状态if l in self.assignments:self.assignments[l] = Noneif ~l in self.assignments:self.assignments[~l] = Nonedef find_unit_clause(self) -> \Union[Tuple[Literal, Clause], Tuple[None, None]]:# 寻找单位子句，返回对应的文字，找不到返回Nonefor clause in self.cnf:len_clause = len(clause.clause) # 子句文字个数num_undefined = 0 # 子句中未赋值的文字个数num_false = 0 # 子句中取值为假的文字个数undefined_literal = None # 未赋值的文字for literal in clause.clause:value = self.get_value(literal)if value == False:num_false += 1elif value == None:undefined_literal = literalnum_undefined += 1if num_undefined == 1 and num_false == len_clause - 1:return undefined_literal, clausereturn None, Nonedef update_clause_value(self): # 更新子句的值for clause in self.cnf:len_clause = len(clause.clause)num_true = 0 # 取真的文字的个数num_false = 0 # 取假的文字的个数for literal in clause.clause:r = self.get_value(literal)if r == True:num_true += 1elif r == False:num_false += 1if num_true >= 1: # 至少有一个文字取真clause.value = True # 则子句取真elif num_false == len_clause: # 所有文字取假（冲突）clause.value = False # 则子句取假else: # 还不能确定子句的取值（没有文字取真，但并不都取假）clause.value = None # 待定def propagate_literal(self, literal: Literal,clause: Union[Clause, None]):# 传播文字literal的赋值self.set_value(literal) # 设置literal的赋值为真self.update_clause_value() # 更新子句的值self.trail.append_node_to_current_level(literal, clause)# 在迹中添加节点def unit_propagation(self): # 单位传播# 动态维护变量赋值、子句赋值和迹literal = None # 用于单位传播的文字while True:literal, clause = self.find_unit_clause()if literal == None:break # 不能进行单位传播了self.propagate_literal(literal, clause)def detect_conflict(self) -> Union[Clause, None]: # 检查是否有冲突for clause in self.cnf:if clause.value == False: # 若发现取值为假的子句，返回该子句return clausereturn Nonedef find_unassigned_literal(self) -> Union[Literal, None]:# 找到一个未赋值的文字，找不到就返回Nonefor literal, value in self.assignments.items():if value == None: # 若某子句的取值为None，说明它未赋值return literalreturn Nonedef clause_learning(self, conflict_clause: Clause) -> \Tuple[Clause, int]: # 子句学习latest_level_nodes = self.trail.levels[-1].nodes# 最近一次决策层的节点can_be_UIP = dict()# 存储每个最近一层的节点是否可能是唯一蕴含点的字典for node in latest_level_nodes:can_be_UIP[node] = True # can_be_UIP先全部设置为True# 由于迹是蕴含图的拓扑序，如果某条最近一层节点之间的边跨过了某个节点，# 那么这个节点必然不是唯一蕴含点（有路径不经过该节点）# 下面按正向建图conflict_node = self.Trail.DecisionLevel.Node(None,self.trail.levels[-1].dl, conflict_clause) # 冲突节点all_nodes = latest_level_nodes + [conflict_node]# 所有最近一层的节点，包括冲突节点V = set() # 计算顶点集Vfor level in self.trail.levels:for node in level.nodes:V.add(node)V.add(conflict_node)adjacency_list = dict() # 最近一层的邻接表for node in all_nodes:adjacency_list[node] = []node_from_literal = dict() # 从文字到节点的字典for node in V:node_from_literal[node.literal] = nodeall_literals = set() # all_nodes对应的文字集合for node in all_nodes:all_literals.add(node.literal)for node in all_nodes: # 构造邻接表rs = node.reasonif rs != None:for from_literal in rs.clause:if from_literal != node.literal \and ~from_literal in all_literals:from_node = node_from_literal[~from_literal]adjacency_list[from_node].append(node)# 下面按边排除不可能是唯一蕴含点的节点i = iter(all_nodes)for node in latest_level_nodes:next(i)for to in adjacency_list[node]:j = deepcopy(i)while True:k = next(j)if k == to:breakcan_be_UIP[k] = FalseUIP = None # 唯一蕴含点for node in reversed(latest_level_nodes):# 寻找唯一蕴含点# 节点的拓扑序越靠后，说明以它作为唯一蕴含点，唯一蕴含冲突切割的A集合越大# 因此拓扑序最靠后的唯一蕴含点就是对应于第一个唯一蕴含冲突切割的唯一蕴含点if can_be_UIP[node]:UIP = nodebreakcan_reach_conflict_node = set() # 可到达冲突节点的节点Q = [conflict_node] # 利用广度优先搜索进行计算，Q是队列while len(Q) > 0:u = Q[0]can_reach_conflict_node.add(u)del Q[0]rs = u.reasonif rs != None:for literal in rs.clause:if literal != u.literal and \~literal in all_literals:node = node_from_literal[~literal]Q.append(node)successor_of_UIP = set() # 唯一蕴含点的所有后继Q = [UIP] # 仍然广度优先搜索进行计算while len(Q) > 0:u = Q[0]del Q[0]for node in adjacency_list[u]:successor_of_UIP.add(node)Q.append(node)B = can_reach_conflict_node.intersection(successor_of_UIP)# B包含是UIP的后继并且能到达冲突节点的节点，所以取两个集合的交集A = V - B # 冲突切割W=(A,B)，A∪B=VR = set() # 原因集entire_adjacency_list = dict() # 整个蕴含图的邻接表for node in V:entire_adjacency_list[node] = []for node in V: # 构造entire_adjacency_listrs = node.reasonif rs != None:for from_literal in rs.clause:if from_literal != node.literal:from_node = node_from_literal[~from_literal]entire_adjacency_list[from_node].append(node)for node in A: # 找出R中的元素for to in entire_adjacency_list[node]:if to in B:R.add(node)breaknew_clause = set()for node in R:new_clause.add(~node.literal)learned_clause = Clause(new_clause, len(self.cnf)) # 学到的子句self.cnf.append(learned_clause)R_levels = sorted(list(set([node.dl for node in R])))# R的元素的决策层集合backtrack_level = 0if len(R_levels) > 1:backtrack_level = R_levels[-2] # 第二大return learned_clause, backtrack_level# 返回学到的子句和应回溯到的决策层def backtrack(self, clause: Clause, level: int): # 回溯到第level层while self.trail.levels[-1].dl > level: # 考察在第level层之后的层for node in self.trail.levels[-1].nodes:self.clear_value(node.literal) # 文字重新退回到未赋值状态self.trail.levels.pop() # 从迹中删除该层self.update_clause_value() # 更新子句的值def CDCL(self) -> bool:decision_level = 0 # 一开始决策层是0while True:self.unit_propagation() # 单位传播conflict_clause = self.detect_conflict()if conflict_clause != None: # 发现冲突if decision_level == 0:return False # 在决策层0发现冲突说明不可满足else:learned_clause, backtrack_level = \self.clause_learning(conflict_clause) # 子句学习self.backtrack(learned_clause,backtrack_level) # 回溯decision_level = backtrack_levelelse:literal = self.find_unassigned_literal()if literal == None:# 所有变量均被赋值且未发生冲突，说明可满足return Trueelse:decision_level += 1 # 开始一个新的决策层self.trail.append_level(decision_level)self.propagate_literal(literal, None)

参考文献

Unit propagation - Wikipedia
Conflict-driven clause learning - Wikipedia
Conflict Driven Clause Learning (cse442-17f.github.io)
CDCL SAT Solvers & SAT-Based Problem Solving (aalto.fi)
Conflict-driven clause learning (CDCL) SAT solvers — CS-E3220: Propositional satisfiability and SAT solvers documentation (aalto.fi)

合取范式可满足性问题：CDCL（Conflict-Driven Clause Learning）算法详解相关推荐

PyTorch 迁移学习 (Transfer Learning) 代码详解
PyTorch 迁移学习代码详解概述为什么使用迁移学习更好的结果节省时间加载模型 ResNet152 冻层实现模型初始化获取需更新参数训练模型获取数据完整代码概述迁移学习 ( ...
联邦学习入门（二）-Practical Secure Aggregation for Privacy-Preserving Machine Learning论文算法详解
本文介绍了一种实用的安全聚合算法(Secure Aggregation Protocol),主要参考了Google的论文Practical Secure Aggregation for Privacy ...
PODNet: Pooled Outputs Distillation for Small-Tasks Incremental Learning论文详解ECCV2020
ECCV2020 论文地址:https://doi.org/10.1007/978-3-030-58565_6 代码地址:https://github.com/arthurdouillard/incr ...
Video Target Tracking Based on Online Learning—TLD单目标跟踪算法详解
视频目标跟踪问题分析视频跟踪技术的主要目的是从复杂多变的的背景环境中准确提取相关的目标特征,准确地识别出跟踪目标,并且对目标的位置和姿态等信息精确地定位,为后续目标物体行为分析提供足 ...
联邦学习（Federated Learning）详解以及示例代码
联邦学习也称为协同学习,它可以在产生数据的设备上进行大规模的训练,并且这些敏感数据保留在数据的所有者那里,本地收集.本地训练.在本地训练后,中央的训练协调器通过获取分布模型的更新获得每个节点的训练贡献 ...
Deep QLearning算法详解（强化学习 Reinforcement Learning）
一.算法详解文章最后附有博主自己实现的深度qlearning玩space invader游戏本文介绍的是基于神经网络的qlearning算法.我们知道传统的qlearning算法只能处理状态和动作 ...
Online Learning算法理论与实践
Online Learning是工业界比较常用的机器学习算法,在很多场景下都能有很好的效果.本文主要介绍Online Learning的基本原理和两种常用的Online Learning算法:FTRL ...
论文笔记：CLIP：Learning Transferable Visual Models From Natural Language Supervision详解
paper:https://arxiv.org/abs/2103.00020 代码:GitHub - openai/CLIP: Contrastive Language-Image Pretraini ...
Incremental Learning of Object Detectors without Catastrophic Forgetting详解
Incremental Learning of Object Detectors without Catastrophic Forgetting详解最近由于项目的需要在研究incremental l ...
Unsupervised Monocular Depth and Ego-motion Learning with Structure and Semantics 之论文详解
Unsupervised Monocular Depth and Ego-motion Learning with Structure and Semantics 1.论文详解 2.问题 1.如何理解 ...

合取范式可满足性问题：CDCL（Conflict-Driven Clause Learning）算法详解