Abstract of Holger H. Hoos's PhD thesis
accepted by the Computer Science Department
of the Darmstadt University of Technology / Germany
Today, stochastic local search (SLS) algorithms belong to the standard methods for solving hard combinatorial problems from various areas of Artificial Intelligence and Operations Research. Some of the most successful and powerful algorithms for prominent problems like SAT (the Satisfiability Problem in Propositional Logic), CSP (the Constraint Satisfaction Problem), TSP (the Traveling Salesperson Problem), or QAP (the Quadratic Assignment Problem), are based on stochastic local search.
In this thesis we study various aspects of SLS algorithms, in particular we focus on modelling these algorithms, empirically evaluating their performance, characterising and improving their behaviour, and understanding the factors which influence their efficiency. We study these issues for the SAT problem in propositional logic as our primary application domain. SAT has the advantage of being conceptually very simple, which facilitates the design, implementation, and presentation of algorithms as well as their analysis. However, most of the methodology generalises easily to other combinatorial problems like CSP.
We develop a new model especially suited for representing and developing hybrid SLS algorithms and a new empirical methodology for evaluating the behaviour of Las Vegas algorithms (a super-class of SLS algorithms). The results we present include a comparative study of various popular SLS algorithms' performance over a broad range of SAT instances, some theoretical result on the approximate completeness of modern SLS algorithms for SAT, an empirical characterisation of SLS behaviour, and finally, an analysis of how different SAT-encoding strategies affect search space structure and, consequently, SLS performance.