Irregular Behaviour in SLS Algorithms for SAT

by Holger H Hoos

Stochastic Local Search (SLS) algorithms, which are amongst the most effective approaches for solving hard and large propositional satisfiability (SAT) problems, 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. Furthermore, 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 GSAT with Random Walk or WalkSAT deviate substantially from exponential distributions. In this note, we study these deviations and present models and explanations for the irregular SLS behaviour. In particular, we show that the irregular RTDs can be modelled using mixtures of exponential distributions; we present evidence that such mixture distributions reflect stagnation behaviour in the search process caused by "traps" in the underlying search spaces; and we propose an extremely simple Markov chain model for the observed SLS behaviour.

Back to the LCI Forum page