A typical challenge faced when developing a parametrized solver is to evaluate a set of strategies over a set of benchmarking problems. When the set of strategies is large, the evaluation is often done with a restricted time limit and/or on a smaller subset of problems in order to estimate the quality of the strategies in a reasonable time. Firstly, considering the standard SMT-LIB benchmarks, we ask the question how much the time evaluation limit and benchmark size can be restricted to still obtain reasonable performance results. Furthermore, we propose a method to construct a benchmark characteristic subset which faithfully characterizes all benchmark problems. To achieve this, we collect problem performance statistics and employ clustering methods. We evaluate the quality of our benchmark characteristic subsets on the task of the best cover construction, and we compare the results with randomly selected benchmark subsets. We show that our method achieves smaller relative error than random problem selection.
Optimizing the performance of a Satisfiability Modulo Theories (SMT) solver, like CVC4 [
Within a large problem library, one can expect a large number of syntactically similar problems or problems with similar performance with respect to many strategies. Identification of similar problems could help us to speed up the evaluation, as we can select a single representative from each similarity class. To identify classes of similar problems, we propose to perform short evaluation runs of several CVC4 strategies and to collect run-time statistics. Then, problems with similar statistics might be considered similar. To evaluate this approach, we experiment with the best cover construction, that is, a selection of strategies with the best performance on a given set of problems. We construct the best cover on a smaller benchmark subset and we compare its performance with the optimal cover constructed on all problems. This gives us a quality measure of problem subset selection.
The paper is structured as follows. Section 2 describes the proposed method of identification of similar problems based on performance statistics, and how to construct a benchmark characteristic subset. Section 3 describes the best cover construction task which is used for empirical evaluation of the quality of constructed subsets in Section 4. We conclude in Section 5.
Restricting the evaluation of a solver to a smaller random subset of all benchmark problems
is a common and efective method used by developers. Considering a large set of benchmark
problems, like the SMT-LIB library [
Clustering algorithms [
To employ clustering algorithms, the entities, in our case benchmark problems, need to be
represented by numeric feature vectors. We could create the feature vectors from the syntactic
structure of problems, similarly to ENIGMA [
1We run CVC4 with argument –rlimit=10000 to limit the resources (roughly the number of SAT conflicts).
Once the performance feature vectors for all benchmark problems are constructed, we employ
the -means [
The above gives us the following method for the construction of the benchmark characteristic set. We construct the performance feature vectors for all benchmark problems by extracting runtime statistics from short probing solver runs. As diferent features might have values of diferent units, we normalize the vectors by dividing each feature by the standard deviation across all feature values. Then we employ the -means algorithm and construct problem clusters and their centroids. From each cluster, we select the problem whose performance feature vector is the closest to the cluster centroid. Thusly selected problems form the benchmark characteristic subset of size .
To evaluate the quality of the benchmark characteristic subsets from Section 2, we consider the task of the best cover construction. Let be the set of benchmark problems and let be a set of strategies. Suppose we evaluate all strategies over problems . The coverage of over , denoted coverage(S,P), is the count of problems solved by strategies .
coverage(S,P) = ⃒⃒⃒ ⋃︁ { ∈ : strategy solves problem }⃒⃒⃒
∈ The best cover of strategies over of size is the subset of 0 ⊆ with |0| ≤ and with the highest possible coverage(0, ).
Suppose we construct the best cover 0 ⊆ based only on a partial evaluation of strategies over a subset 0 of problems . This is typically done when the set of strategies and the set of problems are large. We can then compare the performance of the best cover constructed on 0 with the optimal performance of the best cover constructed with the full evaluation over . The performance of the two covers should be similar, if 0 faithfully characterizes . More formally, let us fix strategies and the cover size . Let 0 be the best cover over 0 and let best be the best cover over . We will measure the diference between their coverages coverage(0, ) and coverage(best, ) over all problems . We usually do not have all strategies evaluated over all problems, but for the sake of the evaluation in this paper we shall compute them.
We consider two methods to construct the best covers. First, an approximative but fast method called greedy cover (Section 3.1). Second, an exact but a bit slower best cover construction using an ILP solver (Section 3.2). 1 Function greedy( , , )
Input : set of problems , set of strategies , size
Output : a subset of of size approximating the best cover 2 ← ∅ 3 while || < and ((∃ ∈ )(∃ ∈ ) : strategy s solves problem p) do 4 for ∈ do // compute the problems solved by each strategy ∈ 5 ← { ∈ : strategy solves problem } argmax∈ (||) ∖ ∪ {} // obtain the best strategy on current problems
// remove the problems solved by . . .
Algorithm 1: Greedy cover algorithm.
The greedy cover algorithm is an approximative method for the construction of the best cover of strategies over problems of size . The algorithm greedy(P,S,n) (see Algorithm 1) proceeds as follows. It starts with an empty cover and it finds the strategy ∈ which solves most problems from . The strategy is added to and the problems solved by are removed from . This process is iteratively repeated until reaches the desired size or no strategy can solve any of the remaining problems.
We will measure the relative error of constructing the greedy cover (of size ) by a partial evaluation of strategies over a subset 0 of all problems using the standard formula below. The experimental evaluation of greedy cover construction on random subsets and on benchmark characteristic subsets based on performance features is given in Section 4.
⃒ error(0,n) = 100 · ⃒⃒ 1 − coverage(greedy(0,,n),P) ⃒
⃒ coverage(greedy( ,,n),P) ⃒
Apart from the approximative greedy cover construction, we also consider an exact best cover
construction method based on the representation of the best cover problem by an Integer Linear
Programming (ILP) formulation. The ILP problems are solved by the Gurobi solver [
We consider a maximal set cover formulation, i.e., without taking into account the solving time. This means that given a set of strategies , a set of solved problems by each strategy ∈ , and the size of the cover , the goal is to select a set of strategies ′ ⊆ with || = that maximizes the total number of instances solved, i.e., maximizing the cardinality of ⋃︀∈′ .
We remark that the exact cover maximization is typically only slightly better than the greedy cover. However, interestingly, Gurobi has proven to be extremely eficient on these problems; typically we observe solving times around 1 s.
In this section, we describe the experimental setup in Section 4.1. We experiment with the best cover construction of random benchmark subsets in Section 4.2. In Section 4.3, we discuss reasonable restrictions of the evaluation time limit. Mainly, in Section 4.4, we evaluate the quality of benchmark characteristic subsets constructed using performance features and the -means clustering method introduced in Section 2.
For our experiments, we consider the quantified fragment of the SMT-LIB library [
Figure 1 graphically depicts benchmark problem properties. The bar graph on the left shows
the count of problems from diferent logics. The plot on the right visualizes the performance
feature vectors of the problems described in Section 2. The plot is produced by dimensionality
reduction to 2 dimensions by the t-SNE [
In this section, we present an experiment on the best cover construction on randomly selected subsets of benchmark problems. From all 75814 benchmark problems, we construct random subsets of diferent sizes, ranging from 100 up to 75800 with step 100. Moreover, we construct 10 diferent collections of these subsets to measure the efect of random selection. On every benchmark subset, we construct the greedy and exact covers of the 14 diferent strategies, called validation strategies (see Section 4.1). We construct covers of diferent sizes ( ∈ {1, 2, . . . , 10}). We evaluate the constructed covers on all benchmark problems and we measure the error as described in Section 3.1 and Section 3.2.
Figure 2 presents the error for the greedy cover (left) and exact cover (right) construction. For every random subset size, we plot the worst case error (red solid line), and the average error (dotted line). Given 10 random subset collections and 10 diferent cover sizes, each value is computed from 100 relative error values.
We can see that with benchmark subsets bigger than 1000 problems (roughly 1.3% of benchmark problems), we obtain less than 2% error even in the worst case. With subsets bigger than 10000, the worst case error drops below 0.5%. From the relatively big diference between the worst case and the average, we can conclude that the accuracy of the benchmark approximation by a random subset depends considerably on the coincidence of random selection. In Section 4.4 we show that performance features can help us reduce this dependence by constructing better benchmark characteristic problems.
In this section, we present basic statistics on the solver runtime. In particular, we are interested in how many problems are solved with a decreased evaluation time limit. This information can help developers to set time limits for evaluation experiments.
For each of the 24 considered strategies, we measure how many problems are solved in the -th second, that is, the count of problems solved with runtime between − 1 and . Figure 3 shows the results for two representative strategies, namely, the strategy that solves the most problems in the first second (left) and the strategy that solves the most problems with runtime greater than 1 second. The corresponding strategies (cvc1 and cvc16) can be found in Appendix B.
From Figure 3, we can see that the majority of problems are solved within the first second of runtime, and this is the case with all evaluated strategies. Note the logarithmic -axis in the figure. We have conducted experiments with greedy cover construction, similar to the experiments in Section 4.2. The experiments show that the greedy cover constructed with the evaluation restricted to the time limit of 1 second shows less than 0.25% error, when compared with greedy covers constructed with the full time limit of 60 seconds. With the time limit of 10 seconds, we reach the error less than 0.15% and with the limit of 30 seconds the error drops below 0.05%.
In this section, we evaluate the quality of benchmark characteristic subsets constructed with performance features and -means clustering from Section 2. We compare the relative error of the construction of the best covers on benchmark characteristic subsets and on random benchmark subsets. Out of the 24 strategies considered in this experiment (see Section 4.1), we use 10 CVC4 strategies to construct the performance features of benchmark problems. We use only the remaining 14 strategies to construct the best covers to provide an independent validation set of strategies.
The performance features are computed by short CVC4 runs with limited resources as described in Section 2. Computing the performance features took less than 2 hours. We construct benchmark characteristic subsets3 of diferent sizes corresponding to the sizes of 3We use scipy.org’s implementation of -means, namely function scipy.cluster.vq.kmeans2 with parameter minit set to points. random benchmark subsets from Section 4.2. In this case, however, we do not construct 10 diferent collections but only one subset for each size. On the benchmark characteristic subsets, we compute both greedy and exact covers of diferent sizes ( ∈ {1, 2, . . . , 10}), and we measure the relative error as in Section 4.2.
Figure 4 presents the worst case relative errors for greedy cover (left) and exact cover (right) constructions. The red lines correspond to the relative error on random benchmark subsets, that is, they correspond to the red lines from Figure 2, but this time the results are computed only on the 14 validation strategies. The blue lines correspond to relative errors on the benchmark characteristic subsets. We can see that in both cases, the relative errors on the benchmark characteristic subsets are significantly lower, especially for smaller benchmark subsets. Even with the smallest subset of size 100, we get almost 2% worst case error. Moreover, from size 600 we obtain the worst case error below 1%. Furthermore, the error on benchmark characteristic subsets approaches the average error on random subsets (see the dotted lines in Figure 2). This suggests that the construction of benchmark characteristic subsets is less coincidental than random selection.
We propose and evaluate a method of constructing a benchmark characteristic subset that represents the whole benchmark. We provide empirical evidence that our method, based on clustering of problem performance feature vectors, gives better results than a random benchmark sampling. To evaluate our method, we use the task of best cover construction. However, we believe that our method shall prove useful for many other tasks. Furthermore, we provide an experimental evaluation of how restricting the benchmark size and evaluation time limits afect the solver performance. The characteristic subsets of quantified problems from SMT-LIB library computed using the -means clustering method are available for download. Hence SMT users can directly benefit from the results published in this paper by speeding up their solver evaluation.
As future work, we would like to experiment with diferent methods of measuring the quality of benchmark characteristic subsets, other than the best cover construction. Moreover, we would like to employ diferent clustering algorithms than -means. Finally, we would like to propose diferent methods of constructing problem characteristic feature vectors, for example, extracting features directly from the problem syntax.
The results were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902, and by the ERC Project SMART Starting Grant no. 714034. This scientific article is part of the RICAIP project that has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement no. 857306.
We use the following statistic keys, obtained by running CVC4 with option -stats, to construct problem performance feature vectors. sat::conflicts sat::decisions Instantiate::Instantiations_Total SharedTermsDatabase::termsCount resource::PreprocessStep resource::RewriteStep resource::resourceUnitsUsed
The following 23 CVC4 strategies, described as CVC4 command line arguments, are used in the experiments. The 24th strategy is Z3 in the default mode. The first ten {cvc1, . . . , cvc10} are used to construct the performance feature vectors of problems. The remaining 14 are used as validation strategies. –simplification=none –full-saturate-quant –no-e-matching –full-saturate-quant –relevant-triggers –full-saturate-quant –trigger-sel=max –full-saturate-quant –multi-trigger-when-single –full-saturate-quant –multi-trigger-when-single –multi-trigger-priority –full-saturate-quant –multi-trigger-cache –full-saturate-quant –no-multi-trigger-linear –full-saturate-quant –pre-skolem-quant –full-saturate-quant –inst-when=full –full-saturate-quant –no-e-matching –no-quant-cf –full-saturate-quant –full-saturate-quant –quant-ind –decision=internal –simplification=none –no-inst-no-entail \\ –no-quant-cf –full-saturate-quant –decision=internal –full-saturate-quant –term-db-mode=relevant –full-saturate-quant –fs-interleave –full-saturate-quant –finite-model-find –mbqi=none –finite-model-find –decision=internal –finite-model-find –macros-quant –macros-quant-mode=all –finite-model-find –uf-ss=no-minimal –finite-model-find –fmf-inst-engine –finite-model-find –decision=internal –full-saturate-quant