Divide and Conquer: Towards Faster Pseudo-Boolean Solving#

简介#

SAT 的局限性›

CDCL 的推理（reasoning）能力差，因为其推理能力主要基于归结证明；以及其表达能力有限，只能解决以 CNF 形式表达的问题（虽然都可以规约，但会引入很多子句和变量），虽然有很多预处理技术（高斯消元，基数推理）可以提高很多速度，但这都与编码方式有很大关系，有时候并不是很有效果

由于 SAT 具有很大的局限性，于是，我们转向使用线性伪布尔约束来描述问题，这种约束形式能够表达比 CNF 更多的信息，但结构又与 CNF 很相似，于是基于 CNF 的技术可以应用到 PB 上

一些 PB 求解器仍然是基于归结的，这些求解器会将输入转化为 CNF，再进行求解；主要有两类做法：

1. eagerly：先转化为 CNF，然后直接调用 CDCL 求解器求解，代表是 MiniSat+，Open-WBO，NaPS
2. lazily：在修改的 CDCL 求解器中，保持输入的 PB 格式，但仅以子句的形式导出新的信息，代表为 Sat4j

另一种做法是使用切平面法来解决 PB 问题，但这种做法需要将 CDCL 框架拓展到 PB 上，这是十分困难的。

从理论的观点来看，使用切割平面似乎是很可取的，因为这种方法从来不比归结差，甚至可以做到指数级的更强。然而，实际上并非如此，通常基于 CDCL 的求解器优于基于切平面法的 PB 求解器。

在这篇文章中，提出了一个基于 CDCL 的 PB 求解器 RoundingSAT

基于冲突分析的 PB 求解#

首先，我们回顾 PB 约束的标准形式：

\sum_i c_i \cdot l_i \geq w

其中，, ，而 ，将 称为满足度（或者简称为度）

我们将部分真值赋值 看作由 设定为真的文字集合，也就是说如果 ，那么

一个传统的 CDCL 框架如下图所示：

在这里，我们不详细解释 CDCL 是如何工作的，我们希望做的是将 CDCL 中的两个重要部件引入到 PB 中来（重启与子句库之类的技术不在本文的探讨范围内）

单元传播#

在 SAT 中，对于任意一条子句，只要有一个文字为真，子句即可为真，因此我们可以很轻松的进行单元传播，而在 PB 中，这种简单的成真条件不存在了，于是我们需要重新考虑传播的方案

首先，我们引入一个记号，对于任意一条约束 ：

slack(C, \rho) = \sum_{i\colon \rho(l_i) \not= 0}c_i - w

可以发现 本质上表示，在给定赋值 的条件下，还差多少就能够满足约束 （本质上度量了一种满足的 progress)

显然当 时，约束是不满足的，我们定义传播如下：

如果文字 未被赋值，且有 ，那么我们称 蕴含/传播了文字 ，也就是说除非将 赋值为真，否则约束 不成立

冲突分析#

分析的方法是使用广义归结来进行，其定义如下：

给定一对存在冲突的约束 与约束 ，其在文字 的赋值上有冲突，我们假定 ，那么广义归结 定义为：

\frac{b}{g}\sum_ic_i\cdot l_i + \frac{a}{g}\sum_i c_i^\prime \cdot l_i^\prime \geq \frac{bw + aw^\prime -ab}{g}

随后，我们反复回退决策层，试图找到最早的那次冲突决策点，从而得到学习子句（这也是 CDCL 中 1UIP 的做法）

存在的问题#

我们考虑以下例子，，，假定，我们的决策序为 ，此时 trail 中的文字为

随后，在单元传播时，我们会在 中考虑传播 ，trail 变为 ，但此时 发生冲突，我们需要进行冲突分析，根据前文，我们得到 ，然而这个约束直接将 trail 中 的赋值全违反了，此时我们得到的学习子句（学习约束？）就没有任何意义了

弱化与饱和#

我们通过两个算子， 与 来解决这个问题

弱化#

从约束中删除一个文字，并从度中减去它的系数

例如对于约束 ，我们考虑对 做弱化操作

可以发现，弱化操作就是直接将某个文字的取值假定为真

饱和#

将约束中所有系数的大小降低到刚好不满足约束的程度，形式化的写为

例如对于约束 ，

最终的冲突分析#

于是，最终的冲突分析如下所示：

一个简单的分析示例›

考虑两个约束 ，我们可以发现，这两条约束本质上是两条基数约束：，这两条基数约束显然是矛盾的，不过算法没办法立刻发现这个问题

假设此时的 trail 为 ，此时，我们发现 不满足，于是我们进行冲突分析（其中，冲突约束为 ，原因约束为 ）

1. 对于 trail 中的最后一个文字，我们有 ，其 ，于是我们进行归结
2. 我们在原因约束中选择一个不同于 的不导致冲突的文字，例如 ，接着我们做弱化与饱和操作，得到新的原因约束：，其中饱和操作没有任何影响，因为 为真
3. 接着，我们得到新一轮的归结 ，此归结的 ，于是我们继续进行归结
4. 下一个被选择的文字为 ，我们得到新的原因约束为 ，此时归结的 ，其 ，于是继续归结
5. 下一个被选择的为 ，得到新的原因约束为 ，于是归结为 ，此时的 ，结束循环

最终，我们得到的

值得注意的是，我们并没有真正的计算 的值，我们通过使用上界来近似计算，以获得更好的效率：

slack(C + C^\prime, \rho) \leq slack(C, \rho) + slack(C^\prime, \rho)

基于 Division 的冲突分析#

我们将饱和算子替换为分割算子，其工作原理如下所示：

divide(C, d) \colon \sum_i \lceil c_i/d \rceil\cdot l_i \geq \lceil w/d \rceil

其中

RoundToOne#

首先外面介绍一个组件算法，RoundToOne，其流程如下图所示：

其接受一条约束 ，一个文字 以及当前的 trail 为参数，输出一条约束 ，这条约束是将 在 上的舍入（这里称为 rounding），且 的系数为 ，约束 还有一个额外的性质：

对于任意 trail 和任意 PB 约束 ，对于文字 我们有如下性质成立：

slack(\text{roundingToOne}(C, l_i, \rho), \rho) = \lfloor slack(C, \rho)/c_i \rfloor

于是，我们有推论：

若一条约束 是一条未违背的约束，且其在赋值为 的条件下传播了文字 ，即 ，那么我们有 ，否则，如果 ，那么

RoundToOne 的示例›

考虑两个约束 ，假设此时的 trail 为 ，此时，我们发现 不满足，于是我们进行冲突分析（其中，冲突约束为 ，原因约束为 ）

1. 我们求得 的系数为 ，随后开始迭代
2. 由于 均不是成假的，因此我们进入第二步判断，而由于只有 的系数无法整除 ，于是， 被弱化，我们得到了约束 ，此时循环结束
3. 最后，我们通过分割算子得到了以下约束：

此时，我们得到了一个比原来的方案更强的约束（原来的约束为 ）

RoundToOne 的变形›

考虑 ，此时我们在 的情况下对 做舍入，我们将会得到约束

但如果我们不在一次执行让所有满足条件的文字弱化，而是让算法每次在某一个文字上弱化，并且在分割后的 时终止，那么我们就可以得到更强的约束

然而，可以证明，无论进行弱化的顺序如何，这种迭代方法总是会弱化几乎和 roundToOne 一样多的文字；更准确地说，区别至多是 个文字，其中 是除数

另一种变形是在文字上做部分弱化，例如，从 中导出 ，随后，分割得到

RoundingSAT 冲突分析#

我们的冲突分析算法如下所示：

PB 冲突分析中存在一些特殊情况，使其比 CDCL 更加复杂

1. 一个归结操作可能会取消当前决策层的所有赋假文字，在这种情况下，分析可能会继续到更早的决策层，甚至可能发生冲突分析能够进行到最高决策层，从而推导出实例是不可满足的

2. 学习到的约束可能在其断言（激活）级别¹被违反，在这种情况下，在调用单元传播之前会重复执行冲突分析。

实验#

这部分，对比了算法：

1. Sat4j
2. Open-WBO
3. Sat4jRes+CP（使用了切平面法的 Sat4j）

Benchmark 为 PB 竞赛的例子，分类为 DEC-SMALLINT-LIN

结果如下图所示：

未来工作#

一个明显方向是进一步改进我们的求解器。与其他伪布尔求解器一样，RoundingSat 对输入格式很敏感，在 CNF 公式上表现很差。

解决这一问题的一种方法是在可能的情况下将 CNF 重写为更有效的线性约束的规则；特别地，一个重要的挑战是对编码基数约束的子句集合进行 该内容未公开或不可用

脚注#

1. 断言级别（Assertion Level）  是冲突驱动子句学习（CDCL）SAT 求解器中的一个重要概念，用于描述在搜索过程中某个约束（或子句）被“断言”或“激活”的决策级别。它表示在搜索树的某个特定层次上，某个约束开始对当前的变量赋值产生影响。 ↩