Fast, flexible MUS enumeration
Fast, flexible MUS enumeration
复制标题
DOI：
10.1007/s10601-015-9183-0
复制
发表时间：
2016-04-01
期刊：
影响因子：
1.6
通讯作者：
Marques-Silva, Joao
中科院分区：
文献类型：
--
作者：
Liffiton, Mark H.;Previti, Alessandro;Marques-Silva, Joao
枚举不可行约束系统的最小不可满足子集的问题具有挑战性，首先是由于计算单个MU的复杂性，其次是一个实例可能包含的MU的潜在难以处理的数量。对于后一个问题，当完全列举不可行时，部分列举MU可能是有价值的，理想情况下，每个MU输出的时间成本不大于提取单个MU所需的时间成本。最近，两篇论文独立地提出了一种新的适用于部分MU枚举的MU枚举算法(Liffiton和Malik，2013，Previti和Marque-Silva，2013)。该算法表现出良好的随时性能，在其执行过程中稳定地产生缪斯；它是约束不可知的，同样适用于任何类型的约束系统；其灵活的结构使其能够结合单个MU提取算法的进步，并简化了进一步改进和修改的创建。本文统一和扩展了前人的工作，在一个框架中对算法的运行进行了详细的解释，并与以前的方法进行了更清晰的比较，同时我们也提出了一种新的算法优化。扩展的实验结果表明了该算法在过去方法上的改进，并对其一些变体进行了新的探索。
The problem of enumerating minimal unsatisfiable subsets (MUSes) of an infeasible constraint system is challenging due first to the complexity of computing even a single MUS and second to the potentially intractable number of MUSes an instance may contain. In the face of the latter issue, when complete enumeration is not feasible, a partial enumeration of MUSes can be valuable, ideally with a time cost for each MUS output no greater than that needed to extract a single MUS. Recently, two papers independently presented a new MUS enumeration algorithm well suited to partial MUS enumeration (Liffiton and Malik, 2013, Previti and Marques-Silva, 2013). The algorithm exhibits good anytime performance, steadily producing MUSes throughout its execution; it is constraint agnostic, applying equally well to any type of constraint system; and its flexible structure allows it to incorporate advances in single MUS extraction algorithms and eases the creation of further improvements and modifications. This paper unifies and expands upon the earlier work, presenting a detailed explanation of the algorithm's operation in a framework that also enables clearer comparisons to previous approaches, and we present a new optimization of the algorithm as well. Expanded experimental results illustrate the algorithm's improvement over past approaches and newly explore some of its variants.