Page 388 - 《软件学报》2024年第4期

1966 软件学报 2024 年第 35 卷第 4 期

即代表给定公式的子句集的某一个子集的节点, 根据其可满足性必能得到一个 MUS 或 MCS, 若得到的是 MCS
则利用碰集的对偶性求解出 MUS, 因此该算法不必等到全部 MCS 求出后再开始枚举 MUS. 在这类算法中, 由于
极小碰集的求解复杂度高且算法要多次调用碰集求解过程, 因此这类算法普遍存在耗时较大的问题.
基于种子缩减的算法则是利用收缩操作遍历当前种子节点的子集, 在找到其对应的 MUS 后, 对其超集进行
剪枝, 从而避免了对无解空间的探索, 这类方法的代表算法有 MARCO [21−23] 、MARCO-MAM [24,25] 、TOME [26] 、
ReMUS [27] 等. 2013 年, Liffiton 等人 [21] 提出结合哈斯图枚举 MUS/MSS 的 MARCO 方法, 对于在哈斯图中任意一
个未探索的种子节点, 根据其可满足性做相应的扩充 (或收缩) 操作, 从而得到一个 MSS (或 MUS). 2016 年,
Liffiton 等人 [22] 针对尽可能减少对扩充和收缩操作的调用次数、让算法更倾向于优先找到不可满足的种子等目
标, 将 eMUS 中极大化模型的概念引入用于优化 MARCO 算法, 省去了对可满足种子节点的扩充过程. 同年, Zhao
等人 [23] 提出了极大化 MARCO 算法的多种子并行求解方法, 通过并行计算加速了算法枚举效率. 2019 年, 欧阳丹
彤等人 [24] 提出了基于双模型的 MARCO-MAM 算法, 在极大化模型的 MARCO 算法基础上增加了中间模型, 用于
加速 MUS 或 MSS 的枚举. 文献 [22] 中指出, 在这类算法中扩充和收缩操作一共平均占据总运行时间的约 80%.
因此, 扩充和收缩操作是基于种子缩减算法的主要耗时操作. 要想减少对扩充和收缩操作的调用, 就需要对搜索空
间进行更充分的剪枝. 通过剪枝更多节点来减少算法所需的迭代次数, 从而达到减少对扩充和收缩操作调用次数
的目的.
这两类算法从不同的角度出发来枚举 MUS, 它们的利弊也各不相同. 在上述第 1 类方法中, 碰集的求解是算
法中的主要耗时操作; 而在第 2 类方法中, 由于调用一次收缩 (或扩充) 操作将涉及对其子集 (或超集) 的可满足性
逐个判断直到得到一个 MUS (或 MSS), 因此调用收缩和扩充操作的过程则是算法中最为耗时的部分. 本文在对上
述求解 MUS 算法的深入分析基础上, 意图设计出一种将上述两类算法的优势结合起来的策略来加强对搜索空间
剪枝. 借助第 1 类方法中使用 MUS、MCS 及 MSS 三者之间的关系来枚举 MUS 的思想, 对使用第 2 类方法的基
本框架的算法制定剪枝方案, 从而使应用该剪枝策略后的算法拥有了这两类方法各自的优势. 考虑到部分具有特
殊结构特征的 MSS 可以帮助算法对搜索空间进行剪枝, 提出关键 MSS 的概念, 利用关键 MSS 的特殊性质对搜索
空间中的无解空间进行剪枝, 从而提高枚举的效率.
通过上述分析, 我们将本文提出的加强剪枝策略 ABC (accelerating by critical MSS) 的优势总结为以下
3 点: 首先, 当算法求解出关键 MSS 时, 通过 MSS、MCS、MUS 这 3 者之间的相互关系和碰集的特点, 可以
直接构造出一个子句集, 使得该集合中的每一个元素都一定包含在该问题的 MUS 中. 这样保证了整个算法
中没有碰集求解过程的情况下, 利用碰集自身的性质和 3 种集合间的关系而获得了碰集求解的效果, 避免计
算碰集的大范围时间开销. 其次, 极大化模型使得算法前期在哈斯图的顶部区域搜索, 而关键 MSS 自身特点
使得其在哈斯图中的位置一定处于顶部区域. 因此, 本文提出的策略与使用极大化模型的算法框架结合起来
将可以保证在算法执行的前期就可以找到尽可能多的关键 MSS, 从而保证其构造出的 MUS 子集尽可能大,
对无解空间的剪枝也随之更加充分. 最后, 本文通过证明得出结论: 当关键 MSS 构造出的子句集不可满足时,
那么它是该问题唯一的 MUS. 因此, 若构造出的子句集判断为不可满足时, 使用本文提出的 ABC 策略可以使
算法提前结束执行.
本文第 1 节介绍本文所需的基础知识, 包括 SAT 问题中的相关概念, MUS、MSS 和 MCS 的概念及 3 者之间
的关系, 哈斯图结构及相关操作. 第 2 节介绍 MARCO 算法和 MARCO-MAM 算法. 第 3 节介绍本文提出的加强
剪枝策略 ABC, 并总结出 4 个性质从理论上证明了策略的正确和有效性. 第 4 节将所提出的方法应用于已有的

MARCO 算法和 MARCO-MAM 算法中, 通过对比实验验证了所提模型的有效性. 最后总结全文.
1 基础知识

本节主要介绍本文所涉及的基本概念, 首先介绍 SAT 问题中的定义, 然后介绍 MUS、MSS 及 MCS 的基本
概念及相关性质, 最后介绍哈斯图及对哈斯图的探索操作和剪枝操作.