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

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

seed 扩充成一个 seed 收缩为一个 MUS.
(2) 判断 seed 的可满足性: 若可满足, 将 MSS; 否则, 将
(3) 将其全部子集或全部超集标记为已探索.

算法 1. MARCO.
输入: 不可满足的子句集 C;
输出: 已找到的子句集 C 的 MUS 集合和 MSS 集合.
1. map ← BooleanFormula(nvars=|C|)
2. while map 是可满足的 do
3. seed ← GetUnexplored(map)
4. if seed is SAT then
5. MSS ← Grow(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
在 MARCO 算法的每一次迭代中, 都会将当前的 seed 转化为一个 MSS 或 MUS, 因此保证了每轮迭代都会有
一个新输出的解. 根据可满足性问题的特点可知, 一个可满足的子句集的任何一个子集也一定是可满足的, 一个不
可满足的子句集的任何一个超集也一定是不可满足的. 因此, 算法每输出一个 MSS (或 MUS) 时, 将通过
BlockDown (或 BlockUp) 操作向公式 map 中添加相应子句以阻塞该 MSS 的全部子集 (或该 MUS 的全部超集), 从
而缩减了搜索空间, 避免了算法在无解空间中的探索.
使用极大化模型的 MARCO 算法 (算法 2) 是其作者在 2016 年对于 MARCO 算法提出的一个优化版本 [22] , 它
与上文提到的 MARCO 算法有两个主要差别: (1) 在每轮迭代开始时, MARCO 算法随机选择一个未探索的种子节
点, 而极大化模型的 MARCO 算法则选择当前哈斯图中的极大未探索种子节点. (2) 当选择的种子节点判定为可满
足时, MARCO 算法需要对该种子进行扩充操作, 使其转化为一个 MSS; 而极大化模型的 MARCO 算法则可以省
略对种子的扩充操作, 直接将该种子输出为一个 MSS, 这是由于极大化模型保证了种子节点是极大未探索子集,
因此无需对种子进行扩充操作. 极大化模型 MARCO 算法的伪代码描述在算法 2 中, 可以看出算法 1 和算法 2 的
区别也体现在第 3 行和第 5 行. 算法 1 中第 3 行通过调用 GetUnexplored 函数从 map 中选取一个子句集的未探索子集作

为 seed , 而算法 2 中第 3 行则调用 GetUnexploredMax 函数从 map 中选取一个子句集的极大未探索子集作为 seed ;
算法 1 中第 5 行对当前判定为可满足的 seed 执行了扩充操作, 得到一个极大可满足子集, 而算法 2 中第 5 行将当
前判定为可满足的 seed 直接作为一个极大可满足子集. 优化后的 MARCO 在算法初期更倾向于找到更多的 MUS,
同时省去了扩充操作的时间开销, 在一定程度上加速了枚举 MUS 的效率.
算法 2. MARCO+: 使用极大化模型的优化版本.

输入: 不可满足的子句集 C;
输出: 已找到的子句集 C 的 MUS 集合和 MSS 集合.

1. map ← BooleanFormula(nvars=|C|)
2. while map 是可满足的 do