MUST: Minimal Unsatisfiable Subsets Enumeration Tool
139
0000
0100
1000
0010
0001
1100
1010
1001
0110
0101
0011
1110
1101
1011
0111
1111
Fig. 1: Illustration of Example 2. We encode individual subsets of C as bitvectors; for example, the subset {c 1 , c 3 , c 4 } is written as 1011.
Definition 3 (Minimal Unexplored Subset). A set S is a minimal unexplored subset, if S is unexplored and for all c ∈ S is S \ {c} explored.
Definition 4 (Maximal Unexplored Subset). A set S is a maximal unexplored subset, if S is unexplored and for all c ∈ C \ S is S ∪ {c} explored.
Details on how we actually store, maintain, and use unexplored subsets are
described later in Section 4.2. Here, we conclude by defining the concept of
minable critical constraints:
Definition 5 (minable critical). Let N be an unsatisfiable subset of C such
that N ∈ Unexplored , and let c ∈ N . The constraint c is a minable critical
constraint for N if N \ {c} } ∈ Unexplored .
Example 2. Let us illustrate the concepts on an example. Assume that we are
given the same set of four constraints as in Example 1: c 1 = a, c 2 = ¬a, c 3 = b,
and c 4 = ¬a ∨ ¬b. Fig. 1 shows a possible state of exploration of the power-set.
Satisfiable subsets are drawn with a solid border and unsatisfiable ones with a
dashed border. There are 2 explored unsatisfiable subsets (red color), 7 explored
satisfiable subsets (green color), and 7 unexplored subsets (black color). There
are two minimal unexplored subsets: {c 2 } and {c 1 , c 3 , c 4 }, and three maximal
unexplored subsets: {c 1 , c 2 , c 3 }, {c 1 , c 3 , c 4 } and {c 2 , c 3 , c 4 }. As for the minable
critical constraints, we can for example see that c 2 is minable critical for the set
{c 1 , c 2 , c 3 }, and that all constraints are minable critical for the set {c 1 , c 3 , c 4 }.
3 Implemented Algorithms
Our tool currently implements three domain agnostic algorithms for online MUS
enumeration: MARCO [22], TOME [7], and ReMUS [9]. MARCO was originally
developed by Liffiton et al. [22]; the other two algorithms are originally ours.
All the three algorithms are based on a common scheme that we call seed-shrink
scheme. In this section, we first describe the base scheme and then briefly comment also on the individual algorithms.
139
0000
0100
1000
0010
0001
1100
1010
1001
0110
0101
0011
1110
1101
1011
0111
1111
Fig. 1: Illustration of Example 2. We encode individual subsets of C as bitvectors; for example, the subset {c 1 , c 3 , c 4 } is written as 1011.
Definition 3 (Minimal Unexplored Subset). A set S is a minimal unexplored subset, if S is unexplored and for all c ∈ S is S \ {c} explored.
Definition 4 (Maximal Unexplored Subset). A set S is a maximal unexplored subset, if S is unexplored and for all c ∈ C \ S is S ∪ {c} explored.
Details on how we actually store, maintain, and use unexplored subsets are
described later in Section 4.2. Here, we conclude by defining the concept of
minable critical constraints:
Definition 5 (minable critical). Let N be an unsatisfiable subset of C such
that N ∈ Unexplored , and let c ∈ N . The constraint c is a minable critical
constraint for N if N \ {c} } ∈ Unexplored .
Example 2. Let us illustrate the concepts on an example. Assume that we are
given the same set of four constraints as in Example 1: c 1 = a, c 2 = ¬a, c 3 = b,
and c 4 = ¬a ∨ ¬b. Fig. 1 shows a possible state of exploration of the power-set.
Satisfiable subsets are drawn with a solid border and unsatisfiable ones with a
dashed border. There are 2 explored unsatisfiable subsets (red color), 7 explored
satisfiable subsets (green color), and 7 unexplored subsets (black color). There
are two minimal unexplored subsets: {c 2 } and {c 1 , c 3 , c 4 }, and three maximal
unexplored subsets: {c 1 , c 2 , c 3 }, {c 1 , c 3 , c 4 } and {c 2 , c 3 , c 4 }. As for the minable
critical constraints, we can for example see that c 2 is minable critical for the set
{c 1 , c 2 , c 3 }, and that all constraints are minable critical for the set {c 1 , c 3 , c 4 }.
3 Implemented Algorithms
Our tool currently implements three domain agnostic algorithms for online MUS
enumeration: MARCO [22], TOME [7], and ReMUS [9]. MARCO was originally
developed by Liffiton et al. [22]; the other two algorithms are originally ours.
All the three algorithms are based on a common scheme that we call seed-shrink
scheme. In this section, we first describe the base scheme and then briefly comment also on the individual algorithms.