Statistical Regimes and Runtime Prediction

The last decade has seen a growing interest in solver portfolios, automated solver configuration, and runtime prediction methods. At their core, these methods rely on a deterministic, consis-tent behaviour from the underlying algorithms and solvers. However, modern state-of-the-art solvers have elements of stochasticity built in such as ran-domised variable and value selection, tie-breaking, and randomised restarting. Such features can elicit dramatic variations in the overall performance be-tween repeated runs of the solver, often by several orders of magnitude. Despite the success of the aforementioned fields, such performance variations in the underlying solvers have largely been ignored. Supported by a large-scale empirical study employ-ing many years of industrial SAT Competition in-stances including repeated runs, we present statisti-cal and empirical evidence that such a performance variation phenomenon necessitates a change in the evaluation of portfolio, runtime prediction, and au-tomated configuration methods. In addition, we demonstrate that this phenomenon can have a sig-nificant impact on empirical solver competitions. Specifically, we show that the top three solvers from the 2014 SAT Competition could have been ranked in any permutation. These findings demon-strate the need for more statistically well-founded regimes in empirical evaluations.