140
J. Bend´ ık and I. ˇ
Cern´ a
Algorithm 2: Seed-Shrink Scheme
input : an unsatisfiable set C of constraints
output: All MUSes of C
1 Unexplored ← P(C)
2 while there is a seed do
3
S ← find a seed
4
crits ← collect minable critical constraints for S
5
Smus ← Shrink(S, crits)
6
Unexplored ← Unexplored \ {T | T ⊂ Smus or Smus ⊆ T ⊆ C}
7
output Smus
3.1 Seed-Shrink Scheme
The seed-shrink scheme is shown in Algorithm 2. The computation starts by
initializing the set Unexplored to P(C), i.e. all subsets of C are initially unexplored. Subsequently, the scheme iteratively identifies all MUSes of C. Each
iteration starts by finding a so called seed, i.e. an unexplored subset that is unsatisfiable. Subsequently, the set crits of all constraints that are minable critical
for the seed are collected and the shrinking procedure is used to find a MUS of
the seed. The iteration is concluded by marking all subsets and supersets of the
MUS as explored (the subsets are necessarily satisfiable, and the supersets are
unsatisfiable). The computation terminates once there is no more seed.
The scheme does not specify how to find a seed; this part differs for individual
algorithms implementing the scheme. In general, to find a seed, the algorithms
check several unexplored subsets for satisfiability and reduce the set Unexplored.
The difference between the algorithms is in which and how many subsets they
check, and how large is the resultant seed. In general, the smaller the seed is,
the easier is to shrink it. On the other hand, unsatisfiable subsets are naturally
more concentrated among the larger subsets, thus looking for a seed among small
unexplored subsets might come with the price of checking many unexplored subsets for satisfiability. Individual seed-shrink algorithms make a different trade-off
between the size of identified seeds and the number of satisfiability checks that
are performed to identify the seeds. In some constraint domains, it is worth to
find a small seed even if it requires performing many satisfiability checks, and
in other constraint domains the situation is exactly the opposite. The optimal
choice of a seed-shrink algorithm thus differs for individual constraint domains.
MARCO [22] searches for a seed S among the maximal unexplored subsets and
often performs only few satisfiability checks to identify a seed. Since maximal
unexplored subsets are usually very large, the seeds identified by MARCO are
generally hard to be shrunk. Yet, in some constraint domains, such as SAT
and SMT, the size of the seed has just a negligible effect on the complexity
of the shrinking. In particular, in the SAT and SMT domains, contemporary
satisfiability solvers can extract an unsat core of the seed S, i.e. unsatisfiable,
yet not necessarily minimal, subset of S. The extraction comes with almost no
J. Bend´ ık and I. ˇ
Cern´ a
Algorithm 2: Seed-Shrink Scheme
input : an unsatisfiable set C of constraints
output: All MUSes of C
1 Unexplored ← P(C)
2 while there is a seed do
3
S ← find a seed
4
crits ← collect minable critical constraints for S
5
Smus ← Shrink(S, crits)
6
Unexplored ← Unexplored \ {T | T ⊂ Smus or Smus ⊆ T ⊆ C}
7
output Smus
3.1 Seed-Shrink Scheme
The seed-shrink scheme is shown in Algorithm 2. The computation starts by
initializing the set Unexplored to P(C), i.e. all subsets of C are initially unexplored. Subsequently, the scheme iteratively identifies all MUSes of C. Each
iteration starts by finding a so called seed, i.e. an unexplored subset that is unsatisfiable. Subsequently, the set crits of all constraints that are minable critical
for the seed are collected and the shrinking procedure is used to find a MUS of
the seed. The iteration is concluded by marking all subsets and supersets of the
MUS as explored (the subsets are necessarily satisfiable, and the supersets are
unsatisfiable). The computation terminates once there is no more seed.
The scheme does not specify how to find a seed; this part differs for individual
algorithms implementing the scheme. In general, to find a seed, the algorithms
check several unexplored subsets for satisfiability and reduce the set Unexplored.
The difference between the algorithms is in which and how many subsets they
check, and how large is the resultant seed. In general, the smaller the seed is,
the easier is to shrink it. On the other hand, unsatisfiable subsets are naturally
more concentrated among the larger subsets, thus looking for a seed among small
unexplored subsets might come with the price of checking many unexplored subsets for satisfiability. Individual seed-shrink algorithms make a different trade-off
between the size of identified seeds and the number of satisfiability checks that
are performed to identify the seeds. In some constraint domains, it is worth to
find a small seed even if it requires performing many satisfiability checks, and
in other constraint domains the situation is exactly the opposite. The optimal
choice of a seed-shrink algorithm thus differs for individual constraint domains.
MARCO [22] searches for a seed S among the maximal unexplored subsets and
often performs only few satisfiability checks to identify a seed. Since maximal
unexplored subsets are usually very large, the seeds identified by MARCO are
generally hard to be shrunk. Yet, in some constraint domains, such as SAT
and SMT, the size of the seed has just a negligible effect on the complexity
of the shrinking. In particular, in the SAT and SMT domains, contemporary
satisfiability solvers can extract an unsat core of the seed S, i.e. unsatisfiable,
yet not necessarily minimal, subset of S. The extraction comes with almost no