@inproceedings{
    SeAO05,
    editor = "Bacchus, F. and Walsh, T.",
    author = "Seitz, Sakari and Alava, Mikko and Orponen, Pekka",
    volume = "3569",
    title = "Threshold behaviour of {W}alk{SAT} and focused {M}etropolis search on random 3-satisfiability",
    url = "http://dx.doi.org/10.1007/11499107_41",
    series = "Lecture Notes in Computer Science",
    booktitle = "Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT'05, St. Andrews, Scotland, June 2005)",
    publisher = "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 $\alpha > 4.2$. This is much closer to the satisfiability transition threshold $\alpha_c \approx 4.267$ than has generally been assumed possible for local search algorithms.",
    note = "",
    flags = "public",
    year = "2005",
    keywords = "satisfiability, local search, phase transition, WalkSAT, Metropolis algorithm",
    pages = "475--481",
    address = "Berlin Heidelberg"
}