基于增量信息交互的极小不可满足子集求解算法  

Incremental Information Interaction-Based Algorithm for Enumerating MUSes

作　　者：蒋璐宇 欧阳丹彤[1,2] 张奇 太然 张立明[1,2] Jiang Luyu;Ouyang Dantong;Zhang Qi;Tai Ran;Zhang Liming(College of Computer Science and Technology,Jilin University,Changchun 130012;Key Laboratory of Symbol Computation and Knowledge Engineering(Jilin University),Ministry of Education,Changchun 130012)

机构地区：[1]吉林大学计算机科学与技术学院,长春130012 [2]符号计算与知识工程教育部重点实验室(吉林大学),长春130012

出　　处：《计算机研究与发展》2025年第5期1226-1234,共9页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(62076108,61872159);吉林省教育厅科学研究项目(JJKH20211106KJ,JJKH20211103KJ)。

摘　　要：极小不可满足子集(minimal unsatisfiable subset,MUS)的求解是理论计算机科学的重要问题.由于MUS的个数随问题规模呈指数级增长,现有算法致力于在合适的时间限制内求解出尽可能多的MUS.在庞大的搜索空间中,选择合适的节点来扩展可以大幅减小收缩和扩充操作的时间开销,从而提高算法的求解效率.提出一种基于增量信息交互的MUS求解算法MARCO-MSS4MUS,利用MUS、极小修正集(minimal correction set,MCS)和极大可满足子集(maximal satisfiable subset,MSS)之间的对偶和互补关系,在采用MARCO算法框架增量求解MSS和MUS的过程中,根据已求解的MSS的交集和并集信息辅助选择节点来扩展,即通过增量的MSS信息启发用于扩展节点选择以加速MUS枚举,这一过程同时利于算法找到更多的MSS,在枚举过程中新识别出的MSS又能辅助下一轮扩展节点的选择,从而实现了增量信息的有效交互.针对交互的增量信息提出2个定理及2个推论,从理论角度分析了MARCO-MSS4MUS算法的可行性,并通过MUS标准测试用例上的实验验证了所提算法相较于当前先进算法的优越性,在部分测试用例上的结果显示所提算法的枚举效率和枚举获胜个数较已有算法均有显著的提高.Enumerating minimal unsatisfiable subsets(MUS)is an important issue in theoretical computer science.Given an unsatisfiable Boolean formula,the number of its MUS is exponentially related to the formula’s scale.Contemporary methods aim to identify MUSes as many as possible within appropriate time limits.Dealing with the huge search space and choosing a suitable node to expand can markedly reduce the time consumption on shrink and grow operations,thereby the algorithm could obtain better performance.We introduce an incremental information interaction-based MUS solving algorithm,denoted as MARCO-MSS4MUS,which utilizes the duality and complementary relationships among MUS,minimal correction set(MCS),and maximal satisfiable subset(MSS).Based on the framework of MARCO algorithm,the proposed algorithm selects a more suitable node to expand via intersection and union information of previously identified MSSes during the search,i.e.,the incremental MSS information is employed as a heuristic for node selection to accelerate the enumeration of MUS.This process also benefits in identifying more MSSes,in turn,the incremental MSS information helps select a better node for next exploration,thereby achieving an interaction of incremental information.Two theorems and two corollaries regarding interactive incremental information are proposed and the feasibility of our MARCO-MSS4MUS algorithm is theoretically analyzed.Experiments on standard MUS benchmark instances show the superiority of the proposed algorithm over state-of-the-art algorithms.Both the enumeration efficiency and the number of enumerated wins of the proposed algorithm are significantly improved compared with existing algorithms.

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

分 类 号：TP391[自动化与计算机技术—计算机应用技术]