An efficient local search method for random 3-satisfiability

Reference:

Sakari Seitz and Pekka Orponen. An efficient local search method for random 3-satisfiability. In Lefteris M. Kirousis and Evangelos Kranakis, editors, Proceedings of the IEEE LICS'03 Workshop on Typical Case Complexity and Phase Transitions (Ottawa, Canada, June 2003), volume 16 of Electronic Notes in Discrete Mathematics, Amsterdam, 2003. Elsevier.

Abstract:

We report on some exceptionally good results in the solution of randomly generated 3-satisfiability instances using the ``record-to-record travel (RRT)'' local search method. When this simple, but less-studied algorithm is applied to random one-million variable instances from the problem's satisfiable phase, it seems to find satisfying truth assignments almost always in linear time, with the coefficient of linearity depending on the ratio of clauses to variables in the generated instances. RRT has a parameter for tuning ``greediness''. By lessening greediness, the linear time phase can be extended up to very close to the satisfiability threshold . Such linear time complexity is typical for random-walk based local search methods for small values of . Previously, however, it has been suspected that these methods necessarily lose their time linearity far below the satisfiability threshold. The only previously introduced algorithm reported to have nearly linear time complexity also close to the satisfiability threshold is the survey propagation (SP) algorithm. However, SP is not a local search method and is more complicated to implement than RRT. Comparative experiments with the WalkSAT local search algorithm show behavior somewhat similar to RRT, but with the linear time phase not extending quite as close to the satisfiability threshold.

Keywords:

stochastic algorithms, local search, combinatorial phase transitions, satisfiability problem

Suggested BibTeX entry:

@inproceedings{SeOr03,
    address = {Amsterdam},
    author = {Sakari Seitz and Pekka Orponen},
    booktitle = {Proceedings of the IEEE LICS'03 Workshop on Typical Case Complexity and Phase Transitions (Ottawa, Canada, June 2003)},
    editor = {Lefteris M. Kirousis and Evangelos Kranakis},
    publisher = {Elsevier},
    series = {Electronic Notes in Discrete Mathematics},
    title = {An efficient local search method for random 3-satisfiability},
    volume = {16},
    year = {2003},
}