SAT Encoding and CDCL Algorithm听课笔记

CDCL：：归结式

如果x不出现在公式的别的地方，那么两者可以等价

CDCL：：watched literals

通过监测文字来判断当前子句是否是单元子句

先选择两个未赋值的文字作为监测文字，若其中的监测文字被赋值后则去寻找其他未被赋值的文字作为监测文字，若最后的两个监测文字重合，即只剩下一个未被赋值的文字，则为单元子句（unit clause）

CDCL：：clause learning

假设之前已经对c=0，f=0进行赋值，现在对a=0进行赋值

最后一个子句会出现冲突，这样我们可以得出一个新的学习子句

即a，c，f最少有一个为1，同时为0则会出现冲突

CDCL：：implication graph（蕴含图）

在第5层，表示x2赋值为0

蕴含图的箭头表示对方是通过单元子句传播得到的值，所以蕴含图是不断生长的

当出现冲突时（红箭头指向）

就需要学习经验，也就是需要生成学习子句，可以进行如下图的分离割，将决策与冲突分离开

三条边只要不成立就不会出现右侧的冲突，而三条边对应的点为x4与x21，则我们可以学习到x4=1与x21=0不能同时成立，即学习子句：非x4或者x21

学习子句不唯一，因为可以有不同的分离割，不同的分离割对应不同的学习子句

那到底应该在哪个地方进行割，引出概念独一蕴含点

蕴含图的数据结构

对每个变量要维护三个信息，变量的值；变量的层级，变量被哪个子句单元传播过来的

CDCL：：unique implication point（独一蕴含点）

UIP（独一蕴含点）：在部分蕴含图中决策点走到冲突点所有路径都要经过的点

First UIP:离冲突结点最近的UIP、

目标就是通过蕴含图找到冲突点的First UIP然后分离割，进行学习子句