摘要:极小不可满足子集(minimal unsatisfiable subsets, MUS)的求解是布尔可满足性问题中的一个重要子问题. 对于一个给定的不可满足问题, 其MUS的求解能够反映出问题中导致其不可满足的关键原因. 然而, MUS的求解是一项极其耗时的任务, 不同的剪枝过程将直接影响到搜索空间的大小、算法的迭代次数, 从而影响算法的求解效率. 提出一种针对MUS求解的加强剪枝策略ABC (accelerating by critical MSS), 依据MSS、MCS、MUS这3者之间的对偶性和碰集关系特点, 提出cMSS和subMUS概念, 并总结出4条性质, 即每个MUS必是subMUS的超集, 进而在避免对MCS的碰集进行求解的情况下有效利用MUS和MCS互为碰集的特征, 有效避免求解碰集时的时间开销. 当subMUS不可满足时, 则subMUS是唯一的MUS, 算法将提前结束执行; 当subMUS可满足时, 则剪枝掉此节点, 进而有效避免对求解空间中的冗余空间进行搜索. 同时, 通过理论证明ABC策略的有效性, 并将其应用于目前最高效的单一化模型算法MARCO和双模型算法MARCO-MAM, 在标准测试用例下的实验结果表明, 该策略可以有效地对搜索空间进行进一步剪枝, 从而提高MUS的枚举效率.