Walksat stalls well below the satisfiability threshold

TL;DR

This paper rigorously demonstrates that WalkSAT, a popular randomized SAT solver, fails to find solutions efficiently once the clause-to-variable ratio exceeds a certain threshold related to phase transitions in the solution space.

Contribution

The paper provides the first rigorous proof that WalkSAT stalls well below the satisfiability threshold in random k-SAT problems, linking algorithm failure to the geometry of solutions.

Findings

WalkSAT fails with high probability when m/n > c2^k ln^2 k / k.

WalkSAT is effective in linear time when m/n < c'2^k / k.

Phase transitions in solution space affect practical algorithm performance.

Abstract

Partly on the basis of heuristic arguments from physics it has been suggested that the performance of certain types of algorithms on random $k$-SAT formulas is linked to phase transitions that affect the geometry of the set of satisfying assignments. But beyond intuition there has been scant rigorous evidence that "practical" algorithms are affected by these phase transitions. In this paper we prove that \walksat, a popular randomised satisfiability algorithm, fails on random $k$-SAT formulas not very far above clause/variable density where the set of satisfying assignments shatters into tiny, well-separated clusters. Specifically, we prove \walksat\ is ineffective with high probability if $m/n>c2^k\ln^2k/k$, where $m$ is the number of clauses, $n$ is the number of variables and $c>0$ is an absolute constant. By comparison, \walksat\ is known to find satisfying assignments in linear time \whp\ if $m/n<c'2^k/k$ for another constant $c'>0$ [Coja-Oghlan and Frieze, SIAM J.\ Computing 2014].