RC2: an Efficient MaxSAT Solver
RC2：高效 MaxSAT 求解器
https://alexeyignatiev.github.io/assets/pdf/imms-jsat19-preprint.pdf
摘要
最近的工作提出了一个名为PySAT的工具包，旨在在Python中快速且轻松地使用命题可满足性（SAT）预言机原型设计，这使得人们能够在Python中利用最先进SAT求解器的原始实现。最大可满足性（MaxSAT）是SAT的一个众所周知的优化版本，可以通过一系列对SAT预言机的调用来解决。基于这一事实，并受到PySAT工具包背后思想的启发，本文描述并评估了RC2（代表可放松的基数约束），这是一个用Python编写的新的以核心引导的MaxSAT求解器，它在2018年MaxSAT评估的主要赛道中赢得了无权重和有权重两个类别的冠军。
关键词：最大可满足性，可放松/软基数约束，Python
1. 引言
最大可满足性（MaxSAT）代表了命题公式在合取范式（CNF）中的优化问题。MaxSAT问题可以如下一般性地表述。子句可以有关联的权重，子句可以是硬性的（对应于无限大的正权重）。目标是找到最大化满足子句成本的赋值。（假设硬性子句是可满足的；否则成本将是无限的。）MaxSAT在程序分析、故障定位以及一般基于模型的诊断等领域找到了日益广泛的应用。
本文描述了RC2，一个开源的MaxSAT求解器，用Python编写，并基于PySAT框架2。[11]。尽管是用Python原型设计的，RC2在2018年MaxSAT评估的两个完整类别中排名第一。本文不仅描述了支持RC2的设计决策，包括最初在[19]中提出的算法，还概述了实现细节，使得能够在PySAT框架之上实现一个高性能的MaxSAT求解器。
本文的组织如下。第2节介绍了整个论文中使用的必要定义和符号。第3节描述了RC2求解器的组织和实现以及所使用的启发式方法。第4节展示了评估RC2不同配置性能的实验结果。第5节讨论了RC2的可用性，随后是第6节中的结论。
2. 初步知识
本节介绍本文使用的符号和定义。标准的命题逻辑定义适用（例如[7]）。命题公式是在一组布尔变量上定义的。如果一个命题公式F被表示为子句的合取，也即作为子句的集合，那么它被称为合取范式（CNF）。子句是字面量的析取，也即作为字面量的集合。字面量是一个命题变量或其补集。在下文中，CNF公式将使用SAT预言机来处理。给定一个CNF公式F，一个SAT预言机决定F是否可满足，如果是，它返回一个满足赋值。给定一个不可满足的CNF公式F，一个SAT预言机也可以返回一个不可满足的核心U ⊆ F，这是F的一个子句子集，它本身是不可满足的。假设SAT预言机是一个冲突驱动的子句学习（CDCL）SAT求解器。CDCL SAT求解器在[7]中进行了总结。
在最大可满足性（MaxSAT）问题的背景下，通常考虑（加权）部分CNF公式。部分CNF公式中的子句被特征化为硬性的，意味着这些必须被满足，或软性的，意味着如果可能的话，这些应该被满足。每个软子句都可以关联一个整数权重，最大可满足性（MaxSAT）的目标是找到一个赋值给命题变量，使得硬子句被满足，并且满足的软子句的权重之和被最大化。在方便的时候，软子句将被表示为对（c, w），其中c是一个字面量的析取，w是它的权重。同样，在相同背景下的硬子句将被标记为权重>，即（c, >）。存在多种MaxSAT求解算法，包括迭代和核心引导算法[22, 4, 20]，以及基于隐式击中集枚举的算法[6]。
3. 求解器描述
本节描述了求解器的组织结构、使用的MaxSAT算法以及集成的启发式方法。此外，本节还指出了提交给2018年MaxSAT评估的两种配置之间的一些差异，即RC2-a和RC2-b。
与我们之前的MaxSAT求解器MSCG[21]不同，后者实现了大量MaxSAT算法[20]，例如包括基于进展的[10]和OLL[19]算法，RC2专门关注后者算法的一个变体，遵循[21]的实现。下面一节详细描述了该算法。RC2支持PySAT提供的多种SAT求解器，通过基于假设的Minisat-like[8]增量接口。默认情况下，RC2使用Glucose 3.0[5]作为底层的SAT预言机。
3.1 RC2 MaxSAT算法
RC2代表可放松的基数约束。本节描述了在RC2中实现的MaxSAT算法。最初，OLL算法是为解决ASP优化问题[1]而创建的。然后在2014年，该算法被改编用于解决MaxSAT问题[19]，但重复使用发现的基数约束。RC2改进了适应MaxSAT的OLL算法[19]，并在后续章节中解释了附加功能。在描述算法之前，我们将提供一个说明性示例。
在我们的示例中，我们将滥用符号，将约束称为字面量或子句。考虑F = S ∪ H是一个部分MaxSAT公式，其中软子句集合S = {(x1, 1),(x2, 1), (x3, 1), (x4, 1), (x5, 1)}，硬子句集合H = {(¬x1 ∨ ¬x2 ∨ ¬x3 ∨ ¬x4), (¬x1 ∨ ¬x2), (¬x3 ∨ ¬x4), (¬x1 ∨ ¬x5), (¬x2 ∨ ¬x5), (¬x3 ∨ ¬x5), (¬x4 ∨ ¬x5)}。
最初，F被发送到SAT求解器，该求解器报告F是不可满足的。假设返回的不可满足核心由软子句(x1, 1), (x2, 1), (x3, 1), (x4, 1)以及硬子句(¬x1 ∨ ¬x2 ∨ ¬x3 ∨ ¬x4)组成。为了修复核心，至少需要忽略核心中的一个软子句。类似于其他MaxSAT算法，算法通过在核心中放松每个软子句（即通过增加一个称为放松变量的新鲜变量）并限制放松变量的总和最多为一（通过添加基数约束）来继续进行。创建了新的放松变量r1、r2、r3、r4，并将核心中的软子句在F中替换为硬子句(x1 ∨ r1), (x2 ∨ r2), (x3 ∨ r3), (x4 ∨ r4)。该算法与其他已知MaxSAT算法的不同之处在于，它不是将放松变量变成新的软子句，而是使新的基数约束成为软约束。新的软约束((r1 + r2 + r3 + r4 ≤ 1), 1)被添加到F中，因此F更新为：
到目前为止，总的MaxSAT成本被设置为1。
此时，使用更新后的公式开始新的迭代，并将公式发送给SAT求解器。求解器报告该公式不可满足，并包含一个新的不可满足核心（除了硬子句之外），其中包含软约束((r1 + r2 + r3 + r4 ≤ 1), 1)。由于核心中没有原始的软子句（只有这个软约束），所以没有放松任何子句。软约束将其右手边（RHS）增加到2，即S更新为：
MaxSAT的成本更新为2。
第三次迭代将更新后的公式发送给SAT求解器，求解器再次得出公式不可满足的结论。这一次，不可满足的核心包含软子句(x5, 1)和软约束(r1 + r2 + r3 + r4 ≤ 2, 1)，以及一些硬子句。由于(x5, 1)是公式中的原始软子句，因此使用新变量r5来放松该子句。此时，算法移除了核心中涉及的软子句和软约束，并添加了两个新的软约束(r5 + ¬(r1 + r2 + r3 + r4 ≤ 2) ≤ 1, 1)和(r1 + r2 + r3 + r4 ≤ 3, 1)。添加的第一个软约束将放松变量与之前的软约束相关联。如果将r5设置为真并且之前的软约束被违反（即r1 + r2 + r3 + r4 ≥ 3），则该约束会被违反。第二个软约束增加了之前软约束的界限。总的来说，这两个添加的约束允许要么将r5设置为真（满足之前的软约束），要么让之前的放松变量中多一个可以设置为真。更新后的公式是：
MaxSAT的成本被设置为3。
最后，在算法的最后一次迭代中，新的公式被发送给SAT求解器，求解器报告该公式是可满足的，因此最终的MaxSAT成本被确定为3。
正如前一个例子所说明的，算法的思想是通过不可满足的迭代，直到获得一个可满足的公式。每当识别出一个新的不可满足的核心时，就更新公式，以便要么满足核心中的所有先前软约束，并且最多允许一个新放松变量被设置为真，或者允许其中一个软约束将其界限增加1。
该例子还说明了基数约束被用作软约束。在RC2中，软基数约束（∑m_i xi ≤ k, 1）被分为左手边（LHS）求和（∑m_i xi）和右手边（RHS）（≤ k）。LHS求和被编码为一组硬子句（使用迭代总计器编码[17]），使用辅助变量o1, ..., om表示一元数om ... o1。通过添加软单元子句（¬ok+1, 1）来强制执行RHS。
RC2 MaxSAT算法的伪代码在算法1中展示。该算法以部分MaxSAT公式F作为输入。最初（第5行），创建了一个字典映射，将字面量与软基数约束关联起来。对于给定的字面量l，map[l]返回一对（sumOutputs，rhs），其中sumOutputs是一个向量，编码软基数约束的左侧和（作为一元数），rhs是软基数约束的当前右侧。然后在第6行设置初始成本为0。算法的主要迭代发生在第7到27行。在第8行调用SAT求解器处理当前公式F。如果公式是可满足的，那么st被设置为true，算法终止，并在第10行返回最优值成本和满足赋值A（由SAT求解器报告）的一对。
如果公式是不可满足的，那么获得一个核心C，成本增加1（第12行），并创建一个新的集合L来保存要创建的新软基数约束的左侧和的输入变量（第13行）。算法通过检查核心中的每个软约束（第14行）继续进行。如果软约束是F的原始软子句，那么在子句中添加一个新的放松变量，将子句在F中变硬，并将放松变量添加到L中。这个过程是通过在第16行调用函数RelaxAndHarden(L, F, c)（在第1-4行中定义）来完成的。否则，约束是一个软基数约束，并且从F中移除（第18行）。将强制基数约束的相应单位字面量（s）添加到L中（第20行）。如果可能增加基数约束的右侧（第22行），那么使用相同的左侧和增加的右侧在F中强制执行一个新的软基数约束（第23和24行）。
当核心中的所有软约束都已处理完毕时，使用函数EncodeSum(L)对新软基数约束的左侧和进行编码，该函数返回包含表示总和的输出变量so4的一对，以及编码总和的硬子句集合sc（第25行）。将硬子句和强制新软基数约束的右侧（≤1）的软单位子句添加到F中（第26行）。将有关新软基数约束的信息添加到映射中（第27行）。
上述算法处理的是未加权的部分MaxSAT公式。在加权的情况下，RC2根据核心中软约束的最小权重拆分软约束（类似于其他MaxSAT算法）。每次找到一个新的核心时，计算核心中软约束的最小权重min。然后，每个权重大于最小权重的软约束（ci, wi）被替换为两个软约束：（ci, min）和（ci, wi − min）。在这里，RC2像处理部分情况一样处理包含权重min的软约束的核心，并且还通过min更新成本。
3.2 启发式方法
实现在求解器中的RC2 MaxSAT算法增加了一些额外的启发式方法，旨在提高其性能。所有集成的启发式方法都可以通过使用相应的命令行选项来启用或禁用。
3.2.1 SAT求解器接口
RC2利用标准的MiniSat类增量接口与SAT求解器交互，即通过指定一组假设字面量来多次调用求解器，这些假设字面量可能在每次求解器调用之间发生变化。这是通过以下方式完成的。给定一个不可满足的部分公式H ∧ S，求解器为每个软子句c ∈ S增加一个新鲜的选择器字面量¬s，即考虑一组修改后的软子句：S′ = {c ∨ ¬s | c ∈ S}。现在，通过将选择器字面量设置为真（或假），可以激活（或停用）相应的子句，并且这些偏好可以作为给求解器的假设列表指定。（此外，可以考虑使S′的子句变硬，并使用相应的选择器作为单位大小的软子句。）这样做的原因是，增量使用SAT求解器可以重用求解器，一旦它被创建。这使得求解器能够保留之前SAT调用中学到的所有子句。
3.2.2 处理加权公式
可以选择应用布尔字典序优化（BLO）[14]和分层[2]。这两种技术在处理加权公式时证明是有帮助的。BLO和分层被认为是处理涉及不可满足核心的软子句的MaxSAT算法的关键，例如在FM [9]及其改进[16, 15, 3, 12]中，以及OLL和RC2 [19]（也在上文中详细说明）。这两种启发式方法都旨在根据它们的权重对软子句施加偏好，并在问题解决时尽快向MaxSAT算法提供更多的软子句。
3.2.3 核心耗尽
RC2中使用的一个重要启发式方法是不可满足核心耗尽（最初称为覆盖优化）[2]。该启发式方法如下。回想一下，每个新识别的不可满足核心都会得到放松，并在核心中被证伪的子句数量上设定一个新的界限为1。假设每个不可满足核心C的子句都得到了放松，即转换为一组放松子句Cr和相应的放松变量集合R。注意，H ∧ Cr ∧ (∑r∈R r ≤ 1) 可能仍然是不可满足的。核心耗尽启发式的思想是迅速将界限从1增加到某个值k ≤ |R|，使得H ∧ Cr ∧ (∑r∈R r ≤ k) 仍然是不可满足的，而进一步增加k使公式变得可满足。这里的理论是，通过增量调用求解器对一系列略微修改的公式进行调用，只关注最近计算出的不可满足核心，而忽略公式的其余部分，可能在实践中是有效的。
3.2.4 内在的AtMost1约束
可以指示求解器检测公式中一些软子句的内在AtMost1约束，并在执行主要MaxSAT算法之前处理它们。这种启发式方法的工作原理如下。为了简单起见，考虑一组未加权的软子句（该技术可以很容易地扩展到加权软子句的情况）。假设有一个子集S′ ⊆ S，使得∑c∈S′ c ≤ 1成立，即在公式的硬子句存在的情况下，这些子句中至多有一个可以被满足。在这种情况下，可以立即得出结论，该公式的成本至少为|S′| - 1。此外，可以用一个单位权重的软子句∨c∈S′ c替换S′中的原始软子句。如果MaxSAT解决方案使这个新子句为假，S′中的所有原始软子句也将被证伪。回想一下，RC2中的每个公式的软子句都增加了一个新鲜的选择器字面量，即求解器处理的子句为c′ = c ∨ ¬s，对于每个原始软子句c ∈ S。在这里，c′被变硬，其选择器s被视为单位大小的软子句。因此，RC2中内在AtMost1约束启发式的实现是用它们的选择器的单个析取替换S′中的子句。
注意，可以检测到多个两两不相交的S的子集，每个子集都按照上述方式处理。每个这样的子集S′都有助于公式的总MaxSAT成本。请注意，此过程不涉及SAT求解器调用。可以通过将其中一个选择器（例如s1）设置为真，并应用单位传播，然后检查另一个选择器（例如s2）是否被暗示为假，来检查至多一个软子句（c1 ∨ ¬s1）和（c2 ∨ ¬s2）可以被满足。
3.3 MSE18版本
提交给2018年MaxSAT评估的两个求解器变体包括RC2a和RC2-b。两个版本都使用Glucose 3.0 [5]作为底层SAT引擎，应用BLO、分层、核心耗尽，并检测内在的AtMost1约束。求解器变体之间的唯一区别是不可满足核心缩减的策略。
3.3.1 核心缩减
与RC2-a不同，RC2-b应用基于简单删除的启发式不可满足核心最小化，使用最小不可满足子集（MUS）提取算法[13]。实现遵循算法2。这个想法是尝试逐个停用不可满足核心的软子句，同时检查剩余的软子句与公式的硬部分是否不可满足。对于保持不可满足性所必需的子句构成了输入公式的一个MUS（它包含在给定的不可满足核心中），并作为程序的结果报告。在RC2-b的核心最小化阶段，获得1000个冲突后，所有SAT调用都被丢弃。请注意，对于大型纯MaxSAT公式，即那些没有硬子句但有超过100000个软子句的公式，RC2-b中的核心最小化是禁用的。原因是，拥有这么多软子句（因此，有这么多假设字面量）且没有硬子句被认为会使SAT调用变得过于昂贵。
尽管在RC2-a中禁用了核心最小化，但由于RC2算法的性质，即由于应用于不可满足核心子句的基于权重的分割技术，减小不可满足核心的大小仍然对加权实例有帮助。因此，在处理加权实例时，RC2-a最多修剪不可满足核心5次（例如，有关不可满足核心修剪的详细信息，请参阅[21]），目的是摆脱不必要的子句。请注意，对于未加权的MaxSAT实例，RC2-a中禁用了不可满足核心修剪，而RC2-b则根本不使用它。
3.4 增量MaxSAT求解
除了上述描述的功能外，RC2还支持增量MaxSAT求解。这意味着人们不仅可以使用RC2计算与MaxSAT解决方案相对应的满足赋值，即与最优MaxSAT成本相对应的赋值，还可以迭代地枚举给定数量的赋值，或者无需重新启动求解器即可详尽地枚举所有赋值。请注意，枚举模式可以用来计算排序后的top-k MaxSAT解决方案，即首先计算成本最低的解决方案。RC2中的增量MaxSAT求解与RC2按需向工作公式添加硬子句和软子句的能力相关联，即在必要时（有关详细信息，请参阅RC2源代码中的add_clause()方法）。
4. 实验结果
本节致力于评估RC2的基本版本及其竞赛版本，即RC2-a和RC2-b。此外，它还评估了上述两种启发式方法在求解器整体性能中的贡献，即核心耗尽（见第3.2.3节）和内在的AtMost1约束（如第3.2.4节所述）。因此，在下文中，RC2表示求解器的基本版本（包括对加权公式使用BLO和分层），而RC2?在基本版本的基础上增加了不可满足核心耗尽，RC2??还额外执行了内在AtMost1约束的检测和适应。
为了进行比较，我们选择了2018年MaxSAT评估（MSE18）[18]中的所有（即未加权和加权）基准测试。基准测试套件包含600个未加权和600个加权MaxSAT实例。实验在Ubuntu Linux上进行，使用的是Intel Xeon E5-2630 2.60GHz处理器和64GByte的内存。每个单独运行的过程的时间限制设置为1800秒，内存限制设置为10GByte。为了比较的目的，我们为每种基准测试类别选择了在MSE18中表现最好的两个求解器（除了RC2-a和RC2-b）。这些包括Maxino和MaxHS用于未加权实例，以及MaxHS和Pacose用于加权实例。
图1和图2显示了展示所有选定竞争对手性能的仙人掌图。根据实验数据，可以得出以下结论。
首先，可以观察到，RC2-a和RC2-b被确认为性能最佳的MaxSAT求解器。它们分别解决了406个和414个未加权实例以及394个和403个加权基准测试。（请注意，解决实例的数量与评估中的数量不同，这可以通过使用不同的时间和内存限制以及不同的机器配置来解释。）此外，RC2的基本版本在两种情况下都排在最后，解决了350个未加权和314个加权实例。使用不可满足核心耗尽，即在图中看到的RC2?，在未加权和加权类别中分别增加了15个和22个解决的实例，因此，分别解决了365个未加权和336个加权公式。额外应用内在的AtMost1约束增加了更多的41个未加权和50个加权实例解决，即RC2??总共解决了406个未加权和386个加权实例。（请注意，RC2-a和RC2??在未加权类别中的表现相同，因为它们代表了求解器在未加权公式的相同配置，而在加权子句的情况下则不是这样。）此外，可以观察到，不可满足核心缩减在处理加权MaxSAT公式时似乎很重要（参见图2，RC2的竞争版本如何超越RC2??）。
图1和图2还描绘了两种配置的虚拟最佳求解器（VBS）的性能：VBSall和VBSsrc2。虽然后者VBSsrc2包括了RC2的所有配置，但前者VBSall整合了所有测试的求解器。请注意，VBSsrc2解决了422个未加权和418个加权基准测试。这比仅由获胜配置RC2-b解决的实例数量多出8个未加权和15个加权基准测试。因此，调整RC2中使用的启发式方法和参数可能会使求解器的整体性能更好。还请注意，VBSall解决了460个未加权和482个加权基准测试。这一结果包括了VBSall与表现最佳的独立求解器之间的令人印象深刻的性能差距，这表明在实际问题解决中使用顶级MaxSAT求解器组合可能是战略性的。
总之，所示的实验结果不仅证实了RC2-a和RC2-b在未加权和加权MaxSAT求解（由Maxino、MaxHS和Pacose代表）方面相对于现有技术的优势，而且还表明所提出的启发式方法对RC2的整体性能至关重要。这特别是对于内在AtMost1约束的检测而言。请注意，这种启发式方法可以应用于任何MaxSAT求解器，这可能会导致显著的性能提升。此外，我们对RC2的未来工作之一是研究该技术是否可以有效地推广到AtMostk约束的情况。
5. 可用性
RC2作为PySAT框架的一部分进行分发，可在https://pysathq.github.io. 下获得，它也以MIT许可证提供。它也可以作为Python包从PyPI安装：
RC2求解器可以作为独立的可执行文件rc2.py使用，也可以集成到复杂的基于Python的问题解决工具中，例如使用Python的标准导入接口：
6. 结论
本文描述了在2018年MaxSAT评估中两个完整类别中排名第一的RC2原型MaxSAT求解器的组织结构[18]。RC2基于PySAT框架，并且是公开可用的（见第5节）。未来的工作将寻求通过添加额外的MaxSAT算法来扩展RC2，目的是提供参考实现。
