Statistical Regimes and Runtime Prediction

1 Introduction

Modern combinatorial search solvers contain many elements that are stochastic in nature, such as randomised variable and value selection, tie breaking in heuristics, and random restarting. These elements add a degree of robustness to the solver. Nevertheless, this stochasticity results in variations in runtime between repeated runs of the solver, a fact which is often not accounted for by users and practitioners in related fields. This paper illustrates the consequences that such assumptions can have when comparing solver performance.

One such field is that of solver portfolios [Gomes and Selman, 2001; Kotthoff, 2014], which have consolidated and advanced the state-of-the-art across a broad range of problem domains such as Constraint Programming (CP) [O'Mahony et al., 2008; Hurley et al., 2014], Satisfiability (SAT) [Xu et al., 2008; Kadioglu et al., 2010], MaxSAT [Ans´otegui et al., 2014], Planning [Seipp et al., 2015], and many more. Their effectiveness relies on the ability to identify the best solver for each individual instance. At its core, training a portfolio involves collecting the runtime performance of each solver on a collection of benchmarks. From this, machine learning techniques are used to choose amongst the solvers based on instance features. Existing work in this area has only considered a single sample of the solver runtime for each instance, and makes the assumption that the behaviour is consistent between repeated runs of the solver. However, as we will see, the performance of a solver can vary by many orders of magnitude between repeated runs. This behaviour is related to heavy-tailed distributions discovered by [Gomes et al., 2000].

In a related field, automated solver configuration tools [Hutter et al., 2011; Ans´otegui et al., 2009; Fitzgerald et al., 2014] have successfully been able to tune solvers to surpass their default configuration. Their effectiveness relies on obtaining consistent, representative performance data for a given parameterisation on a sample of input instances. Crucially, these methods will not typically make allowances for any stochastic behaviour in the underlying solvers.

Related to the above is the task of solver runtime prediction [Hutter et al., 2014]. This focuses on building an empirical hardness model to predict the performance of a solver based on instance specific features. This paper will demonstrate that state-of-the-art runtime prediction methods do not account for the stochastic aspect of solver runtime and as such can have a substantial effect on their accuracy.

Thus, the contributions of this paper are as follows:

• we demonstrate that dramatic runtime variations occur in practice and can alter the outcome of empirical comparisons, such as the annual SAT competitions,
• we show that runtime variation needs to be accounted for in fields such as solver runtime prediction, portfolios, and automated configuration,
• we conduct a large-scale empirical evaluation on over 10 years of industrial SAT instances consuming over 600 weeks of CPU-time, and
• we provide a statistical analysis that can be applied to compare the performance of solvers from a runtime distribution perspective.

Figure 1: Log-log plots showing the empirical runtime distribution of two instances from the application category at the 2014 SAT Competition. The three solvers are the top-ranked solvers from the competition and the vertical lines mark their observed runtime during the competition.

2 Runtime Variations in Practice

This section illustrates a deficiency of empirical comparisons based on a single run. Figure 1 shows the runtime distribution of the top three solvers [Biere, 2014; Alfonso and Manthey, 2014; Oh, 2014] on two industrial instances from the 2014 SAT Competition. Vertical lines mark the solver's observed runtime during the competition, and the other lines plot the survival function of the empirical runtime distribution over 100 runs. In Figure 1a, the solver SWDiA5BY solved the instance faster than Lingeling during the competition, however we can clearly deduce from the runtime distribution that over repeated runs there is a larger probability of SWDiA5BY having a longer runtime than Lingeling. In this instance, the runtime distribution shows a clear ranking of the solvers: Lingeling ≺ SWDiA5BY ≺ Riss BlackBox. In Figure 1b the distinction between solvers is not as pronounced. Interestingly, in the competition, SWDiA5BY is ranked as the fastest of the three solvers on this instance, however when you consider its runtime distribution, it is most likely to take the longest.

This exemplifies a critical flaw in this type of empirical evaluation that is often performed when comparing solvers, only a single sample of the solver's runtime is taken on each benchmark instance. The current evaluation metric used in the SAT Competition purely considers the number of instances solved within a specified timeout, and only uses runtimes in the case of ties. However, the runtime distribution can often span over the timeout value, thus affecting the number of instances solved. Section 4 will demonstrate the ramifications of this, showing that these three solvers could have been ranked in any permutation. However, first, Section 3 will present a more holistic, statistically-founded methodology which is lacking in current comparisons.

3 Expected Performance

We can model the performance of a solver on a set of benchmark instances as a random variable, doing so will allow us to define bounds on the possible outcomes. Let pi be the probability that instance i is solved within a given timeout. pi will be simply 0.0 or 1.0 if a single sample runtime is taken, or a continuous value if a solver is run multiple times on the same instance. Naturally, the accuracy of pi is proportional to the number of repeated runs performed.

Next, let Xi be a discrete random variable which takes the value 1 if instance i is solved within the timeout, 0 otherwise. The expected value of Xi is pi:

We can define a bound on the variation of Xi by taking the critical value for pi = 0.5; thus the standard deviation of Xi can be bounded by 1 2 :

If the benchmark set contains k instances, then the success rate S, or ratio of instances solved within the timeout, is simply the mean of the Xi variables over the k instances. This allows the definition of the expected value of S as being the mean over the pi values:

Finally, bounds on the variation and standard deviation of S can be defined:

Importantly, this means that even over repeated runs, the variation in the total number of instances solved is bounded by a function of the number of instances. This fact should be of great consequence to the designers of empirical comparisons.

4 SAT Competition 2014

This section will project the analysis of Section 3 onto one annual empirical solver comparison. Consider the top three solvers from the application category at 2014 SAT Competition, namely, Lingeling [Biere, 2014], SWDiA5BY5by [Oh, 2014], and Riss BlackBox [Alfonso and Manthey, 2014] which solved 231, 228, and 226 of the 300 instances in this category, respectively. Note that, like many other empirical competitions, only a single sample of the solver's runtime is taken during the evaluation and the scoring metric is purely based on the number of instances solved within the specified timeout. Using the equations of Section 3, we can postulate on possible outcomes and give upper-bounds on the variation that could occur in such empirical evaluations, this is presented in Table 1.

Given that the performance difference amongst the topranked solvers is so narrow, it is not unreasonable to suspect that the outcome could have been different if the competition was re-run. To assess the potential outcomes, each of the three solvers above were re-run 100 times on each of the 300 instances from the industrial/application category at the SAT Competition 2014. Since Lingeling is the only one of these solvers to support the ability to pass a random seed as input, we emulate the functionality across all solvers simply by shuffling the input instance: randomly renaming the variables, shuffling their order in each clause, and reordering the clauses. This preserves the same structure and semantics of the original instance but may result in the solver taking different paths in the solving process across runs. Note that it is common in the SAT Competition to re-use instances from previous years by performing this type of shuffling [Le Berre and Simon, 2004].

Performance data was collected on a cluster of Intel Xeon E5430 2.66Ghz processors running CentOS 6. The solvers were limited to 1 hour and 2GB of RAM per instance. All times are reported in CPU-time. Note that these experiments are run on different hardware to that used in the SAT Competition and used a shorter timeout due to the increased computational complexity. In total, 322 CPU-weeks were used to record the data.

Considering the observed runtime distributions across 100 runs, together with the analysis from Section 3, we can quantify more statistically well-founded outcomes to the SAT Competition; these are presented in Table 2. Additionally, we can derive 95% confidence bounds on the expected success rate if we assume it to be normally distributed; which we will see to be reasonable in Figure 2. Significantly, the 95% confidence bounds of the solvers overlap, and as such, any permutation of the ordering could be possible.

Figure 2 augments these results by visualising the distribution of the total number of instances solved by each solver across the runs. Their frequencies appear normally distributed but additional samples would be needed to verify this. Ordering by probability mass would rank the solvers SWDiA5BY ≺ Lingeling ≺ Riss BlackBox, consistent with the ranking from Table 2. Interestingly, this is a different ranking to that of the official competition.

Table 3 presents some more detailed statistics about the performance of the three solvers, only a sample of the 300 instances is presented due to space constraints. We list the runtime which was observed in the SAT Competition under the 'Comp.' column. Notice that for numerous instances where a solver recorded a timeout in the SAT Competition we also observe many timeouts across the runs, but critically, the solver may also solve the instance very quickly.

We observe dramatic variations in runtime, often more than three orders of magnitude between a solver's best and worse time on an instance. In numerous cases, on a single instance, a solver will timeout on a large proportion of the runs but conversely may solve the instance very quickly in other cases. This could be the critical difference between solved or unsolved in the competition setting. Given that the difference amongst the top ranked solvers in the SAT Competitions is typically only a handful of instances, this constitutes a significant observation.

5 State-of-the-art Runtime Prediction

The ability to predict the runtime of a solver is interesting from a number of perspectives. Solver designers can make use of it as an informative analytical tool and it frequently serves as a central component in solver portfolios and configuration tools. Often, these tools base their decisions on underlying runtime prediction models. The prediction target is the runtime of the solver on an instance, which has conventionally been collected by recording a single runtime. However this approach is flawed, since in reality we are dealing with solvers that exhibit a highly variable runtime distribution, a single value is simply not representative. This section highlights the detrimental effects that this fundamental flaw can have on state-of-the-art runtime prediction methods.

5.1 Log Transformation

The typical practice when predicting solver runtime is to logtransform the runtime in seconds [Hutter et al., 2014]. Error calculations on this, like root-mean-squared error and mean absolute error, will over-penalise runtimes of less than one second. Differences between runtimes of 0.01 seconds and 0.1 seconds are valued to the same extent as the difference between 10 and 100 seconds. These are all an order of magnitude different, but we argue that the first order of magnitude for runtimes should range from [0..9) seconds, the second from [9..99), and so on. Thus, the runtimes should be transformed as log(1 + runtime). This additionally eliminates the need to censor runtimes of zero seconds which would have been needed when performing the log transformation. For the predictions in this section we will use the adjusted logtransformed runtime, log10(1 + runtime).

5.2 Experimental Setup

The benchmark set comprises 1676 industrial instances from 9 years of the SAT Competitions, Races, and Challenges between 2002 and 2011. We use MiniSat 2.0 [E´en and S¨orensson, 2004] as the solver with a timeout of 1 hour and a limit of 2GB RAM. Performance data was collected on a cluster of Intel Xeon E5430 Processors (2.66GHz) running CentOS 6. A total of 315 weeks of CPU-time was consumed to accumulate this performance data. Table 4 presents a sample summary of the runtimes. The dataset is available at http://ucc.insight-centre.org/bhurley/

5.3 Predictive Fragility

To perform the regression we use a random forest with the same parameters as [Hutter et al., 2014], that is using 10 regression trees, using half of the variables as split variables at each node (perc = 0.5), a maximum of 5 data-points in leaf nodes (nmin = 5). This configuration was shown to be the most accurate for runtime prediction in comparison to ridge regression, neural networks, Gaussian processes, and individual regression trees. The random forest may choose from a set of 138 SAT features [Lin Xu and Leyton-Brown, 2012] which have been used for runtime prediction and many award winning portfolios. As per [Hutter et al., 2014] and other work on runtime prediction, we do not treat runs that timeout with any speciality, they are considered to just have taken the timeout value. We use a standard randomised 10fold cross-validation, where the dataset is split in 10 folds. Each of the folds takes a turn as the test set, with a model being built from the remaining 9 folds of training data. We use a standard error metric for regression, the root-mean-squared error (RMSE) from the predicted value to the true test value.

Some simple statistical values are extracted from the runtime distribution on each instance in order to model a range of scenarios which may arise using the current methodology, where it is possible for the models to be trained on completely different runtime samples to that considered in testing. Table 5 presents a set of these scenarios, highlighting the fragility in current state-of-the-art runtime prediction methods. Columns vary the target metric and rows vary the training sample. Within each column, values in italics highlight the best mean RMSE, bold values are those which produced predictions statistically significantly different (95% confidence) from this best.

The closest setting to current methodology is shown in the sample entries, this simply uses a random sample of the observed runtimes. The predictions produced by these models are reasonable but are not the most accurate. Unsurprisingly, the most accurate predictions typically arise when we are using the same sample statistic for both training and testing. For example, when aiming to predict the median runtime it is best to have used the median runtime of the training set instances, likewise for predicting the minimum and maximum runtimes.

Conversely, another setting, albeit the most extreme, is if the training data consists of the minimum value from each distribution and we are attempting to predict the maximum runtime. In this case, the runtime prediction values are off by one order of magnitude on average. Likewise for predicting the minimum runtime where the maximum is used as training.

It is clear, and should seem natural, that the origin of the training sample has a considerable impact on the outcome of the models, but surprisingly, this is not something which is considered in existing methodology.

6 RelatedWork

A large body of work in the SAT community has studied runtime variations when running deterministic backtracking algorithms on distributions of random instances, but also by repeated runs of randomised backtracking algorithms on individual instances. The Handbook of Satisfiability dedicates a chapter [Gomes and Sabharwal, 2009] to runtime variations in complete solvers, modelling them as complex physical phenomena. The chapter focuses on an analysis and prevention of extreme variations using the framework of fat- and heavy-tailed distributions.

[Gomes et al., 2000] first presented the heavy- and fattailed phenomenon in solver runtime. That paper was written during a time before randomised restarting was common and the fastest complete-search solvers for SAT were based on the DPLL method; modern SAT solvers have come a long way since. The paper also modified the algorithms to add an element of randomisation and a new heuristic equivalence parameter to increase its frequency. Our work has not modified the solvers in any way, we use the current state-of-the-art solvers. Nevertheless, it is evident that modern solvers have an element of stochasticity built in, resulting in runtime distributions with significant variance.

[Nikoli´c, 2010] formed a methodology for statistically comparing two solvers given observations from their runtime distributions. Our paper provides substantial additional evidence to support the need for such comparisons. [Van Gelder, 2011] proposes a new careful ranking method for competitions which addresses a number of issues with existing ranking methods, but the system is still based on individual runtime samples.

[Hutter et al., 2014] presents the state-of-the-art for solver runtime prediction, evaluating the effectiveness of a number of machine learning methods for runtime prediction across a wide range of SAT, MIP, and TSP benchmarks. Our comparison in Section 5 does not compare different models on their accuracy, but does question a fundamental assumption being made about the underlying runtime behaviour.

[Fawcett et al., 2014] tackles runtime predictions for stateof-the-art planners where they observe substantial runtime variations of planners across different domains. The authors propose new feature sets which improve the accuracy of predictions however the work does not consider runtime variations on individual instances, only a single sample runtime is taken.

[Leyton-Brown et al., 2002] identified features of combinatorial auction problems to predict the runtime of CPLEX on different distributions of instances, but only one sample runtime is taken despite elements of randomness in the solver.

7 Conclusions and Discussion

This paper questions a fundamental assumption being made about the runtime behaviour of complete search solvers. Modern solvers usually have some form of in-built randomness. As a consequence their runtime exhibit significant variation, sometimes by orders of magnitudes on individual instances. We have shown that the outcome of empirical comparisons such as the SAT Competitions can fluctuate simply by re-running the experiments, and we provide statistical bounds on such variations. We also project the fragility of state-of-the-art runtime prediction methods to these runtime distributions, showing that it is insufficient to take a single sample of the runtime in the current practice. Such observations have broad reaching implications for empirical comparisons in a number of fields, solver analysis, portfolios, automated configuration, and runtime prediction.

There may not be a single solution that should be applied to overcome this phenomenon, but rather a context dependant approach should be taken. For empirical evaluations, solvers should be compared based on their runtime distributions. Statistical tests such as the Kolmogorov-Smirnov or chi-squared tests would be applicable. Of course, this increases the computational cost but gives the advantage of more authoritative conclusions. One related question concerns the appropriate number of runtime samples required to obtain representative results.

For the fields of runtime prediction, solver portfolios, and automated configurators, there remains a great number of open questions. It is simply insufficient to take a single sample of a solver's runtime as ground-truths. Alternatively we should consider predicting statistics or parameters of the runtime distribution. Depending on the application we may attempt to maximise the probability of solving an instance within a certain time, we may prefer solvers which give more consistent behaviour, or conversely a solver which varies dramatically in the hope that we may get lucky. Additionally, in a parallel setting this would have knock-on effects. There are many avenues for future study in these areas.

Acknowledgments

This work is supported by Science Foundation Ireland (SFI) Grant 10/IN.1/I3032 and FP7 FET-Open Grant 284715. The Insight Centre for Data Analytics is supported by SFI Grant SFI/12/RC/2289. We would like to thank Nic Wilson for his valuable contributions to Section 3.