针对MUS求解问题的加强剪枝策略  

Enhanced Pruning Scheme for Enumerating MUS

作　　者：蒋璐宇 欧阳丹彤[1,3] 董博文 张立明[1,3] JIANG Lu-Yu;OUYANG Dan-Tong;DONG Bo-Wen;ZHANG Li-Ming(College of Computer Science and Technology,Jilin University,Changchun 130012,China;College of Software,Jilin University,Changchun 130012,China;Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education(Jilin University),Changchun 130012,China)

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

出　　处：《软件学报》2024年第4期1964-1979,共16页Journal of Software

基　　金：国家自然科学基金(62076108,61872159,61972360)。

摘　　要：极小不可满足子集(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的枚举效率.Enumerating minimal unsatisfiable subsets(MUS)is an important subproblem in the Boolean satisfiability problem.For an unsatisfiable problem,the MUS enumeration can reflect the key factors resulting in its unsatisfiability.However,enumerating MUS is extremely time-consuming,and different pruning schemes will directly affect the size of the search space and the total number of iterations,thus affecting the algorithm efficiency.This study proposes a novel enhanced pruning scheme,accelerating by critical MSS(ABC),to accelerate the MUS enumeration.According to the relationship among maximal satisfiable subsets(MSS),minimal correction sets(MCS),and MUS,the concepts of cMSS and subMUS are put forward.Additionally,four properties are summarized,namely that 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.

关 键 词：极小不可满足子集 极大可满足子集 MUS枚举 幂集探索 不可行分析 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]