138
J. Bend´ ık and I. ˇ
Cern´ a
Algorithm 1: Domain Agnostic Shrinking
input : an unsatisfiable set S of constraints
input : a set crits of constraints that are critical for S
output: A MUS of S
1 for c ∈ S \ crits do
2
if not CheckSat(S \ {c}) then
3
S ← S \ {c}
4 return S
2.2 Shrink
Let us now define an operation, called Shrink, that is used in our tool to identify
individual MUSes.
– Shrink(S, crits) takes an unsatisfiable subset S of C together with a set
crits of constraints that are critical for S and returns a MUS S mus of S.
We say that S is shrunk into a MUS S mus . The shrinking is maintained in
in our algorithms as a black-box subroutine and thus can be implemented using
any available single MUS extraction algorithm. Especially, we can implement the
operation using a domain specific solution and thus indirectly exploit domain
specific properties of particular constraint domains.
To shed more light on how a shrinking can be done, we describe in Algorithm 1 a domain agnostic single MUS extraction approach that forms the basis
of many contemporary domain specific solutions. To find a MUS of S, the algorithm iteratively attempts to remove individual constraints in S \ crits from
S, checking each new set for satisfiability, and keeping only the changes that
preserve S to be unsatisfiable. The most expensive part of the shrinking are the
satisfiability checks. In total, the algorithm performs |S| − |crits| satisfiability
checks. Domain specific algorithms (e.g. [5,24,1,19]) that are based on Algorithm 1 are often able to further reduce the number of performed satisfiability
checks by exploiting domain specific properties of particular constraint domains.
2.3 Unexplored Subsets
Our algorithms for MUS enumeration during their computation gradually explore
satisfiability of individual subsets of C. The explored subsets are those, whose
satisfiability is already known by the algorithm whereas unexplored subsets are
those whose satisfiability is not determined yet. We use Unexplored to denote
the set of all unexplored subsets of C. Recall that all subsets of a satisfiable set
are also satisfiable. Thus, if a set S is determined to be satisfiable, then not just
S but also all of its subsets become explored. Dually, if a set U is determined
to be unsatisfiable, then all supersets of U become explored. We further classify
unexplored subsets as follows:
J. Bend´ ık and I. ˇ
Cern´ a
Algorithm 1: Domain Agnostic Shrinking
input : an unsatisfiable set S of constraints
input : a set crits of constraints that are critical for S
output: A MUS of S
1 for c ∈ S \ crits do
2
if not CheckSat(S \ {c}) then
3
S ← S \ {c}
4 return S
2.2 Shrink
Let us now define an operation, called Shrink, that is used in our tool to identify
individual MUSes.
– Shrink(S, crits) takes an unsatisfiable subset S of C together with a set
crits of constraints that are critical for S and returns a MUS S mus of S.
We say that S is shrunk into a MUS S mus . The shrinking is maintained in
in our algorithms as a black-box subroutine and thus can be implemented using
any available single MUS extraction algorithm. Especially, we can implement the
operation using a domain specific solution and thus indirectly exploit domain
specific properties of particular constraint domains.
To shed more light on how a shrinking can be done, we describe in Algorithm 1 a domain agnostic single MUS extraction approach that forms the basis
of many contemporary domain specific solutions. To find a MUS of S, the algorithm iteratively attempts to remove individual constraints in S \ crits from
S, checking each new set for satisfiability, and keeping only the changes that
preserve S to be unsatisfiable. The most expensive part of the shrinking are the
satisfiability checks. In total, the algorithm performs |S| − |crits| satisfiability
checks. Domain specific algorithms (e.g. [5,24,1,19]) that are based on Algorithm 1 are often able to further reduce the number of performed satisfiability
checks by exploiting domain specific properties of particular constraint domains.
2.3 Unexplored Subsets
Our algorithms for MUS enumeration during their computation gradually explore
satisfiability of individual subsets of C. The explored subsets are those, whose
satisfiability is already known by the algorithm whereas unexplored subsets are
those whose satisfiability is not determined yet. We use Unexplored to denote
the set of all unexplored subsets of C. Recall that all subsets of a satisfiable set
are also satisfiable. Thus, if a set S is determined to be satisfiable, then not just
S but also all of its subsets become explored. Dually, if a set U is determined
to be unsatisfiable, then all supersets of U become explored. We further classify
unexplored subsets as follows: