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

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2024,35(4):1964−1979 [doi: 10.13328/j.cnki.jos.006845] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
针对 MUS 求解问题的加强剪枝策略

蒋璐宇 1,3 , 欧阳丹彤 1,3 , 董博文 2,3 , 张立明 1,3

1
(吉林大学 计算机科学与技术学院, 吉林 长春 130012)
2
(吉林大学 软件学院, 吉林 长春 130012)
(符号计算与知识工程教育部重点实验室 (吉林大学), 吉林 长春 130012)
3
通信作者: 张立明, E-mail: limingzhang@jlu.edu.cn

摘 要: 极小不可满足子集 (minimal unsatisfiable subsets, MUS) 的求解是布尔可满足性问题中的一个重要子问题.
对于一个给定的不可满足问题, 其 MUS 的求解能够反映出问题中导致其不可满足的关键原因. 然而, MUS 的求解
是一项极其耗时的任务, 不同的剪枝过程将直接影响到搜索空间的大小、算法的迭代次数, 从而影响算法的求解
效率. 提出一种针对 MUS 求解的加强剪枝策略 ABC (accelerating by critical MSS), 依据 MSS、MCS、MUS 这 3
者之间的对偶性和碰集关系特点, 提出 cMSS 和 subMUS 概念, 并总结出 4 条性质, 即每个 MUS 必是 subMUS 的
超集, 进而在避免对 MCS 的碰集进行求解的情况下有效利用 MUS 和 MCS 互为碰集的特征, 有效避免求解碰集
时的时间开销. 当 subMUS 不可满足时, 则 subMUS 是唯一的 MUS, 算法将提前结束执行; 当 subMUS 可满足时,
则剪枝掉此节点, 进而有效避免对求解空间中的冗余空间进行搜索. 同时, 通过理论证明 ABC 策略的有效性, 并将
其应用于目前最高效的单一化模型算法 MARCO 和双模型算法 MARCO-MAM, 在标准测试用例下的实验结果表
明, 该策略可以有效地对搜索空间进行进一步剪枝, 从而提高 MUS 的枚举效率.
关键词: 极小不可满足子集; 极大可满足子集; MUS 枚举; 幂集探索; 不可行分析
中图法分类号: TP18

中文引用格式: 蒋璐宇, 欧阳丹彤, 董博文, 张立明. 针对MUS求解问题的加强剪枝策略. 软件学报, 2024, 35(4): 1964–1979. http://
www.jos.org.cn/1000-9825/6845.htm
英文引用格式: Jiang LY, Ouyang DT, Dong BW, Zhang LM. Enhanced Pruning Scheme for Enumerating MUS. Ruan Jian Xue
Bao/Journal of Software, 2024, 35(4): 1964–1979 (in Chinese). http://www.jos.org.cn/1000-9825/6845.htm

Enhanced Pruning Scheme for Enumerating MUS
1,3
1,3
2,3
JIANG Lu-Yu , OUYANG Dan-Tong , DONG Bo-Wen , ZHANG Li-Ming 1,3
1
(College of Computer Science and Technology, Jilin University, Changchun 130012, China)
2
(College of Software, Jilin University, Changchun 130012, China)
3
(Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education (Jilin University), Changchun 130012,
China)
Abstract: Enumerating minimal unsatisfiable subsets (MUS) is an important subproblem in the Boolean satisfiability problem. For an
unsatisfiable problem, the MUS enumeration can reflect the key factors resulting in its unsatisfiability. However, enumerating MUS is
extremely time-consuming, and different pruning schemes will directly affect the size of the search space and the total number of
iterations, thus affecting the algorithm efficiency. This study proposes a novel enhanced pruning scheme, accelerating by critical MSS
(ABC), to accelerate the MUS enumeration. According to the relationship among maximal satisfiable subsets (MSS), minimal correction
sets (MCS), and MUS, the concepts of cMSS and subMUS are put forward. Additionally, four properties are summarized, namely that

* 基金项目: 国家自然科学基金 (62076108, 61872159, 61972360)
收稿时间: 2022-06-15; 修改时间: 2022-11-06; 采用时间: 2022-11-23; jos 在线出版时间: 2023-07-28
CNKI 网络首发时间: 2023-07-31