# Online Estimation Of Sat Solving Runtime⋆

Shai Haim and Toby Walsh NICTA and UNSW
{shai.haim,toby.walsh}@nicta.com.au Abstract. **We present an online method for estimating the cost of solving SAT problems. Modern SAT solvers present several challenges to**
estimate search cost including non-chronological backtracking, learning and restarts. Our method uses a linear model trained on data gathered at the start of search. We show the effectiveness of this method using random and structured problems. We demonstrate that predictions made in early restarts can be used to improve later predictions. We also show that we can use such cost estimations to select a solver from a **portfolio.**

## 1 Introduction

Modern SAT solvers present several challenges for estimating their runtime. For instance, clause learning repeatedly changes the problem the solver faces. Estimation of the size of the search tree at any point should take into consideration the changes that future learning clauses will cause. As a second example, restarting generates a new search tree which again makes prediction hard. **Our approach**
to these problems is to use a machine learning based on-line method to **predict** the cost of the search by observing the solver's behaviour **at the start of search.**
Previous methods include the Weighted Backtrack Estimator, the Recursive Estimator ([5]) and the SAT Progress Bar ([6]) that do not support backjumping or restarts, and the BDD-based Satometer ([1]) which doesn't provide an estimate for the size of the decision tree. Machine learning has also been used to estimate search cost. Horovitz et al used a Bayesian approach **to classify CSP** and SAT problems according to their runtime [4]. Whilst this work is close to ours, there are some significant differences. For example, they used SATz-Rand which does not use clause learning. Xu et. al [9] used machine learning **to tune**
empirical hardness models [7]. The only non-static features used were generated by probes of DPLL and stochastic search. Their method gives an estimate for the distribution of runtimes and not, as here, an estimate for a specific run.

Finally, an online machine learning method has been used for QBF solvers [8].

## 2 Linear Model Prediction (Lmp)
