In various areas of computer science, e.g. requirements analysis, softwaredevelopment, or formal verification, we deal with a set ofconstraints/requirements. If the constraints cannot be satisfiedsimultaneously, it is desirable to identify the core problems among them. Suchcores are called minimal unsatisfiable subsets (MUSes). The more MUSes areidentified, the more information about the conflicts among the constraints isobtained. However, a full enumeration of all MUSes is in general intractabledue to the combinatorial explosion. We therefore search for algorithms thatenumerate MUSes in an online manner, i.e. algorithms that produce MUSes one byone and can be terminated anytime. Furthermore, as the list of constraintdomains is quite long and new applications still arise, it is desirable to havealgorithms that are applicable in arbitrary constraint domain. The problem of online MUS enumeration in a general constraint domains hasbeen studied before and several algorithms were developed. However, themajority of these algorithms were evaluated only in the domain of Booleanlogic. In this work, we provide a novel recursive algorithm for online MUSenumeration that is applicable to an arbitrary constraint domain and thatoutperforms the state-of-the-art algorithms. We evaluate the algorithm on avariety of benchmarks taken from three different constraint domains: Booleanconstraints, SMT constraints, and LTL constraints.
展开▼
