146
J. Bend´ ık and I. ˇ
Cern´ a
caused by formatting and lines containing only closing brackets (”}”). Therefore,
we claim our tool to be indeed domain agnostic and ready-to-use solution for
any constraint domain.
4.4 Installation and Execution of the Tool
For detailed installation and usage instructions, please follow the README.md
file at: https://github.com/jar-ben/mustool.
Briefly, our tool can be built either in lightweight settings with support
only for SAT domain, or with support also for the SMT and/or LTL domains.
Whereas in the SAT domain, we use miniSAT that can be built very quickly,
the z3 and SPOT solvers that we use in the SMT and LTL domains can take
several hours to install. Once you have installed all the solvers you want to use,
our tool can be simply built with an invocation of the command ”make”.
To run our tool in its default settings, execute:
./must input file,
where input file specifies the input file of constraints, and it has to have either
.cnf, smt2, or .ltl extension. Based on the extension, Master selects and uses an
appropriate derived class of SatSolver. To specify a MUS enumeration algorithm
to be used, invoke the tool by:
./must -a alg input file,
where alg can be either marco, tome, or remus (the default one). To see all the
available settings, run
./must -h.
5 Experimental Evaluation
5.1 Evaluated Tools
The only other existing MUS enumeration tool that can be seen as domain agnostic is the implementation
3 of the domain agnostic algorithm MARCO (invented
by Liffiton et al. [22] and implemented by Liffiton and Zhao). In the following,
we refer to the tool as MARCO. Currently, MARCO supports the SAT and SMT domains and can also relatively easily be extended to support another constraint
domains. Here, we provide results of an experimental comparison of our tool
MUST with MARCO in both the SAT and SMT domains. Moreover, to demonstrate
that our domain agnostic tool can be competitive even to fully domain specific
solutions, we include a comparison with two state-of-the-art MUS enumeration
tools from the SAT domain: MCSMUS
4 [2] and FLINT
5 [25].
Due to the space limitation, we show here only results achieved by the best
(default) configurations of our tool. In particular, in both domains, we use the
3 https://sun.iwu.edu/%7emliffito/marco/
4 https://bitbucket.org/gkatsi/mcsmus/src
5 The tool was kindly provided to us by its author, Nina Narodytska.
J. Bend´ ık and I. ˇ
Cern´ a
caused by formatting and lines containing only closing brackets (”}”). Therefore,
we claim our tool to be indeed domain agnostic and ready-to-use solution for
any constraint domain.
4.4 Installation and Execution of the Tool
For detailed installation and usage instructions, please follow the README.md
file at: https://github.com/jar-ben/mustool.
Briefly, our tool can be built either in lightweight settings with support
only for SAT domain, or with support also for the SMT and/or LTL domains.
Whereas in the SAT domain, we use miniSAT that can be built very quickly,
the z3 and SPOT solvers that we use in the SMT and LTL domains can take
several hours to install. Once you have installed all the solvers you want to use,
our tool can be simply built with an invocation of the command ”make”.
To run our tool in its default settings, execute:
./must input file,
where input file specifies the input file of constraints, and it has to have either
.cnf, smt2, or .ltl extension. Based on the extension, Master selects and uses an
appropriate derived class of SatSolver. To specify a MUS enumeration algorithm
to be used, invoke the tool by:
./must -a alg input file,
where alg can be either marco, tome, or remus (the default one). To see all the
available settings, run
./must -h.
5 Experimental Evaluation
5.1 Evaluated Tools
The only other existing MUS enumeration tool that can be seen as domain agnostic is the implementation
3 of the domain agnostic algorithm MARCO (invented
by Liffiton et al. [22] and implemented by Liffiton and Zhao). In the following,
we refer to the tool as MARCO. Currently, MARCO supports the SAT and SMT domains and can also relatively easily be extended to support another constraint
domains. Here, we provide results of an experimental comparison of our tool
MUST with MARCO in both the SAT and SMT domains. Moreover, to demonstrate
that our domain agnostic tool can be competitive even to fully domain specific
solutions, we include a comparison with two state-of-the-art MUS enumeration
tools from the SAT domain: MCSMUS
4 [2] and FLINT
5 [25].
Due to the space limitation, we show here only results achieved by the best
(default) configurations of our tool. In particular, in both domains, we use the
3 https://sun.iwu.edu/%7emliffito/marco/
4 https://bitbucket.org/gkatsi/mcsmus/src
5 The tool was kindly provided to us by its author, Nina Narodytska.