高级检索

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

    Incremental Information Interaction-Based Method for Enumerating MUSes

    • 摘要: 极小不可满足子集(minimal unsatisfiable subset,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 as many MUSes as possible within appropriate time limits. Dealing with the huge search space, choosing a suitable node to expand can markedly reduce the time consumption on shrink and grow operations, thereby the algorithm could obtain better performance. This paper introduces an incremental information interaction-based MUS solving method, denoted as MARCO-MSS4MUS, which utilizes the duality and complementary relationships among MUS, minimal correction sets (MCS), and maximal satisfiable subsets (MSS). Based on the framework of MARCO algorithm, the proposed method 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 help select a better node for next exploration, thereby achieving an interaction of incremental information. The paper presents two theorems and two corollaries regarding interactive incremental information, analyzing the feasibility of our MARCO-MSS4MUS algorithm theoretically. Experiments on standard MUS benchmark instances show the superiority of the proposed algorithm over state-of-the-art methods. Both the enumeration efficiency and the number of enumerated wins of the proposed method are significantly improved compared to existing methods.

       

    /

    返回文章
    返回