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

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

19. MUS ← Shrink(midseed)
20. output MUS
21. map ← map ∧ BlockUp(midseed)
22. end if
23. end if
24. end if
25. end while

3 利用关键 MSS 的加强剪枝策略

本文提出一种加强对哈斯图的剪枝策略, 并提出关键 MSS 的概念. 根据 MUS、MCS 和 MSS 之间的关系, 我
们可以通过关键 MSS 进一步对哈斯图进行剪枝操作. 本节首先给出所提出剪枝策略的理论依据, 之后介绍将其结
合到 MARCO 算法和 MARCO-MAM 算法中的整体算法流程.
3.1 算法的理论基础
现有的 MARCO 算法和 MARCO-MAM 算法的剪枝过程均通过已找到的 MUS 和 MSS 来完成的, 在哈斯图
中裁剪掉 MUS 的全部超集、MSS 的全部子集, 从而缩减了算法的搜索空间. 然而, 当求解的 MSS 具有某些特定
的结构特征时, 可以利用这些 MSS 对搜索空间进行进一步的剪枝操作. 在下述定义 14 中, 我们给出了这种满足
“具有特定的结构特征的 MSS”的定义.
定义 14. 关键极大可满足子集 (critical MSS, cMSS). 给定一个子句集 C, 称一个极大可满足子集 M 是 C 下的
|M| = |C|−1 , 即, C 中只有一个子句不在 M 中.
一个关键极大可满足子集当且仅当集合的基数满足
定义 15. 子极小不可满足子集 (subMUS). 称所有关键极大可满足子集的补集中唯一的子句组成的集合为子
极小不可满足子集.
在给出关键 MSS 和 subMUS 的定义后, 我们对本文所提出的加强剪枝策略 ABC 表述如下.
算法每求出一个关键 MSS 时, 更新 subMUS 并判断其可满足性: 若可满足, 则对代表集合 subMUS 的节点做
BlockDown 操作; 否则, 输出 subMUS 为 MUS, 算法结束.
性质 1. 集合 subMUS 一定包含在每一个 MUS 中.
证明: 假设给定的子句集 C 中有 n 个 cMSS, 每个 cMSS 记为 cMSS i (1 ⩽ i ⩽ n) cMSS i 中缺少的子句记为 c i ,
,
则 subMUS = {c 1 ,...,c n } . 根据每个 MSS 的补集都是一个 MCS, 则有每个 cMSS i 对应的 MCS i = {c i } , 又根据 MUS
和 MCS 互为极小碰集的性质可知, 每个 MUS 中必然包含 c 1 ,...,c n . 因此集合 subMUS 必然是每个 MUS 的子集,
它一定包含在每一个 MUS 中.
性质 2. 使用 MARCO 类算法框架每搜索到一个关键 MSS, 剪枝后哈斯图中的剩余节点一定是代表 subMUS
的超集的节点.
证明: 哈斯图中的节点除代表 subMUS 和其超集的节点外, 剩余节点或者是代表 subMUS 真子集的节点, 或
者是与 subMUS 之间无包含关系的集合的节点. 采用反证法证明.
首先, 假设剩余节点中存在代表 subMUS 真子集中的节点. (1) 该节点代表空集: 由于空集是任何一个关键
MSS 的子集, 因此算法在找到第 1 个关键 MSS 时, 就已经通过 BlockDown 操作将代表空集的节点剪枝, 故剩余
节点中一定没有代表空集的节点. (2) 该节点代表 subMUS 的一个非空真子集: 令该非空真子集为 Q, 则 Q 中至

少存在一个元素 e , 使得 e ∈ subMUS 且 e < Q. 由 e ∈ subMUS 可知, 已求解出的关键 MSS 必有一个为集合 P=
{i|i ∈ 子句集C且i , e} , 即从子句集 C 中去除一个元素 e 的集合. 由于集合 Q 中没有元素 e , 而集合 P 是所有没有
e 的集合中基数最大的集合, 故必有 Q 是 P 的子集, 而集合 P 又是一个关键 MSS, 求解出该关键 MSS 时通
元素
过 BlockDown 操作已经将其全部子集所在节点剪枝, 因此不存在这样的集合 Q, 故假设不成立, 剩余节点中没有代