Randomization and Restart Strategies.
MMath thesis, University of Waterloo, School of Computer Science, 2006.
The running time for solving constraint satisfaction problems (CSP) and propositional satisfiability problems (SAT) using systematic backtracking search has been shown to exhibit great variability. Randomization and restarts is an effective technique for reducing such variability to achieve better expected performance. Several restart strategies have been proposed and studied in previous work and show differing degrees of empirical effectiveness.
The first topic in this thesis is the extension of analytical results on restart strategies through the introduction of physically based assumptions. In particular, we study the performance of two of the restart strategies on a class of heavy tail distribution that has been used to model running time. We show that the geometric strategy provably removes heavy tail of the Pareto form. We also examine several factors that arise during implementation and their effects on existing restart strategies.
The second topic concerns the development of a new hybrid restart strategy in a realistic problem setting. Our work adapts the existing general approach on dynamic strategy but implements more sophisticated machine learning techniques. The resulting hybrid strategy shows superior performance compared to existing static strategies and an improved robustness.