Threshold Behaviour of WalkSAT and Focused Metropolis Search on Random 3-Satisfiability

摘要

An important heuristic in local search algorithms for Satisfiability is 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 α > 4.2. This is much closer to the satisfiability transition threshold α_c ≈ 4.267 than has generally been assumed possible for local search algorithms.