Ensemble-based prediction of SAT search behaviour

Before attempting to solve an instance of the satisfiability problem, what can we ascertain about the instance at hand and how can we put that information to use when selecting and tuning a SAT algorithm to solve the instance? We argue for an ensemble-based approach and describe an illustrative example of how such a methodology can be applied to determine optimal restart cutoff points for systematic, backtracking search procedures for SAT. We discuss the methodology and indicate how it can be applied to evaluate such strategies as restarts, algorithm comparison, randomization and portfolios of algorithms.