Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BENDÍK Jaroslav ČERNÁ Ivana

Year of publication 2018
Type Article in Proceedings
Conference LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
MU Faculty or unit

Faculty of Informatics

Citation
Web http://www.easychair.org/publications/paper/m8qv
Doi http://dx.doi.org/10.29007/sxzb
Keywords minimal unsatisfiable subsets;mus enumeration;infeasibility analysis;unsatisfiability analysis
Description In many different applications we are given a set of constraints with the goal to decide whether the set is satisfiable. If the set is determined to be unsatisfiable, one might be interested in analysing this unsatisfiability. Identification of minimal unsatisfiable subsets (MUSes) is a kind of such analysis. The more MUSes are identified, the better insight into the unsatisfiability is obtained. However, the full enumeration of all MUSes is often intractable. Therefore, algorithms that identify MUSes in an online fashion, i.e., one by one, are needed. Moreover, since MUSes find applications in various constraint domains, and new applications still arise, there is a desire for domain agnostic MUS enumeration approaches. In this paper, we present an experimental evaluation of four state-of-the-art domain agnostic MUS enumeration algorithms: MARCO, TOME, ReMUS, and DAA. The evaluation is conducted in the SAT, SMT, and LTL constraint domains. The results evidence that there is no silver-bullet algorithm that would beat all the others in all the domains.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.