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

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

算法 5. MARCO-MAM-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. midseed ← GetUnexploredMid(map, seed)
22. if midseed 未被探索过 then
23. if midseed 是可满足的 then
24. MSS ← Grow(midseed)
25. output MSS
26. map ← map ∧ BlockDown(midseed)
27. else
28. MUS ← Shrink(midseed)
29. output MUS
30. map ← map ∧ BlockUp(midseed)
31. end if
32. end if
33. end if
34. end while

4 实验与分析

本文的实验环境为一台 60 GB RAM、Intel Xeon E5-2690v4 2.6 GHz 的 CPU、64 位 Ubuntu 18.04 版本 Linux