Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
Jaroslav Bendik, Ivana Cerna, and Nikola Benes

TL;DR
This paper introduces a recursive online algorithm for efficiently enumerating all minimal unsatisfiable subsets (MUSes) of constraints, reducing the number of satisfiability tests needed and applicable across various domains including SMT.
Contribution
The paper presents a novel recursive algorithm for online MUS enumeration that minimizes satisfiability tests and is effective in domains with costly checks.
Findings
Requires fewer satisfiability tests than existing algorithms.
Finds more MUSes within the same time limits.
Effective in domains with expensive satisfiability checks.
Abstract
In various areas of computer science, we deal with a set of constraints to be satisfied. If the constraints cannot be satisfied simultaneously, it is desirable to identify the core problems among them. Such cores are called minimal unsatisfiable subsets (MUSes). The more MUSes are identified, the more information about the conflicts among the constraints is obtained. However, a full enumeration of all MUSes is in general intractable due to the large number (even exponential) of possible conflicts. Moreover, to identify MUSes algorithms must test sets of constraints for their simultaneous satisfiabilty. The type of the test depends on the application domains. The complexity of tests can be extremely high especially for domains like temporal logics, model checking, or SMT. In this paper, we propose a recursive algorithm that identifies MUSes in an online manner (i.e., one by one) and can…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Model-Driven Software Engineering Techniques
