MUST: Minimal Unsatisfiable Subsets Enumeration Tool
147
algorithm ReMUS. As for the shrinking, in SMT domain, we use our custom
shrinking solution, and in the SAT domain we employ a single MUS extraction
algorithm by Bacchus and Katsirelos [1]. Complete results of the evaluation are
available at: https://www.fi.muni.cz/%7exbendik/research/must.
All experiments were run using a time limit of 3600 seconds and computed on
an Intel(R) Core(TM) i5-4690 CPU, 3.50GHz, 16 GB memory machine running
Arch Linux 4.19.69-1-lts. The comparison criterion used in our evaluation is the
number of identified MUSes within the given time limit.
5.2 Benchmarks
In the SAT domain, we used a collection of 291 Boolean CNF benchmarks that
were taken from the MUS track of the SAT 2011 Competition
6 . This collection
has been used in many recent MUS related papers (e.g. [22,7,9,25,2]), including
the ones that present MARCO, FLINT, and MCSMUS. The benchmarks range in their
size from 70 to 16 million constraints and use from 26 to 4.4 million variables.
In case of 28 benchmarks, all the evaluated algorithms identified all the MUSes
within the given time limit. Since the comparison criterion of our evaluation is
the number of identified MUSes, the 28 benchmarks are irrelevant for the evaluation (all three tools found the same number of MUSes for these benchmarks).
Therefore, only the remaining 263 benchmarks are the subject of our evaluation.
In the SMT domain, we used a collection of 433 benchmarks that were taken
from the QF UF, QF IDL, QF RDL, QF LIA and QF LRA divisions of the library SMT-LIB
7 . Also this collection has been already used in several works, e.g.
in the work by Cimatti et al. [13] or in our recent papers [9,8]. The benchmarks
range in their size from 70 to 16 million constraints and use from 26 to 4.4 million
variables. In case of 249 benchmarks, both the evaluated algorithms identified
all the MUSes. Therefore, we focus here on the remaining 184 benchmarks.
5.3 Results
In Figs. 2a, 2b, and 2c, we provide scatter plots that compare pair-wise MUST
with the other tools in the SAT domain, and in Fig. 2d a scatter plot comparing
MUST with MARCO in the SMT domain. Each point in a scatter plot corresponds
to a single benchmark and shows the number of MUSes identified by the two
algorithms. The x-coordinate of a point is given by the algorithm that labels
the x-axis and the y-coordinate is given by the algorithm that labels the y-axis.
Moreover, note that each scatter plot contains three additional numbers that are
above/on right/in the right corner of the plot. These numbers show the number
of points that are above/below/on the diagonal, respectively.
In the SMT domain, MUST conclusively dominates MARCO: it found more, less,
and the same number of MUSes as MARCO in case of 100, 32, and 52 benchmarks,
respectively. In the SAT domain, MUST outperforms on majority of benchmarks
6 http://www.cril.univ-artois.fr/SAT11/
7 http://www.smt-lib.org/
147
algorithm ReMUS. As for the shrinking, in SMT domain, we use our custom
shrinking solution, and in the SAT domain we employ a single MUS extraction
algorithm by Bacchus and Katsirelos [1]. Complete results of the evaluation are
available at: https://www.fi.muni.cz/%7exbendik/research/must.
All experiments were run using a time limit of 3600 seconds and computed on
an Intel(R) Core(TM) i5-4690 CPU, 3.50GHz, 16 GB memory machine running
Arch Linux 4.19.69-1-lts. The comparison criterion used in our evaluation is the
number of identified MUSes within the given time limit.
5.2 Benchmarks
In the SAT domain, we used a collection of 291 Boolean CNF benchmarks that
were taken from the MUS track of the SAT 2011 Competition
6 . This collection
has been used in many recent MUS related papers (e.g. [22,7,9,25,2]), including
the ones that present MARCO, FLINT, and MCSMUS. The benchmarks range in their
size from 70 to 16 million constraints and use from 26 to 4.4 million variables.
In case of 28 benchmarks, all the evaluated algorithms identified all the MUSes
within the given time limit. Since the comparison criterion of our evaluation is
the number of identified MUSes, the 28 benchmarks are irrelevant for the evaluation (all three tools found the same number of MUSes for these benchmarks).
Therefore, only the remaining 263 benchmarks are the subject of our evaluation.
In the SMT domain, we used a collection of 433 benchmarks that were taken
from the QF UF, QF IDL, QF RDL, QF LIA and QF LRA divisions of the library SMT-LIB
7 . Also this collection has been already used in several works, e.g.
in the work by Cimatti et al. [13] or in our recent papers [9,8]. The benchmarks
range in their size from 70 to 16 million constraints and use from 26 to 4.4 million
variables. In case of 249 benchmarks, both the evaluated algorithms identified
all the MUSes. Therefore, we focus here on the remaining 184 benchmarks.
5.3 Results
In Figs. 2a, 2b, and 2c, we provide scatter plots that compare pair-wise MUST
with the other tools in the SAT domain, and in Fig. 2d a scatter plot comparing
MUST with MARCO in the SMT domain. Each point in a scatter plot corresponds
to a single benchmark and shows the number of MUSes identified by the two
algorithms. The x-coordinate of a point is given by the algorithm that labels
the x-axis and the y-coordinate is given by the algorithm that labels the y-axis.
Moreover, note that each scatter plot contains three additional numbers that are
above/on right/in the right corner of the plot. These numbers show the number
of points that are above/below/on the diagonal, respectively.
In the SMT domain, MUST conclusively dominates MARCO: it found more, less,
and the same number of MUSes as MARCO in case of 100, 32, and 52 benchmarks,
respectively. In the SAT domain, MUST outperforms on majority of benchmarks
6 http://www.cril.univ-artois.fr/SAT11/
7 http://www.smt-lib.org/