148
J. Bend´ ık and I. ˇ
Cern´ a
10 0
10 1
10 2
10 3
10 4
10 5
10 6
10 0 10 1 10 2 10 3 10 4 10 5 10 6
85
162
1 6
# MUSes FLINT
# MUSes MUST
(a) MUST vs. FLINT, SAT domain
10 0
10 1
10 2
10 3
10 4
10 5
10 6
10 0 10 1 10 2 10 3 10 4 10 5 10 6
61
184
1 8
# MUSes MARCO
# MUSes MUST
(b) MUST vs. MARCO, SAT domain
10 0
10 1
10 2
10 3
10 4
10 5
10 6
10 0 10 1 10 2 10 3 10 4 10 5 10 6
138
114
1
1
# MUSes MCSMUS
# MUSes MUST
(c) MUST vs. MCSMUS, SAT domain
10 0
10 1
10 2
10 3
10 4
10 5
10 6
10 0 10 1 10 2 10 3 10 4 10 5 10 6
32
100
5 2
# MUSes MARCO
# MUSes MUST
(d) MUST vs. MARCO, SMT domain
Fig. 2: Scatter plots comparing the number of produced MUSes.
both MARCO and FLINT. Finally, MCSMUS outperforms MUST in case of 52 percent
of benchmarks and is worse than MUST in case of 43 percent of benchmarks. Still,
this is a very good result since MUST is a domain agnostic tool whereas MCSMUS
is tailored to the SAT domain.
Besides the pair-wise comparison of the algorithms, we also provide an overall
ranking of the algorithms on individual benchmarks in the SAT domain. In
particular, assume that for a benchmark B both MUST and MCSMUS found 100
MUSes, FLINT found 80 MUSes, and MARCO found 50 MUSes. In such a case, MUST
and MCSMUS share the 1st (best) rank for B , FLINT is 3rd, and MARCO is on the
4th position. In Fig. 3 we show the average ranking (from all benchmarks) of all
algorithms for each subsequent 60 seconds of the computation. We can see that
MARCO ranked the worse during the whole computation. FLINT ranked quite well
during the first 600 seconds, but then its performance degraded. Finally, MUST
and MCSMUS maintained the best and the second best ranking, respectively. This
might be quite surprising since MCSMUS is slightly better than MUST in Fig. 2c.
J. Bend´ ık and I. ˇ
Cern´ a
10 0
10 1
10 2
10 3
10 4
10 5
10 6
10 0 10 1 10 2 10 3 10 4 10 5 10 6
85
162
1 6
# MUSes FLINT
# MUSes MUST
(a) MUST vs. FLINT, SAT domain
10 0
10 1
10 2
10 3
10 4
10 5
10 6
10 0 10 1 10 2 10 3 10 4 10 5 10 6
61
184
1 8
# MUSes MARCO
# MUSes MUST
(b) MUST vs. MARCO, SAT domain
10 0
10 1
10 2
10 3
10 4
10 5
10 6
10 0 10 1 10 2 10 3 10 4 10 5 10 6
138
114
1
1
# MUSes MCSMUS
# MUSes MUST
(c) MUST vs. MCSMUS, SAT domain
10 0
10 1
10 2
10 3
10 4
10 5
10 6
10 0 10 1 10 2 10 3 10 4 10 5 10 6
32
100
5 2
# MUSes MARCO
# MUSes MUST
(d) MUST vs. MARCO, SMT domain
Fig. 2: Scatter plots comparing the number of produced MUSes.
both MARCO and FLINT. Finally, MCSMUS outperforms MUST in case of 52 percent
of benchmarks and is worse than MUST in case of 43 percent of benchmarks. Still,
this is a very good result since MUST is a domain agnostic tool whereas MCSMUS
is tailored to the SAT domain.
Besides the pair-wise comparison of the algorithms, we also provide an overall
ranking of the algorithms on individual benchmarks in the SAT domain. In
particular, assume that for a benchmark B both MUST and MCSMUS found 100
MUSes, FLINT found 80 MUSes, and MARCO found 50 MUSes. In such a case, MUST
and MCSMUS share the 1st (best) rank for B , FLINT is 3rd, and MARCO is on the
4th position. In Fig. 3 we show the average ranking (from all benchmarks) of all
algorithms for each subsequent 60 seconds of the computation. We can see that
MARCO ranked the worse during the whole computation. FLINT ranked quite well
during the first 600 seconds, but then its performance degraded. Finally, MUST
and MCSMUS maintained the best and the second best ranking, respectively. This
might be quite surprising since MCSMUS is slightly better than MUST in Fig. 2c.