Tunable Online MUS/MSS Enumeration
This work addresses the need for efficient enumeration of MUSes and MSSes in computer science applications, representing an incremental improvement over existing online algorithms.
The authors tackled the problem of enumerating minimal unsatisfiable subsets (MUSes) and maximal satisfiable subsets (MSSes) for constraint systems by developing an online algorithm that outputs results as they are discovered, outperforming current state-of-the-art methods with tunable parameters for performance adjustment.
In various areas of computer science, the problem of dealing with a set of constraints arises. If the set of constraints is unsatisfiable, one may ask for a minimal description of the reason for this unsatisifi- ability. Minimal unsatisifable subsets (MUSes) and maximal satisifiable subsets (MSSes) are two kinds of such minimal descriptions. The goal of this work is the enumeration of MUSes and MSSes for a given constraint system. As such full enumeration may be intractable in general, we focus on building an online algorithm, which produces MUSes/MSSes in an on-the-fly manner as soon as they are discovered. The problem has been studied before even in its online version. However, our algorithm uses a novel approach that is able to outperform current state-of-the art algorithms for online MUS/MSS enumeration. Moreover, the performance of our algorithm can be adjusted using tunable parameters. We evaluate the algorithm on a set of benchmarks.