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

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

each MUS must be a superset of subMUS, and then the feature that MUS and MCS are mutually hitting sets can be effectively employed
to avoid the time cost in solving hitting sets of MCS. When the subMUS is unsatisfiable, it will be the only MUS, and the algorithm will
terminate in advance; otherwise, the node representing subMUS will be pruned to effectively avoid searching the non-solution space.
Meanwhile, the effectiveness of the proposed ABC scheme is proven by theorem, which has been applied to the state-of-the-art algorithms
MARCO and MARCO-MAM, respectively. Experimental results on SAT11 MUS benchmarks show the proposed scheme can effectively
prune the search space to improve the enumeration efficiency of MUS.
Key words: minimal unsatisfiable subset (MUS); maximal satisfiable subset (MSS); MUS enumeration; power set exploration; infeasibility
analysis

布尔可满足性问题 (Boolean satisfiability problem, SAT) 是第一个被证明的 NP 完全问题 [1] , 也是人工智能自
[2]
动推理领域中的关键问题, 在电子设计自动化 (EDA) 、基于模型诊断 [3−5] 、软件验证 [6] 、组合优化 [7−9] 、自动定
理证明 [10] 等问题上有着广泛的应用. 对于一个给定的布尔逻辑公式, SAT 求解器判断其可满足性: 若公式可满足,
则输出“可满足”并返回一组使得公式被满足的对布尔变量的完全赋值; 若公式不可满足, 则仅输出“不可满足”. 因
此, 对于那些不可满足的情况, 若单纯使用 SAT 求解器仅能得出一个“不可满足”的结论, 无法对于公式中的不可
满足性做进一步的分析. 在实际生产应用中, 对于不可满足性的进一步分析是有现实意义和价值的. 例如, 在需求
分析中, 每个需求对应着正在开发的系统中的约束, 对需求的一致性 (也称可满足性) 检查即为检查所有的需求是
否能同时被满足. 若约束集合是不可满足的, 则需要识别并修复这些需求之间的冲突.
当问题的约束 (即子句) 不能同时被满足时, 就构成了一个不可满足问题. 求解该问题的极小不可满足子集
(minimal unsatisfiable subset, MUS) 可以分析出公式中的具体哪些子句之间存在冲突 (即不能同时被满足); 求解该
问题的极大可满足子集 (maximal satisfiable subset, MSS) 可以分析出公式中哪些子句是一致的 (即可以同时被满
足); 求解该问题的极小修正集 (minimal correction set, MCS) 可以分析出去除哪些子句可以使得公式被满足. 对于
一个不可满足的情况, 它们能够从不同角度对不可满足性的原因、解决方案给出更具体的分析. 作为 SAT 问题的
一个重要扩展, MUS 的枚举同样有着广泛的现实应用, 例如本体调试 [11] 、本体中不一致性检测 [12] 、形式等效性
检查 [13] 、布尔函数的 2-分解 [14,15] 、基于模型的诊断问题 [16,17] 等领域中都有重要应用.
近年来, 国内外众多学者致力于对 MUS 枚举方法进行研究 [17−32] . 各式各样的枚举算法相继被提出, 从不同角
度提升了枚举性能. 在早期, 算法集中于求解单个 MUS. 然而, 由于 MUS 是极小不可满足子集, 它们对应于一个没
有被满足的约束系统中的“冲突”, 识别出越多的冲突, 越有助于我们理解系统没有被满足的原因, 从而更好地分析
并修复系统. 因此, 单一 MUS 的提取意义有限, 后续开始有工作倾向于更多 MUS 的枚举, 甚至全部枚举. 然而, 在
通常情况下, 由于 MUS 的个数与给定 CNF (conjunctive normal form) 公式的大小指数相关, 对于一些较大的实例
来说, 其 MUS 的全部枚举将是不可行的. 因此, 当实例的 MUS 完全枚举不可行时, 对其尽可能多的部分枚举成为
最佳选择. 近年来, 相关研究开始集中于 MUS 的部分枚举, 本文的研究也是针对 MUS 的部分枚举. 目前, MUS 的
枚举方法主要有两大分支: 基于碰集对偶性关系的算法和基于种子缩减的算法.
基于碰集对偶性关系的算法利用 MCS 与 MUS 互为极小碰集的性质进行求解, 这类方法通常先求出部分或
全部的 MSS, 然后根据 MCS 与 MSS 互为补集的性质计算出每个 MSS 所对应的 MCS, 对 MCS 集合求极小碰集
从而计算出 MUS 的集合, 代表的算法有 DAA [18] 、CAMUS [19] 、eMUS [20] 等. 2005 年, Bailey 等人 [18] 提出了 DAA
算法, 通过对当前节点进行扩充操作得到一个 MSS, 从而得到其对应的补集 MCS, 对当前的 MCS 集合求极小碰
集并判断其可满足性, 不断迭代上述过程从而计算出 MUS 的集合. 但由于 DAA 算法的枚举不具有完备性,
2008 年, Liffiton 等人 [19] 在 DAA 的基础上提出了完备的 CAMUS 算法, 与之不同的是, CAMUS 首先计算出全部
的 MSS, 再取其补集得到全部的 MCS, 并对 MCS 的集合求极小碰集得到全部 MUS 的集合. 可以看出, CAMUS
算法可以对 MUS 进行完备求解, 但其存在一个明显的短板——在对 MUS 的枚举开始前必须计算出全部的 MCS,
对于存在指数级数目 MCS 的不可满足问题而言, 使用 CAMUS 算法枚举 MUS 就会变得不可行. 2013 年, Previti
等人 [20] 为了克服 CAMUS 算法的这一显著短板提出了 eMUS 算法, 算法中使用极大化模型加速了求解过程. 在极
大化模型下, 若当前节点可满足则必是 MSS, 可以省去扩充操作的时间消耗. 同时, 对于每一个探索的种子节点,