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

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

3. seed ← GetUnexploredMax(map)
4. if seed is SAT then
5. MSS ← seed
6. output MSS
7. map ← map ∧ BlockDown(seed)
8. else
9. MUS ← Shrink(seed)
10. output MUS
11. map ← map ∧ BlockUp(seed)
12. end if
13. end while

2.2 MARCO-MAM 算法
MARCO-MAM 算法是在极大化模型的 MARCO 版本上的进一步改进, 使用极大化模型和中间模型共同求
解, 算法的伪代码描述在算法 3 中. 与极大化模型 MARCO 不同的是, 当目前选取的种子节点 seed 不可满足时, 算
法将通过调用 GetUnexploredMid 函数引入一个中间种子 midseed 辅助求解. 该中间种子所代表的集合是 seed 所

代表集合的子集, 且其基数是 seed 所代表集合的一半, 该中间种子节点即在哈斯图中从节点 seed 处向下路径为其
seed 相同的操作: 先判断其可满足性, 若可满足则将它扩充
层数的一半的某个子集表示的节点. 再对 midseed 做与
为一个 MSS, 否则将其收缩为一个 MUS. 相比之下, 极大化模型更倾向于从哈斯图顶部开始逐步向下搜索, 而极
大化—中间模型则更倾向于在哈斯图的顶部—中部—顶部—中部…这样往复地向上、下搜索.
算法 3. MARCO-MAM.
输入: 不可满足的子句集 C;
输出: 已找到的子句集 C 的 MUS 集合和 MSS 集合.

1. map ← BooleanFormula(nvars=|C|)
2. while map 是可满足的 do
3. seed ← GetUnexploredMax(map)
4. if seed 是可满足的 then
5. MSS ← seed
6. output MSS
7. map ← map ∧ BlockDown(seed)
8. else
9. MUS ← Shrink(seed)
10. output MUS
11. map ← map ∧ BlockUp(seed)
12. midseed ← GetUnexploredMid(map, seed)
13. if midseed 未被探索过 then
14. if midseed 是可满足的 then
15. MSS ← Grow(midseed)
16. output MSS
17. map ← map ∧ BlockDown(midseed)
18. else