On the run-time behaviour of stochastic local search algorithms for SAT

The notion of incompleteness for stochastic decision algorithms is refined by introducing the notion of "probabilistic asymptotic completeness" (PAC) and it is proved for a number of well-known SLS algorithms whether or not they have this property.

Abstract

Stochastic local search (SLS) algorithms for the propositional satisfiability problem (SAT) have been successfully applied to solve suitably encoded search problems from various domains. One drawback of these algorithms is that they are usually incomplete. We refine the notion of incompleteness for stochastic decision algorithms by introducing the notion of "probabilistic asymptotic completeness" (PAC) and prove for a number of well-known SLS algorithms whether or not they have this property. We also give evidence for the practical impact of the PAC property and show how to achieve the PAC property and significantly improved performance in practice for some of the most powerful SLS algorithms for SAT, using a simple and general technique called "random walk extension". Introduction Stochastic local search (SLS) algorithms for the propositional satisfiability problem (SAT) have attracted considerable attention within the AI community over the past few years. They belong t...