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

蒋璐宇 等: 针对 MUS 求解问题的加强剪枝策略 1975

操作系统的主机. 我们将本文提出的加强剪枝策略 ABC 应用于 MARCO 算法和 MARCO-MAM 算法, 分别得到
MARCO-ABC 算法和 MARCO-MAM-ABC 算法并与原算法作对比. 使用的 MARCO (http://www.iwu.edu/∼mliffito/
marco/) 算法代码为文献 [22] 中的使用极大化模型版本, MARCO-MAM 算法、MARCO-ABC 算法和 MARCO-
MAM-ABC 算法均通过在 MARCO 算法的基础上增加相应语句实现 (MARCO-ABC 与 MARCO-MAM-ABC 代码
开放下载网址: https://github.com/jiangluyu1998/ABC-scheme-for-MUS). 算法所用的编程语言为 Python 3.7 版本,
并调用 C++语言编写的 MiniSAT 求解器 [33] 用于种子节点可满足性的判断. 我们采用标准测试用例 SAT11 中的
MUS 实例 [34] 对算法进行了测试, 并对每组实验设置了 3 种时间限制, 分别为 0.5 h、1 h 和 2 h.
表 1 所示为在相同条件下 MARCO 算法与应用本文提出的 ABC 策略的 MARCO-ABC 算法分别在 0.5 h、1 h
和 2 h 的时间限制下枚举 MUS 个数的比较, 表 2 所示为在相同条件下 MARCO-MAM 算法与应用本文提出的
ABC 策略的 MARCO-MAM-ABC 算法分别在 0.5 h、1 h 和 2 h 的时间限制下枚举 MUS 个数的比较. 各表中加粗
的结果表示其枚举个数更多 (对于结果相同的情况, 结果均不加粗), 各表中最后一行的#win 代表在其上方的所有
测试用例中, 算法得到的枚举个数超过对方的测试用例个数.

表 1 MARCO 算法和 MARCO-ABC 算法在不同时间限制下枚举 MUS 个数比较

MARCO MARCO-ABC
Instances
0.5 h 1 h 2 h 0.5 h 1 h 2 h
fdmus_b14_134 158 513 1 566 173 584 1 664
fdmus_b14_141 82 199 642 84 203 642
fdmus_b14_210 80 205 637 80 204 609
fdmus_b15_291 51 102 231 53 108 253
fdmus_b15_294 47 100 224 47 100 218
fdmus_b15_304 32 59 143 31 63 144
fdmus_b15_421 151 294 581 157 327 673
fdmus_b15_463 174 369 764 189 405 823
fdmus_b17_1037 338 338 338 500 1 085 2 356
fdmus_b17_1324 58 117 228 57 116 229
fdmus_b17_1456 195 386 766 186 374 750
fdmus_b17_420 158 318 738 161 327 673
fdmus_b20_141 16 32 67 18 36 71
fdmus_b20_171 20 38 74 21 38 74
fdmus_b20_238 44 93 222 45 92 236
fdmus_b20_341 188 629 1 562 176 639 1 623
fdmus_b20_349 33 66 141 33 63 149
fdmus_b20_381 29 66 162 31 67 158
fdmus_b20_492 38 88 352 40 86 322
fdmus_b20_498 61 179 552 65 200 518
fdmus_b21_111 14 27 55 14 29 60
fdmus_b21_112 14 26 53 15 27 53
fdmus_b21_167 35 70 153 34 70 148
fdmus_b21_481 31 64 224 31 65 175
fdmus_b21_96 115 300 715 118 311 738
fdmus_b22_102 34 63 136 36 70 133
fdmus_b22_113 12 23 45 12 25 49
fdmus_b22_133 46 100 226 54 108 229
fdmus_b22_172 21 42 88 23 42 86
fdmus_b22_241 29 60 145 30 60 142
fdmus_b22_356 14 28 63 14 27 62
fdmus_b22_488 51 110 428 51 122 476
fdmus_b22_600 15 26 62 20 29 69