计算机研究与发展

作者：蒋璐宇,欧阳丹彤,张奇,太然,张立明,

关键词：极小不可满足子集, 极大可满足子集, 不可行分析, 碰集, 对偶性,

极小不可满足子集（minimalunsatisfiablesubset，MUS）的求解是理论计算机科学的重要问题.由于MUS的个数随问题规模呈指数级增长，现有算法致力于在合适的时间限制内求解出尽可能多的MUS.在庞大的搜索空间中，选择合适的节点来扩展可以大幅减小收缩和扩充操作的时间开销，从而提高算法的求解效率.提出一种基于增量信息交互的MUS求解算法MARCO-MSS4MUS，利用MUS、极小修正集（minimalcorrectionset，MCS）和极大可满足子集（maximalsatisfiablesubset，MSS）之间的对偶和互补关系，在采用MARCO算法框架增量求解MSS和MUS的过程中，根据已求解的MSS的交集和并集信息辅助选择节点来扩展，即通过增量的MSS信息启发用于扩展节点选择以加速MUS枚举，这一过程同时利于算法找到更多的MSS，在枚举过程中新识别出的MSS又能辅助下一轮扩展节点的选择，从而实现了增量信息的有效交互.针对交互的增量信息提出2个定理及2个推论，从理论角度分析了MARCO-MSS4MUS算法的可行性，并通过MUS标准测试用例上的实验验证了所提算法相较于当前先进算法的优越性，在部分测试用例上的结果显示所提算法的枚举效率和枚举获胜个数较已有算法均有显著的提高.

来源：2025年第5期

《计算机研究与发展》期刊编辑部

查看计算机研究与发展杂志2025年第5期