A Mixture-Model for the Behaviour of SLS Algorithms for SAT

Stochastic Local Search (SLS) algorithms are amongst the most effective approaches for solving hard and large propositional satisfiability (SAT) problems. Prominent and successful SLS algorithms for SAT, including many members of the WalkSAT and GSAT families of algorithms, tend to show highly regular behaviour when applied to hard SAT instances: The run-time distributions (RTDs) of these algorithms are closely approximated by exponential distributions. The deeper reasons for this regular behaviour are, however, essentially unknown. In this study we show that there are hard problem instances, e.g., from the phase transition region of the widely studied class of Uniform Random 3-SAT instances, for which the RTDs for well-known SLS algorithms such as GWSAT or WalkSAT/SKC deviate substantially fro