MUST: Minimal Unsatisfiable Subsets Enumeration Tool
137
domain specific solutions. Moreover in case of many benchmarks, MUST actually
significantly dominates the other tools.
Finally, to advocate the practical applicability of our tool in industrial settings, we provide a use case from the area of requirements analysis. In particular, we have employed our tool in the European Unions Horizon 2020 project
called AMASS. The project focused on development and verification of cyberphysical systems in the largest industrial markets including automotive, railway,
aerospace, space, and energy. One of the verification tasks is to verify that requirements on the system are consistent, i.e., to ensure that there can be even
built a system that satisfies the requirements. If the requirements are found to
be inconsistent, an identification of minimal inconsistent (unsatisifable) subsets
of the requirements helps to fix the conflicts among the requirements. Our tool
has proved to be very efficient in dealing with this task.
2 Preliminaries
2.1 Basic Definitions
We are given a set C = {c 1 , c 2 , . . . , c n } of constraints such that each subset of C
is either satisfiable or unsatisfiable. The notion of satisfiability varies in particular
constraint domains. We only assume that if a set N , N ⊆ C, is satisfiable then
all subsets of N are also satisfiable. Dually, if a set K, K ⊆ C, is unsatisfiable
then all supersets of K are also unsatisfiable. We will use C to denote the input
set of constraints throughout the whole paper.
Definition 1 (MUS). A subset N of C is a minimal unsatisfiable subset (MUS)
of C if and only if N is unsatisfiable and for all c ∈ N the set N \{c} is satisfiable.
Note that the minimality concept used here is set minimality, not minimum
cardinality. Therefore, there can be MUSes with different cardinalities. Also,
there can be up to exponentially many MUSes w.r.t. the number of constraints
in C (see the Sperner’s theorem [28]).
Definition 2 (critical constraint). Let U be an unsatisfiable subset of C and
c ∈ U . The constraint c is critical for U if and only if U \ {c} is satisfiable.
Note that U is a MUS of C if and only if all constraints in U are critical for
U . Furthermore, if c is critical for U then c has to be contained in every MUS
of U .
Example 1. We illustrate the concepts on a small example. Assume that we are
given a set C of four Boolean satisfiability constraints: c 1 = a, c 2 = ¬a, c 3 = b,
and c 4 = ¬a∨¬b. Clearly, the whole set is unsatisfiable as the first two constraints
are negations of each other. There are two MUSes: {c 1 , c 2 }, {c 1 , c 3 , c 4 }. As for the
critical constraints, we can for example see that c 1 is the only critical constraint
for C, and that c 1 , c 2 are critical for {c 1 , c 2 , c 3 }.
137
domain specific solutions. Moreover in case of many benchmarks, MUST actually
significantly dominates the other tools.
Finally, to advocate the practical applicability of our tool in industrial settings, we provide a use case from the area of requirements analysis. In particular, we have employed our tool in the European Unions Horizon 2020 project
called AMASS. The project focused on development and verification of cyberphysical systems in the largest industrial markets including automotive, railway,
aerospace, space, and energy. One of the verification tasks is to verify that requirements on the system are consistent, i.e., to ensure that there can be even
built a system that satisfies the requirements. If the requirements are found to
be inconsistent, an identification of minimal inconsistent (unsatisifable) subsets
of the requirements helps to fix the conflicts among the requirements. Our tool
has proved to be very efficient in dealing with this task.
2 Preliminaries
2.1 Basic Definitions
We are given a set C = {c 1 , c 2 , . . . , c n } of constraints such that each subset of C
is either satisfiable or unsatisfiable. The notion of satisfiability varies in particular
constraint domains. We only assume that if a set N , N ⊆ C, is satisfiable then
all subsets of N are also satisfiable. Dually, if a set K, K ⊆ C, is unsatisfiable
then all supersets of K are also unsatisfiable. We will use C to denote the input
set of constraints throughout the whole paper.
Definition 1 (MUS). A subset N of C is a minimal unsatisfiable subset (MUS)
of C if and only if N is unsatisfiable and for all c ∈ N the set N \{c} is satisfiable.
Note that the minimality concept used here is set minimality, not minimum
cardinality. Therefore, there can be MUSes with different cardinalities. Also,
there can be up to exponentially many MUSes w.r.t. the number of constraints
in C (see the Sperner’s theorem [28]).
Definition 2 (critical constraint). Let U be an unsatisfiable subset of C and
c ∈ U . The constraint c is critical for U if and only if U \ {c} is satisfiable.
Note that U is a MUS of C if and only if all constraints in U are critical for
U . Furthermore, if c is critical for U then c has to be contained in every MUS
of U .
Example 1. We illustrate the concepts on a small example. Assume that we are
given a set C of four Boolean satisfiability constraints: c 1 = a, c 2 = ¬a, c 3 = b,
and c 4 = ¬a∨¬b. Clearly, the whole set is unsatisfiable as the first two constraints
are negations of each other. There are two MUSes: {c 1 , c 2 }, {c 1 , c 3 , c 4 }. As for the
critical constraints, we can for example see that c 1 is the only critical constraint
for C, and that c 1 , c 2 are critical for {c 1 , c 2 , c 3 }.