136
J. Bend´ ık and I. ˇ
Cern´ a
there can be up to exponentially many MUSes w.r.t. the number of constraints in
C. Therefore, several online MUS enumeration algorithms (e.g. [3,29,22,1,25,10])
were proposed, i.e. algorithms that identify MUSes gradually, one by one, and
thus identify at least some MUSes even in the intractable cases.
Various applications of MUSes arise for example in requirements analysis [4,6], during formal equivalence checking [15], proof based abstraction refinement [23], Boolean function bi-decomposition [12], circuit error diagnosis [21],
type debugging in Haskell [30], or proof explanation in symbolic model checking [20]. The domain of the constraint sets ranges from Boolean formulas [23,14],
over temporal logic formulas [4,6], to transition state predicates constraining
transition systems [20]. Since the list of constraint domains where MUSes find
an application is quite long and new applications still arise, there have been proposed several domain agnostic MUS enumeration algorithms (e.g. [3,22,9,7,10]).
Such algorithms can be used in an arbitrary constraint domain, and thus theoretically serve as ready-to-use solutions for any constraint domain where MUSes
might eventually find an application.
Unfortunately, there is no available domain agnostic tool implementation of
the algorithms that would actually serve as a ready-to-use solution for an arbitrary constraint domain. Although the papers that present existing domain
agnostic algorithms provide results of an experimental evaluation, it is often the
case that the implementation is either not publicly available [4,3], or there is a
hard-coded support for a particular constraint domain [10,20]. The closest to a
domain agnostic tool is a tool by Liffiton et al. [22] where the authors implement their domain agnostic MUS enumeration algorithm MARCO. Their tool
currently supports the SAT and the SMT domains and can be relatively easily extended to support also another constraint domains. However, our recent
evaluation [8] of contemporary domain agnostic algorithms in various constraint
domains has shown that the efficiency of the algorithms (including MARCO)
varies a lot in different constraint domains. There is no silver bullet algorithm
that would be efficient in all the domains. Thus, to deal with a particular constraint domain, one has to wisely choose from individual algorithms.
In this work, we present the first stable release of our domain agnostic tool,
called MUST, for MUS enumeration. The tool implements several domain agnostic
MUS enumeration algorithms and currently provides support for 3 constraint
domains: SAT, SMT, and LTL. Moreover, due to a modular architecture of the
tool, the tool can be easily extended to support another constraint domain: it
requires only to implement an API for communication with a satisfiability solver
for the constraint domain. We also provide a guidance on which algorithms are
suitable for which kinds of input constraint systems.
To demonstrate the efficiency of our tool, we experimentally compare it to
the tool by Liffiton et al. [22] in the SAT and SMT domains, and we show
that our tool clearly wins in both the domains. Moreover, we also provide a
comparison with two contemporary tools that are tailored to the SAT domain:
MCSMUS [1] and FLINT [25]. The results show that MUST is competitive to the two
J. Bend´ ık and I. ˇ
Cern´ a
there can be up to exponentially many MUSes w.r.t. the number of constraints in
C. Therefore, several online MUS enumeration algorithms (e.g. [3,29,22,1,25,10])
were proposed, i.e. algorithms that identify MUSes gradually, one by one, and
thus identify at least some MUSes even in the intractable cases.
Various applications of MUSes arise for example in requirements analysis [4,6], during formal equivalence checking [15], proof based abstraction refinement [23], Boolean function bi-decomposition [12], circuit error diagnosis [21],
type debugging in Haskell [30], or proof explanation in symbolic model checking [20]. The domain of the constraint sets ranges from Boolean formulas [23,14],
over temporal logic formulas [4,6], to transition state predicates constraining
transition systems [20]. Since the list of constraint domains where MUSes find
an application is quite long and new applications still arise, there have been proposed several domain agnostic MUS enumeration algorithms (e.g. [3,22,9,7,10]).
Such algorithms can be used in an arbitrary constraint domain, and thus theoretically serve as ready-to-use solutions for any constraint domain where MUSes
might eventually find an application.
Unfortunately, there is no available domain agnostic tool implementation of
the algorithms that would actually serve as a ready-to-use solution for an arbitrary constraint domain. Although the papers that present existing domain
agnostic algorithms provide results of an experimental evaluation, it is often the
case that the implementation is either not publicly available [4,3], or there is a
hard-coded support for a particular constraint domain [10,20]. The closest to a
domain agnostic tool is a tool by Liffiton et al. [22] where the authors implement their domain agnostic MUS enumeration algorithm MARCO. Their tool
currently supports the SAT and the SMT domains and can be relatively easily extended to support also another constraint domains. However, our recent
evaluation [8] of contemporary domain agnostic algorithms in various constraint
domains has shown that the efficiency of the algorithms (including MARCO)
varies a lot in different constraint domains. There is no silver bullet algorithm
that would be efficient in all the domains. Thus, to deal with a particular constraint domain, one has to wisely choose from individual algorithms.
In this work, we present the first stable release of our domain agnostic tool,
called MUST, for MUS enumeration. The tool implements several domain agnostic
MUS enumeration algorithms and currently provides support for 3 constraint
domains: SAT, SMT, and LTL. Moreover, due to a modular architecture of the
tool, the tool can be easily extended to support another constraint domain: it
requires only to implement an API for communication with a satisfiability solver
for the constraint domain. We also provide a guidance on which algorithms are
suitable for which kinds of input constraint systems.
To demonstrate the efficiency of our tool, we experimentally compare it to
the tool by Liffiton et al. [22] in the SAT and SMT domains, and we show
that our tool clearly wins in both the domains. Moreover, we also provide a
comparison with two contemporary tools that are tailored to the SAT domain:
MCSMUS [1] and FLINT [25]. The results show that MUST is competitive to the two