Tunable Online MUS/MSS Enumeration

TL;DR

This paper introduces a tunable online algorithm for enumerating minimal unsatisfiable subsets (MUSes) and maximal satisfiable subsets (MSSes) in constraint systems, outperforming existing methods and adaptable via adjustable parameters.

Contribution

The paper presents a novel, tunable online algorithm for MUS/MSS enumeration that improves performance over current state-of-the-art methods.

Findings

Outperforms existing online MUS/MSS algorithms.

Performance can be tuned with adjustable parameters.

Evaluated successfully on benchmark datasets.

Abstract

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.