the cutoff by a small subset of strategies, making this data set harder as a suboptimal selection is likely to lead to a timeout.

## 5 Conclusions And Future Work

Restart strategies have an important role in the success of DPLL style SAT solvers. The performance of different strategies varies over different benchmark families. We harness machine learning to enhance the performance of SAT solvers.

We have presented *LMPick***, a technique that uses both satisfiability classification**
and solver runtime estimation to pick promising restart strategies for instances.

We have demonstrated the effectiveness of *LMPick* **and compared its results**
with the most commonly used restart strategies. We have established that in many cases *LMPick* **outperforms any single restart strategy and that it is never**
worse than a randomly picked strategy. We have also discussed the **influence of**
different components of *LMPick* **on its performance.**
While universal restart strategies are more commonly used than dynamic ones, dynamic strategies are getting more attention lately. An interesting continuation to this work would be to use machine learning to develop a fully dynamic restart strategy. Such a strategy could use unsupervised machine learning algorithm to develop a dynamic restart policy for a benchmark family of problems.

Restart strategies are not the only aspect of SAT solving influencing performance on different benchmark families. Machine learning can be also used to tune other parameters that govern the behavior of modern DPLL **based solvers,** namely, parameters that are commonly set manually as a result of a trial and error process, such as decision heuristic parameters, clause deletion policy, etc.

## Acknowledgements

NICTA is funded by the Department of Broadband, Communications **and the** Digial Economy, and the ARC through Backing Australia's Ability and the ICT Centre of Excellence program.

## References

1. Biere, A.: Adaptive Restart Strategies for Conflict Driven SAT Solvers. Proc. of the 11th Int. Conf. on Theory and Applications of Satisfiability **Testing (2008)**
2. Biere, A.: PicoSAT Essentials. Journal on Satisfiability, Boolean Modeling and Computation, 4:75-97 (2008)
3. Bregman, D., Mitchell, D.: The SAT solver MXC (version 0.75). Solver Description for the SAT Race 2008 solver competition (2008)
4. Devlin, D., O'Sullivan, B.: Satisfiability as a Classification Problem. Proc. of the 19th Irish Conf. on Artificial Intelligence and Cognitive Science (2008)
5. E´en, N., S¨orensson, N.: An extensible SAT-solver. Proc. of the 6th Int. Conf. on Theory and Applications of Satisfiability Testing (2003)