Page 395 - 《软件学报》2024年第4期
P. 395
蒋璐宇 等: 针对 MUS 求解问题的加强剪枝策略 1973
索到集合{1, 2, 3, 5}也是一个 MSS 时, 更新该例中 subMUS 为{4, 5}, 则使用 ABC 策略的情况下又可以比不使用
该策略的情况下多剪枝一个代表集合{4, 5}的节点. 因此, 在最优情况下, 使用 ABC 策略所能增加剪枝的节点个数
等同于该子句集中的关键 MSS 个数.
3.2 算法的伪代码
算法 4 和算法 5 分别是将本文提出的 ABC 策略应用于 MARCO 算法和 MARCO 算法后得到的 MARCO-
ABC 算法和 MARCO-MAM-ABC 算法的伪代码. 其中, ABC 策略在两个伪代码中的位置均位于第 8–16 行. 当算
法找到一个 MSS 时, 先通过其集合基数判断是否为关键 MSS. 如果它是关键 MSS, 那么该 MSS 对应的 MCS 为一
个单元素集合, 将此 MCS 中的唯一子句, 即关键 MSS 在子句集下缺少的子句加入 subMUS 中 (第 10 行), 判断
subMUS 的可满足性, 若可满足则剪枝 subMUS 集合所对应的节点 (第 11 行), 否则, 输出 subMUS 集合为该问题
唯一的 MUS, 算法终止 (第 12–15 行). 由于 subMUS 为不可满足时属于一种较为特殊的情况, 在第 3.1 节中的分
析可知, 只有当问题的全部 MSS 都是关键 MSS 时才会导致 subMUS 不可满足, 在这种情况下, 该问题的每一个
MSS 都是关键 MSS, 每一个 MCS 都是单元素集合, 且问题只有一个 MUS, 即 subMUS. 在实际应用中, 它对应于
一个过度约束的系统中只有一个冲突的情况. 因此考虑到这种情况的特殊性在使用该策略时也可以选择去掉伪代
码中 12–15 行的部分, 这样可以省去第 12 行对 SAT 求解器的调用.
算法 4. MARCO-ABC.
输入: 不可满足的子句集 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. if seed 是 cMSS then
9. MCS ← complement(seed)
10. subMUS ← subMUS ∪ MCS
11. map ← map ∧ BlockDown(subMUS)
12. if subMUS 是不可满足的 then
13. MUS ← subMUS
14. return
15. end if
16. end if
17. else
18. MUS ← Shrink(seed)
19. output MUS
20. map ← map ∧ BlockUp(seed)
21. end if
22. end while
