Threshold behaviour of WalkSAT and focused Metropolis search on random 3-satisfiability

Reference:

Sakari Seitz, Mikko Alava, and Pekka Orponen. Threshold behaviour of WalkSAT and focused Metropolis search on random 3-satisfiability. In F. Bacchus and T. Walsh, editors, Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT'05, St. Andrews, Scotland, June 2005), volume 3569 of Lecture Notes in Computer Science, pages 475–481, Berlin Heidelberg, 2005. Springer-Verlag.

Abstract:

An important heuristic in local search algorithms for Satisfiability is em focusing, i.e. restricting the selection of flipped variables to those appearing in presently unsatisfied clauses. We consider the behaviour on large randomly generated 3-SAT instances of two focused solution methods: WalkSAT and Focused Metropolis Search. The algorithms turn out to have qualitatively quite similar behaviour. Both are sensitive to the proper choice of their ``noise'' and ``temperature'' parameters, but with appropriately chosen values, both achieve solution times that scale linearly in the number of variables even for clauses-to-variables ratios . This is much closer to the satisfiability transition threshold than has generally been assumed possible for local search algorithms.

Keywords:

satisfiability, local search, phase transition, WalkSAT, Metropolis algorithm

Suggested BibTeX entry:

@inproceedings{SeAO05,
    address = {Berlin Heidelberg},
    author = {Sakari Seitz and Mikko Alava and Pekka Orponen},
    booktitle = {Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT'05, St. Andrews, Scotland, June 2005)},
    editor = {F. Bacchus and T. Walsh},
    pages = {475--481},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
    title = {Threshold behaviour of {W}alk{SAT} and focused {M}etropolis search on random 3-satisfiability},
    volume = {3569},
    year = {2005},
}