MUST: Minimal Unsatisfiable Subsets
Enumeration Tool
Jaroslav Bend´ ık and Ivana ˇ
Cern´ a
Faculty of Informatics, Masaryk University, Brno, Czech Republic
{xbendik,cerna}@fi.muni.cz
Abstract. In many areas of computer science, we are given an unsatisfiable set of constraints with the goal to provide an insight into the
unsatisfiability. One of common approaches is to identify minimal unsatisfiable subsets (MUSes) of the constraint set. The more MUSes are
identified, the better insight is obtained. However, since there can be
up to exponentially many MUSes, their complete enumeration might be
intractable. Therefore, we focus on algorithms that enumerate MUSes
online, i.e. one by one, and thus can find at least some MUSes even in
the intractable cases.
Since MUSes find applications in different constraint domains and new
applications still arise, there have been proposed several domain agnostic algorithms. Such algorithms can be applied in any constraint domain
and thus theoretically serve as ready-to-use solutions for all the emerging applications. However, there are almost no domain agnostic tools, i.e.
tools that both implement domain agnostic algorithms and can be easily
extended to support any constraint domain. In this work, we close this
gap by introducing a domain agnostic tool called MUST. Our tool outperforms other existing domain agnostic tools and moreover, it is even
competitive to fully domain specific solutions.
Keywords: Minimal unsatisfiable subsets · Unsatisfiability analysis ·
Infeasibility analysis · MUS · Diagnosis.
1 Introduction
In various areas of computer science, we are given a set C of constraints with the
goal to determine whether the set is satisfiable, i.e. whether all the constraints
can hold simultaneously. In the case where the set is shown to be unsatisfiable,
we are often interested in analysing the unsatisfiability. Identification of minimal
unsatisfiable subsets (MUSes) of C is a kind of such analysis. A set M ⊆ C is
a MUS of C iff M is unsatisfiable and all proper subsets of M are satisfiable.
The more MUSes are identified, the better insight into the unsatisfiability of C
is obtained. However, the complete MUS enumeration is often intractable since
This research was supported by ERDF ”CyberSecurity, CyberCrime
and Critical Information Infrastructures Center of Excellence” (No.
CZ.02.1.01/0.0/0.0/16 019/0000822).
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 135–152, 2020.
https://doi.org/10.1007/978-3-030-45190-5 8
TACAS
Evaluation
Artifact
2020
Accepted
Enumeration Tool
Jaroslav Bend´ ık and Ivana ˇ
Cern´ a
Faculty of Informatics, Masaryk University, Brno, Czech Republic
{xbendik,cerna}@fi.muni.cz
Abstract. In many areas of computer science, we are given an unsatisfiable set of constraints with the goal to provide an insight into the
unsatisfiability. One of common approaches is to identify minimal unsatisfiable subsets (MUSes) of the constraint set. The more MUSes are
identified, the better insight is obtained. However, since there can be
up to exponentially many MUSes, their complete enumeration might be
intractable. Therefore, we focus on algorithms that enumerate MUSes
online, i.e. one by one, and thus can find at least some MUSes even in
the intractable cases.
Since MUSes find applications in different constraint domains and new
applications still arise, there have been proposed several domain agnostic algorithms. Such algorithms can be applied in any constraint domain
and thus theoretically serve as ready-to-use solutions for all the emerging applications. However, there are almost no domain agnostic tools, i.e.
tools that both implement domain agnostic algorithms and can be easily
extended to support any constraint domain. In this work, we close this
gap by introducing a domain agnostic tool called MUST. Our tool outperforms other existing domain agnostic tools and moreover, it is even
competitive to fully domain specific solutions.
Keywords: Minimal unsatisfiable subsets · Unsatisfiability analysis ·
Infeasibility analysis · MUS · Diagnosis.
1 Introduction
In various areas of computer science, we are given a set C of constraints with the
goal to determine whether the set is satisfiable, i.e. whether all the constraints
can hold simultaneously. In the case where the set is shown to be unsatisfiable,
we are often interested in analysing the unsatisfiability. Identification of minimal
unsatisfiable subsets (MUSes) of C is a kind of such analysis. A set M ⊆ C is
a MUS of C iff M is unsatisfiable and all proper subsets of M are satisfiable.
The more MUSes are identified, the better insight into the unsatisfiability of C
is obtained. However, the complete MUS enumeration is often intractable since
This research was supported by ERDF ”CyberSecurity, CyberCrime
and Critical Information Infrastructures Center of Excellence” (No.
CZ.02.1.01/0.0/0.0/16 019/0000822).
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 135–152, 2020.
https://doi.org/10.1007/978-3-030-45190-5 8
TACAS
Evaluation
Artifact
2020
Accepted