Runtime estimation of backtracking satisfiability solvers: a machine learning approach

The Boolean Satisfiability Problem (SAT) is a prominent problem in theoretical computer science. While there is currently no known worst case polynomial bound for it, in practice, many computations terminate quickly. However, the runtime variance is large. In recent years, satisfiability solvers have advanced to the point where they can be competitively used for industrial purposes. Nevertheless, the field of empirical estimation of SAT runtime has not received much attention to date. In this dissertation we present a technique for runtime estimation for complete SAT solvers which uses a machine learning based approach. This technique uses data about the satisfiability testing process which are gathered both offline and online. Through experimentation conducted with different datasets, we present results which demonstrate that the proposed technique can effectively estimate the cost of satisfiability testing very early in the process. We further present a method for using this technique in order to tune the behaviour of SAT solvers for better performance