The SAT community, and hence the SMT community, have substantial experience in benchmarking solvers against each other on large sample sets, and publishing summaries, whereas the computer algebra community tends to time solvers on a small set of problems, and publishing individual times. This paper aims to document the SAT community practice for the bene t of the computer algebra community.
0 0.01 base-newrw-strict-tan-msat base-newrw-strict-tan-cvc4 base-newrw-strict-tan-yices
base-newrw-strict-tan-z3 base-newrw-strict-tan-best 10 time 0.1 1 100 1000 10000 1 \Cactus" or \Survival" plots
1. For each method separately (a) Solve each problem pi, noting the time ti (up to some threshold T ). (b) Sort the ti into increasing order (discarding the time-out ones). (c) Plot the points (t1; 1), (t1 + t2; 2) etc., and in general (Pk i=1 ti; k). 2. Place all the plots on the same axes, optionally (as in Figure 1) using a logarithmic scale for time.
N.B. There is therefore no guarantee that the same problems were used to produce time results from di erent solvers.
From 1 we can deduce that, up to 100 seconds, the solvers are pretty similar, and with a time budget of 100 seconds, can solve at most around 500 problems. At a time budget of 1000 seconds, the di erences are more marked, and the worst solved around 1600 problems and the best around 2000. 2 3
An alternative is (still after sorting the ti) to plot (t1; 1), (t2; 2) etc., and in general (tk; k). If we normalise the y axis to [0; 1] (not discarding the timeouts) we have an approximation to the cumulative distribution function. See [7] for some examples. Hence from these plots we can ask questions like \what is the probability of solving a random problem in t seconds". Though not shown in Figure 1, the SAT competition has taken to including a "virtual best solver" (VBS) which is synthesised from the other results by taking the minimum (across all solvers tested) time taken to solve every given benchmark. Thus the VBS time is always equal to the time of some real solver, but which one will change by the benchmark (measuring how often each solver is the VBS is also an interesting metric). The VBS can be added to the survivor/cactus plot to get a feeling for the variability between solvers. In particular, if it tracks one solver, then that is close to being the best, whereas if it does signi cantly better than any individual solver, that is an indication that the di erent real solvers have di erent strengths and weaknesses, and a portfolio approach might be appropriate. See Section 8.
We have therefore added this to our solvers on the diagrams, and counted how often a solver
is the VBS. A variation on counting is provided by [
hwmcc15/Biere-HWMCC15-talk.pdf, exept that these aren't cumulative, i.e. (k; tk) was plotted.
but in a di erent place. One could consider scoring \VBS points": 1 if VBS, 0 if more than 5% slower2 than VBS, and linear interpolation in between. 4
One of the e ects of having a solution process whose running time is widely variable3 is that one
may well not be best served by just running the process to termination. In the case of a single
processor, this issue was considered by [
This is in fact the default behaviour in MiniSAT 2.2.0, where it is known as Luby (though T is in fact measured in terms of con icts rather than time, and it's not a complete restart that is performed, as certain learned clauses are kept).
These days, with processors getting more numerous rather than faster, we might consider running multiple copies in parallel. To see how this might help, consider the trivial case of a process whose running time is 1; K; K2 with equal probability. Then the average time to solution is 13 (1 + K + K2) = 37 when K = 10. Running two copies and aborting the other when one nds the solution has an average time to solution of 19 (5 + 3K + K2) = 15 when K = 10, so the CPU cost is 30 units, still less than the sequential cost. Similarly, three copies gives 217 (19 + 7K + K2) = 7 when K = 10, so the CPU cost is 21 units, even better. For K = 10, the minimum is achieved at 8-fold parallelism, with time-to-solution 1.36 units, and a CPU cost of 10.9 units.
The break even point for two-fold parallel running is K = 12 1 + p37 4:5, and three-fold running is K = 4. It is worth noting, though, that a single Luby process with T = 13 (to avoid T = 1 getting lucky) achieves an average time to solution (and cost) of 9. 5 5.1
Normal Distribution of Times It is far from clear what sort of distribution the running times of SAT, and even less SMT, solvers have, but it would be foolish to ignore the normal distribution. We took 36 hypothetical cases, with 9 di erent running times t0 = 1; : : : ; 9, and standard deviations t0=10; 2t0=10; 3t0=10; 4t0=10 for each running time. The mean running times roughly mimic the fact that a benchmark suite will have problems of a range of di culties (indeed, we may have underplayed the range). Some problems seem to be more variable than others,but we have no real justi cation for the scale of standard deviations.
We used ve (hypothetical) possible solvers. The base line one just took a time t at random from the relevant normal distribution: t 2 N (t0; kt0=10). The second one ran two copies in parallel, terminating when the rst one did, the third ran three copies, and the next two 10 and 20. In this case, the VBS is in fact the equivalent of running 36 copies. The data are in Figure 2A percentage-based approach is probably more appropriate than a xed time, as di erences in time tend to come from consistent features. But this could also do with more experimentation.
the di erent elds. In Symbolic Computation, most Las Vegas algorithms are ones that normally produce the answer in a deterministically-bounded time, but may occcasionally fail and have to try again, and e ort goes into bounding the error probability, and proving that the algorithm will terminate. Modular algorithms are a classic example. But here we are considering algorithms whose running time is intrinsically variable. 2. Note that we are not charging twice for the cost of running two copies, i.e. we are looking at \time to solution" not \cost of solution"
It is also not clear whether we should assume t or log t is normally distributed. Hence we re-ran these experiments, but applied the normal distribution in log t-space. The standard deviation was scaled so that it bore the same ratio to the mean as before, i.e. log = log , where and represent the mean and standard deviation. Again, the VBS is in fact the equivalent of running 36 copies. The data are in Figure 3. We note that the left-hand gures look almost identical, but the right-hand (semi-log plot) ones show a distinct di erence at the lower end. 5.2
Uniform Distribution of Times We then considered uniform distributions, with the lower bounds being t0 = 1; : : : ; 10, and the upper bounds being 10 times that. We used the same hypothetical solvers as before. The data are in Figure 4.
Again, one could say that we should be uniform in log(t), and we did these computations. The data are in Figure 5. It might seem from these that running twice and running thrice were very similar, and in fact that running twice was almost half the time of running once, thus meaning that they were almost equivalent in cost. In fact, this model is susceptible to algebraic treatment, and the formulae (running from 1 to B seconds, with numeric values for B = 10) are as follows: once twice thrice = = =
6 (log B)3 B
B 1 (log2B)2 (B log(Blog B + 1)) ( 21 log B + log B + 1) 3:9087 2:5264 1:9887 Hence in fact the \running thrice" number is approximately correct, at one-half the elapsed time of running once.
6
6
For the rst three tests we used a vector of baseline times (notionally in seconds) of cat(2,[1.1:0.002:2],[2:1:50],[50:5:300]); in MatLab speak, i.e. 1.1 to 2 in steps of 0.002, 2 to 50 in step of 1, and 50 to 300 in steps of 5. 6.1
Predictable We rst measure four solvers: baseline, baseline less 1 second, 40% of baseline and a hybrid of 70% of (baseline less 0.5 seconds). The results are shown in Figure 6. \1 second shorter" was quickest 284 times, and \60% faster" 267 times. However, \60% faster" took 48.3 seconds longer than the Virtual Best (which took 4311 seconds),\1 second shorter" 6036 seconds longer, hybrid 3125 seconds longer and the baseline 6572 seconds longer. 6.2
Predictable plus Fuzz What happens if we multiply each time by a random variable, uniform in [0.8,1.2]? 40 runs of this experiment give a mean VBS time of 4299 seconds, with a standard deviation of 53.455. In the counts of how often each solver was VBS, hybrid appeared, showing up between 5 and 17 times, with corresponding adjustments to the others. \1 second shorter" was always the most common, with the ratio of it over \60% faster" ranging from 1.09 to 1.34. The plots (linear and semilogx) are in Figure 7. 6.3
Predictable plus Random To the previous solvers, we add a \joker", that, on one problem in 10, takes 10% as long as the baseline. The results are shown in Figure 8. The joker was quickest 55 times, \1 second shorter" was quickest 256 times, and \60% faster" 240 times. The time di erences are that \60% faster" took 402 seconds longer than the Virtual Best, \1 second shorter" 6390 seconds, hybrid 3479 seconds, the joker 5865 seconds and the baseline 6941 seconds. 6.4
Judgement The data used so far had 500 \fast" problems (< 2 seconds), 50 \medium" (between 2 and 50) and 5 hard (over 50). What happens if, instead, we have equal numbers in each bracket. The results from this, otherwise using the same methodology as section 6.3, are in Figure 9: the reader can see the di erence from Figure 8: the current gure is dominated by the slow problems. The joker was quickest 593 times, \1 second shorter" was quickest 256 times, and \60% faster" 5084 times. 7
Scatter plots are used to compare pairs of solvers. For each benchmark you plot (sometimes using di erent colours or marks for SAT and UNSAT) a point with x location the time taken by solver 1 and y the time taken by solver 2. To make things easier to follow, people commonly add the diagonal (sometimes annotated with "solver 1 is faster" and "solver 2 is faster" on the relevant sides / corners) and the time-out lines. An example is shown in Figure 10, from which one might reasonably conclude that Solver 1 is typically 10 times slower than Solver 2, and that 8
This section is drawn from Florian Schanda's joint work with Martin Brain, and the authors are very grateful to him for permission to include the slides. Figure 11 is a standard tabular presentation of the summary numerical data from his benchmarking. From this one can certainly deduce that Z3 is slightly more often the winner in terms of %age of problems solved in each category. On the Schanda set (Figure 12), Z3 is the winner, but Colibri is faster while it's in the race. The virtual best solver has a surprisingly good performance, remaining almost at much longer than Colibri, and solving signi cantly more than any individual solver.
Nevertheless, Z3 is not a winner on the Griggio set, and this is clearly shown in Figure 13. Also shown here is the fact the the Virtual Best Solver, while tracking Colibri closely, solves a few more. 9
The SAT community has had substantial experience in measuring, and comparing, solvers whom
time is intrinsically variable, and where selective publication of results could be used to justify
almost every conclusion: for example selection from the data underpinning Figure 10 could
justify anything from \On UNSAT examples, Solver 1 is comparable to Solver 2", to \Solver
2 is thousands of times faster than Solver 1". If the computer algebra community is to move
from publication of a small set of results to more objective comparisons, it will need to develop:
signi cant collections of curated4 problem sets, available in a common machine-readable
format5, as DIMACS [6] and SMT-LIB [
Acknowledgements: The authors are supported by the European Union's Horizon 2020 research and innovation programme under grant agreement No H2020-FETOPEN-2015-CSA 712689 (SC2).
Supporting Data are available at 10.5281/zenodo.896016. [6] I. Spence. Weakening Cardinality Constraints Creates Harder Satis ability Benchmarks. J. Exp.
Algorithmics Article 1.4, 20, 2015. [7] L. Xu, F. Hutter, H.H. Hoos, and K. Leyton-Brown. SATzilla: Portfolio-based Algorithm Selection for SAT. Journal of Arti cial Intelligence Research, 32:565{606, 2008.
unsatisfiable satisfiable 0.1 1 Sol1ve0r 1 100 Figure 10: Scatter Plot Example. Benchmarks With status ‘solved’
Benchmark Schanda Griggio Heizmann Industrial 2 Industrial 2 qf NyxBrain PyMPF SPARK FP SPARK ALL SPARK QF FP Wintersteiger
Summary 19 CVC4 IEEE-754 implementation
A P
F FAlt-iEgrgoure 11C:olibNriumeriCVcC4a(Fl) DataMafthoSArT \ReaCVlC4L(R)ife" t s e Virtualb 50 s 40 s 30 s e m i t 20 s 10 s 0 s 50 s 40 s 25 50
75 100 125 150 175 instances solved