MUST: Minimal Unsatisfiable Subsets Enumeration Tool
145
e.g. invokes the procedure solve(N ), it passes the bit-vector representation
of N to SatSolver and SatSolver converts it to particular constraints.
Besides the above three methods that have to be implemented by every derived class, SatSolver defines and implements a method that can be overridden
by a derived class:
– shrink(N , crits) performs the shrinking, i.e. it takes an unsatisfiable set
N together with a set crits of constraints that are critical for N and returns
a MUS of N . The default domain agnostic implementation of this method
is carried out by Algorithm 1 (Section 2.2).
Currently, our tool supports 3 constraint domains via the following 4 derived
classes of SatSolver:
– MSHandle (implemented in MSHandle.cpp) provides a functionality for the
Boolean CNF domain, i.e. the set of constraints is a set of Boolean clauses.
The input and output format is the DIMACS CNF format. For shrinking,
we integrate two single MUS extraction tools: muser2 [5] by Belov and Silva,
and a tool [1] by Bacchus and Katsirelos. Finally, we use miniSAT [18] to
implement the method solve. Besides checking N for satisfiability, we also
use miniSAT to obtain an unsat core or an extension of N . In particular, an
unsat core is directly provided by miniSAT. To get an extension of N , we
obtain a model π of N from miniSAT and collect the set {c|c ∈ C ∧ π |= c}
of all constraints in C that are satisfied by π.
– Z3Handle (implemented in Z3Handle.cpp) processes SMT constraints that
are represented in the SMT-LIB2 format. We use z3 [16] to parse the input and to implement solve. Moreover, in the same way as in the case of
MSHandle, we obtain unsat cores from z3 and we also obtain models of satisfiables formulas to compute their extensions. The shrinking is implemented
using our custom procedure.
– SpotHandle (implemented in SpotHandle.cpp) supports the LTL domain.
We use SPOT [17] to implement solve and the default domain agnostic
implementation of shrink. In this case, we do not provide support for computing non-trivial unsat cores and non-trivial extension. Therefore, if an
extension or unsat core is required while calling solve(N ), we simply use
N itself (N is a trivial unsat core/extension of N ).
– NuxmvHandle (implemented in NuxmvHandle.cpp) is another alternative
for the LTL domain. Instead of SPOT, it uses nuXmv [11] as a satisfiability
solver, which is, based on our experience, much more efficient than SPOT.
However, nuXmv’s license
2 is more restrictive than the SPOT’s license and
thus not every user of our tool might use it. In this case, we also do not
support an extraction of non-trivial unsat cores and extensions.
If anyone wants to add support for another constraint domain to our tool, it
is enough to implement a derived class of SatSolver. For example, the implementation of SpotHandle takes only 45 lines of code, including several empty lines
2 https://es-static.fbk.eu/tools/nuxmv/index.php?n=Main.License
145
e.g. invokes the procedure solve(N ), it passes the bit-vector representation
of N to SatSolver and SatSolver converts it to particular constraints.
Besides the above three methods that have to be implemented by every derived class, SatSolver defines and implements a method that can be overridden
by a derived class:
– shrink(N , crits) performs the shrinking, i.e. it takes an unsatisfiable set
N together with a set crits of constraints that are critical for N and returns
a MUS of N . The default domain agnostic implementation of this method
is carried out by Algorithm 1 (Section 2.2).
Currently, our tool supports 3 constraint domains via the following 4 derived
classes of SatSolver:
– MSHandle (implemented in MSHandle.cpp) provides a functionality for the
Boolean CNF domain, i.e. the set of constraints is a set of Boolean clauses.
The input and output format is the DIMACS CNF format. For shrinking,
we integrate two single MUS extraction tools: muser2 [5] by Belov and Silva,
and a tool [1] by Bacchus and Katsirelos. Finally, we use miniSAT [18] to
implement the method solve. Besides checking N for satisfiability, we also
use miniSAT to obtain an unsat core or an extension of N . In particular, an
unsat core is directly provided by miniSAT. To get an extension of N , we
obtain a model π of N from miniSAT and collect the set {c|c ∈ C ∧ π |= c}
of all constraints in C that are satisfied by π.
– Z3Handle (implemented in Z3Handle.cpp) processes SMT constraints that
are represented in the SMT-LIB2 format. We use z3 [16] to parse the input and to implement solve. Moreover, in the same way as in the case of
MSHandle, we obtain unsat cores from z3 and we also obtain models of satisfiables formulas to compute their extensions. The shrinking is implemented
using our custom procedure.
– SpotHandle (implemented in SpotHandle.cpp) supports the LTL domain.
We use SPOT [17] to implement solve and the default domain agnostic
implementation of shrink. In this case, we do not provide support for computing non-trivial unsat cores and non-trivial extension. Therefore, if an
extension or unsat core is required while calling solve(N ), we simply use
N itself (N is a trivial unsat core/extension of N ).
– NuxmvHandle (implemented in NuxmvHandle.cpp) is another alternative
for the LTL domain. Instead of SPOT, it uses nuXmv [11] as a satisfiability
solver, which is, based on our experience, much more efficient than SPOT.
However, nuXmv’s license
2 is more restrictive than the SPOT’s license and
thus not every user of our tool might use it. In this case, we also do not
support an extraction of non-trivial unsat cores and extensions.
If anyone wants to add support for another constraint domain to our tool, it
is enough to implement a derived class of SatSolver. For example, the implementation of SpotHandle takes only 45 lines of code, including several empty lines
2 https://es-static.fbk.eu/tools/nuxmv/index.php?n=Main.License