Engineering stochastic local search for the satisfiability problem

Abstract

This thesis describes new algorithms for the Propositional Satisfiability Problem (SAT), a fundamental problem in theoretical and practical computer science. Besides the theoretical relevance of the SAT problem, many practical applications corroborate the importance of the SAT problem. Within this thesis, we provide different improvements for SLS solvers, and also propose new SLS solving techniques for the SAT problem. By means of empirical evaluations, we compare our solving methods with available state-of-the-art methods and show the superiority of the former. The results of our solvers within different SAT competitions further confirm their state-of-the-art performance. First, we propose a new technique to analyze the search behavior of an SLS solver. We show that this approach can be used to construct hybrid solvers that are able to exceed the performance of the SLS component. We present a new type of heuristic for SLS solvers based on the concept of probability distributions, which we implement in the solver Sparrow that reaches state-of-the-art performance on a wide range of randomly generated SAT problems. To improve the applicability of SLS solvers on structured problems, we analyze different preprocessing techniques in combination with the solver Sparrow. We are able to show that the performance of SLS solvers can be significantly improved on structured problems. Within our final study, we propose and analyze a solver based solely on probability distributions. Our new solver, named probSAT, allows a detailed analysis of the role of make and break for SLS solvers. Within comprehensive evaluations, we analyze probSAT on different SAT problems, and show that it establishes new state-of-the-art standards.

Finally we present an advanced framework for the empirical evaluation of algorithms, named EDACC, which provides a plethora of functionalities for the design, execution and analysis of experiments with all kind of algorithms.