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

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

1,2,3,4

1,2,3 1,2,4 1,3,4 2,3,4

1,2 1,3 1,4 2,3 2,4 3,4

1 2 3 4

ø
图 1 哈斯图

算法通过在哈斯图上执行相应的探索操作和剪枝操作来完成对 MUS 的枚举过程. 探索操作对当前种子节点
执行向上或向下探索, 使其扩充为一个 MSS 或者收缩为一个 MUS; 剪枝操作则是根据公理 1 在哈斯图上进行相
应的剪枝, 剪去哈斯图中 MSS 对应节点的全部子集所在节点、MUS 对应节点的全部超集所在节点, 从而缩小算
法的搜索空间. 下面给出两种探索操作 (收缩操作和扩充操作) 以及两种剪枝操作 (向上剪枝和向下剪枝操作) 的
定义.
定义 10. 收缩操作 (Shrink) [21] . 给定一个子句集 C 和当前不可满足的种子 seed , 对 ∀ 子句 l ∈ seed , 将所有满
l
足执行操作 seed = seed\{l} 后不改变 seed 不可满足性质的子句 从 seed 中删除, 从而将 seed 收缩成为一个 MUS
的过程称为对该种子的收缩操作. 对 seed 的收缩过程可以看作在哈斯图中从 seed 节点向下方路径探索的过程.
定义 11. 扩充操作 (Grow) [21] . 给定一个子句集 C 和当前可满足的种子 seed , 对 ∀ 子句 l ∈ C\seed , 将所有满
足执行操作 seed = seed ∪ {l} 后不改变 seed 可满足性质的子句 l 加入 seed 中, 从而将 seed 扩充成为一个 MSS 的
过程称为对该种子的扩充操作. 对 seed 的扩充过程可以看作在哈斯图中从 seed 节点向上方路径探索的过程.
定义 12. 向上剪枝操作 (BlockUp) [21] . 称对给定集合的全部超集从哈斯图上剪枝的操作为对该集合的向上剪
枝操作.
此操作是针对 MUS 的剪枝操作, 通过在 map 中加入以下子句实现. 对于一个 MUS U, 有:
∨
BlockUp(U) = ¬x i ,
i:C i ∈U
其中, C i 为 U 中的一个子句, x i 是 map 中代表子句 C i 的变量.
定义 13. 向下剪枝操作 (BlockDown) [21] . 称对给定集合的全部子集从哈斯图上剪枝的操作为对该集合的向下
剪枝操作.
此操作是针对 MSS 的剪枝操作, 通过在 map 中加入以下子句实现: 对于一个 MSS S, 有:
∨
BlockDown(S ) = x i ,
i:C i <S
其中, 将公式的完整子句集命名为 F, C i 为集合 F\S 中的一个子句, x i 是 map 中代表子句 C i 的变量.
2 MUS 求解算法回顾

本节将回顾 MARCO 算法, 包括传统版本和优化版本, 即极大化模型的 MARCO 算法, 以及 MARCO-MAM
算法.
2.1 MARCO 算法
MARCO 算法是近年来最受欢迎的 MUS 枚举算法之一, 其框架简单、枚举快速. MARCO 算法的伪代码如算
法 1 所示, 其基本流程是不断地重复以下 3 个步骤.
(1) 当哈斯图中存在未探索节点时, 取一个未探索节点 seed .