142
J. Bend´ ık and I. ˇ
Cern´ a
4 Architecture of the Tool
Our tool is implemented in C++ and is available under the MIT license at:
https://github.com/jar-ben/mustool
The tool consists of six logical components: SatSolver, Explorer, Master, Algorithms, Heuristics, and Initializer. In the following section 4.1 we provide a
brief description of the individual components. Subsequently, in Sections 4.2 and
4.3 we provide a more detailed description of Explorer and SatSolver. Finally, in
Section 4.4, we give instructions on how to install and use our tool.
4.1 Logical Components
SatSolver SatSolver (declared in SatSolver.h) is the only domain specific part
of our tool. It provides the functionality for checking sets of constraints for
satisfiability, and implements the shrinking procedure. Also, SatSolver copes
with parsing the input set of constraints (provided by the user) and exporting
the identified MUSes in particular domain specific formats. A more detailed
description of SatSolver is provided in Section 4.3.
Explorer Explorer (declared in Explorer.h) maintains the set Unexplored of all
unexplored subsets and handles related operations including: marking sets as
explored, obtaining unexplored subsets, and mining critical constraints based on
the set Unexplored. For more information, see Section 4.2.
Master Master (declared in Master.h) is the coordinator of the whole computation. In particular, it holds an instance of Explorer and an instance of SatSolver
and provides wrappers for calling their methods. Moreover, it runs a MUS enumeration algorithm that is specified by the user via a command line argument
(see below).
Algorithms The algorithms MARCO [22], TOME [7], and ReMUS [9] are
declared in Master (Master.h) and implemented in marco.cpp, tome.cpp, and
remus.cpp, respectively. All calls to SatSolver and Explorer are made via the
wrappers defined in Master. This means that any improvement to Explorer and
especially to SatSolver (i.e. a more efficient shrinking procedure or satisfiability
solver) is immediately reflected by all the algorithms.
Heuristics There are several heuristics that are bound to the wrappers defined
in Master, and thus can be exploited by all the three algorithms. For example, in
the wrapper for invoking the shrinking procedure, we provide two heuristics for
computing critical constraints for the set that is being shrunk. One of the two
heuristics uses Explorer to compute critical constraints based on the set Unexplored. The other heuristic uses SatSolver to obtain additional critical constraints
that cannot be mined from Unexplored.
J. Bend´ ık and I. ˇ
Cern´ a
4 Architecture of the Tool
Our tool is implemented in C++ and is available under the MIT license at:
https://github.com/jar-ben/mustool
The tool consists of six logical components: SatSolver, Explorer, Master, Algorithms, Heuristics, and Initializer. In the following section 4.1 we provide a
brief description of the individual components. Subsequently, in Sections 4.2 and
4.3 we provide a more detailed description of Explorer and SatSolver. Finally, in
Section 4.4, we give instructions on how to install and use our tool.
4.1 Logical Components
SatSolver SatSolver (declared in SatSolver.h) is the only domain specific part
of our tool. It provides the functionality for checking sets of constraints for
satisfiability, and implements the shrinking procedure. Also, SatSolver copes
with parsing the input set of constraints (provided by the user) and exporting
the identified MUSes in particular domain specific formats. A more detailed
description of SatSolver is provided in Section 4.3.
Explorer Explorer (declared in Explorer.h) maintains the set Unexplored of all
unexplored subsets and handles related operations including: marking sets as
explored, obtaining unexplored subsets, and mining critical constraints based on
the set Unexplored. For more information, see Section 4.2.
Master Master (declared in Master.h) is the coordinator of the whole computation. In particular, it holds an instance of Explorer and an instance of SatSolver
and provides wrappers for calling their methods. Moreover, it runs a MUS enumeration algorithm that is specified by the user via a command line argument
(see below).
Algorithms The algorithms MARCO [22], TOME [7], and ReMUS [9] are
declared in Master (Master.h) and implemented in marco.cpp, tome.cpp, and
remus.cpp, respectively. All calls to SatSolver and Explorer are made via the
wrappers defined in Master. This means that any improvement to Explorer and
especially to SatSolver (i.e. a more efficient shrinking procedure or satisfiability
solver) is immediately reflected by all the algorithms.
Heuristics There are several heuristics that are bound to the wrappers defined
in Master, and thus can be exploited by all the three algorithms. For example, in
the wrapper for invoking the shrinking procedure, we provide two heuristics for
computing critical constraints for the set that is being shrunk. One of the two
heuristics uses Explorer to compute critical constraints based on the set Unexplored. The other heuristic uses SatSolver to obtain additional critical constraints
that cannot be mined from Unexplored.