MUST: Minimal Unsatisfiable Subsets Enumeration Tool
141
overhead compared to an ordinary check for satisfiability, and the unsat core
is usually very close, in terms of cardinality, to a MUS of S. Thus, instead of
shrinking the whole S, the unsat core is passed to the shrinking procedure.
TOME [7] identifies seeds iteratively as follows. Each iteration of the algorithm
starts by picking a minimal unexplored subset N 1 and a maximal unexplored
subset N p such that N 1 ⊆ N p . Subsequently, TOME builds a chain N 1 ⊂ N 2 ⊂
· · · ⊂ N p of unexplored subsets. Such a chain necessarily either contains only
unsatisfiable subsets, only satisfiable subsets, or it contains an element N i such
that ∀j, 1 ≤ j < i, is N j satisfiable and ∀k, i ≤ k ≤ p, is N k unsatisfiable. In the
first case, it is guaranteed that N 1 is a MUS. In the second case, the chain does
not give us any seed. Finally, in the third case, TOME finds N i using binary
search (which takes only O(log 2 p) satisfiability checks). Subsequently N i is used
as a seed for the shrinking procedure and shrunk into a MUS.
There are no guarantees on distribution of satisfiable and unsatisfiable subsets on the chain, since the subsets are unexplored. In the best case, where N 1
is unsatisfiable, TOME identifies a MUS using just a single satisfiability check.
In the worst case, the whole chain is satisfiable and TOME has to build another
chain. Based on our experience, TOME on average performs more satisfiability
checks to find a seed than MARCO does, but the seeds are much smaller than in
the case of MARCO. Thus, TOME is efficient especially in constraint domains
where the size of the seed highly affects the complexity of the shrinking.
ReMUS [9] is based on the following observation: if C, C
k , and M are unsatisfiable sets such that C
k
⊆ C and M is a MUS of C
k , then M is necessarily also
a MUS of C. Note that the smaller C
k is the smaller seeds are in C
k . ReMUS
tends to identify C
k that is very small, yet contains many MUSes, and searches
for seeds in C
k . In particular, the very first seed S is found among the maximal
unexplored subsets of C
0 = C and then shrunk to a MUS S mus . To find a next
seed, ReMUS chooses C
1 such that S mus ⊆ C
1
⊆ S, and searches for a seed S
1
among maximal unexplored subsets of C
1 . If a seed S
1 is identified, then it is
again shrunk to a MUS S
1
mus and again used to reduce the search space, i.e. the
a next seed S
2 is searched for in a set C
2 such that S
1
mus ⊆ C
2
⊆ S
1 . The search
space reduction is recursively repeated as long as possible. Once the current
search space is completely explored, ReMUS backtracks from the recursion and
searches for a seed on the previous recursion level. Moreover, ReMUS employs
several heuristics to pre-emptively backtrack from a search space that contains
a lot of unexplored subsets but only few MUSes.
The larger the input set C of constraints is, the more extensive recursive
reduction is possible, and thus the smaller seeds can be found. We recommend to
use ReMUS, rather than MARCO or TOME, if the input constraint set contains
at least hundreds of constraints and hundreds of MUSes, no matter what the
constraint domain is.
For a more elaborated description of the three algorithms, please refer to the
original papers [22,7,9] or to our recent work [8] where we have experimentally
compared the algorithms in various constraint domains.
141
overhead compared to an ordinary check for satisfiability, and the unsat core
is usually very close, in terms of cardinality, to a MUS of S. Thus, instead of
shrinking the whole S, the unsat core is passed to the shrinking procedure.
TOME [7] identifies seeds iteratively as follows. Each iteration of the algorithm
starts by picking a minimal unexplored subset N 1 and a maximal unexplored
subset N p such that N 1 ⊆ N p . Subsequently, TOME builds a chain N 1 ⊂ N 2 ⊂
· · · ⊂ N p of unexplored subsets. Such a chain necessarily either contains only
unsatisfiable subsets, only satisfiable subsets, or it contains an element N i such
that ∀j, 1 ≤ j < i, is N j satisfiable and ∀k, i ≤ k ≤ p, is N k unsatisfiable. In the
first case, it is guaranteed that N 1 is a MUS. In the second case, the chain does
not give us any seed. Finally, in the third case, TOME finds N i using binary
search (which takes only O(log 2 p) satisfiability checks). Subsequently N i is used
as a seed for the shrinking procedure and shrunk into a MUS.
There are no guarantees on distribution of satisfiable and unsatisfiable subsets on the chain, since the subsets are unexplored. In the best case, where N 1
is unsatisfiable, TOME identifies a MUS using just a single satisfiability check.
In the worst case, the whole chain is satisfiable and TOME has to build another
chain. Based on our experience, TOME on average performs more satisfiability
checks to find a seed than MARCO does, but the seeds are much smaller than in
the case of MARCO. Thus, TOME is efficient especially in constraint domains
where the size of the seed highly affects the complexity of the shrinking.
ReMUS [9] is based on the following observation: if C, C
k , and M are unsatisfiable sets such that C
k
⊆ C and M is a MUS of C
k , then M is necessarily also
a MUS of C. Note that the smaller C
k is the smaller seeds are in C
k . ReMUS
tends to identify C
k that is very small, yet contains many MUSes, and searches
for seeds in C
k . In particular, the very first seed S is found among the maximal
unexplored subsets of C
0 = C and then shrunk to a MUS S mus . To find a next
seed, ReMUS chooses C
1 such that S mus ⊆ C
1
⊆ S, and searches for a seed S
1
among maximal unexplored subsets of C
1 . If a seed S
1 is identified, then it is
again shrunk to a MUS S
1
mus and again used to reduce the search space, i.e. the
a next seed S
2 is searched for in a set C
2 such that S
1
mus ⊆ C
2
⊆ S
1 . The search
space reduction is recursively repeated as long as possible. Once the current
search space is completely explored, ReMUS backtracks from the recursion and
searches for a seed on the previous recursion level. Moreover, ReMUS employs
several heuristics to pre-emptively backtrack from a search space that contains
a lot of unexplored subsets but only few MUSes.
The larger the input set C of constraints is, the more extensive recursive
reduction is possible, and thus the smaller seeds can be found. We recommend to
use ReMUS, rather than MARCO or TOME, if the input constraint set contains
at least hundreds of constraints and hundreds of MUSes, no matter what the
constraint domain is.
For a more elaborated description of the three algorithms, please refer to the
original papers [22,7,9] or to our recent work [8] where we have experimentally
compared the algorithms in various constraint domains.