高级检索

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

    Incremental Information Interaction-Based Algorithm for Enumerating MUSes

    • 摘要: 极小不可满足子集(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标准测试用例上的实验验证了所提算法相较于当前先进算法的优越性,在部分测试用例上的结果显示所提算法的枚举效率和枚举获胜个数较已有算法均有显著的提高.

       

      Abstract: 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 theoretically is 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.

       

    /

    返回文章
    返回