Walksat Stalls Well Below Satisfiability.

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 randomized 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 that Walksat is ineffective with high probability (w.h.p.) if m/n > c2(k) ln(2) k/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 w.h.p. if m/n < c' 2(k)/k for another constant c' > 0 [A. Coja-Oghlan and A. Frieze, SIAM J. Comput., 43 (2014), pp. 1456-1485].