Extended Conjunctive Normal Form and An Efficient Algorithm for Cardinality Constraints#

问题定义与记号#

SAT 问题的定义如下：

给定一个变量集合 ，和一个 CNF 范式 ， 问是否存在一组赋值 使得此

我们可以将 SAT 问题拓展为一个优化版本：如果我们对子句进行分类，必须满足的子句称为硬子句，可以被不满足的子句称为软子句，我们的优化目标是让不满足的软子句最少，这个问题被称为 Partial MaxSAT，当所有子句都是软子句时，这个问题被称为 MaxSAT

进一步的，如果我们对子句进行加权，我们的优化目标是使得未满足的子句的权值和最小，那么这个问题被称为 Weighed Partial MaxSAT

这里我们研究的只是 PMS 问题（拓展到基数约束版本）

基数约束#

关于基数约束的定义可以参考 这篇文章，简而言之，基数约束可以写为如下形式：

\sum^{r}_{i=1}l_i \triangleright k\quad  \, \triangleright \in \{\geq, \leq, =\}, k \in \mathbb{N^+_0}

值得注意的是，所有的基数约束都可以写为至少的形式，例如至多有 个为真可以写为至少有 个为假：

\sum^{r}_{i=1}l_i \leq k \leftrightarrow \sum^{r}_{i=1}\neg l_i \geq r-k

因此，我们在后面只考虑 “子句中至少有 个变量为真” 这一形式的基数约束

对于每条软基数约束 ，我们都考虑其有一个惩罚值 了，在这里，我们将硬子句也编码为基数约束的形式 ：

我们需要求解的问题就是，在所有子句形式都是基数约束的条件下（区分软硬子句），求 当所有硬子句都满足时，不满足的软子句惩罚值最小 的一个赋值

LS-ECNF#

这里，我们引入两种技术来构建搜索框架：

1. 子句加权
2. 打分函数

子句加权#

本文的子句加权技术称为 Weighting-EPMS，我们假定对每个子句，都存在一个权重 ，注意这个权重不是实例中给定的，是算法引入的，在最开始时，硬子句的 ，软子句的 （这里的 ，可以考虑成一个可调的参数）

当搜索卡在局部最优时，也就是我们无法通过翻转变量获得更好的解时，此时，子句的权值会更新如下：

1. 以 的概率，对每个不满足的硬子句 ，，对每个不满足的软子句 ，只有当 时， ，在本文中，
2. 以 的概率，对每个满足的子句 ，

打分函数#

我们首先需要定义对于一个未满足子句 （软硬子句均如此定义），其带来的惩罚值是多少，我们可以根据优化目标进行重写：

penalty(c) = w(c) \times (r - \sum^{r}_{i=1}l_i)

这样，对于一个变量 ，我们对其的打分 定义为：翻转变量 后，目标函数（未满足子句的惩罚值）的下降值

整体框架#

整体框架如下图所示：

首先，我们通过 #广义单元传播算法 初始化一个赋值，然后开始迭代搜索

每次迭代时，我们选择一个 的变量做翻转，如果能够得到一个可行解（且比到目前位置的最优解更好），我们就做一次替换，否则继续搜索

而如果我们无法找到任何一个能带来正收益的变量，说明此时我们已经达到了局部最优，于是，我们对通过 #子句加权 来调整子句的权重，进而调整搜索的方向，接着，我们会优先选择硬子句来满足，以优先得到可行解

广义单元传播算法#

首先，我们定义广义单元子句（Generalized Unit Clause）：对于子句 ，如果其基数约束 大于等于此子句中含有的文字数，我们将其称为一个广义单元子句

于是，广义单元传播算法的流程如下图所示：

本质上我们对赋值做了优先级划分：

1. 硬的广义单元子句
2. 软的广义单元子句
3. 其他

实验#

选取的 Benchmark 为 Nurse Rostering 与 Tomography Problem，都是 OR 中的经典问题，可以在 OR 的 Benchmark 中找到

选取的对比算法为：

1. SATLike
2. Loandra
3. TT-Open-WBO-inc
4. CADICAL
5. Gurobi

采用的 SAT 编码方式为

1. Sequential encoding
2. Cardinality networks encoding
3. Pigeon-hole encoding

效果如下图所示：

护士排班问题：

离散数字成像问题：

ECNF 与 CNF 和 PB 的联系#

ECNF 通过引入基数约束的概念对 CNF 进行了扩展，在没有任何辅助变量和子句的情况下，可以将基数约束编码到 ECNF 中，ECNF 可视为 PBO 的特例，这在 PBO 问题简介 中有提及