WalkSAT is linear on random 2-SAT

TL;DR

This paper proves that the WalkSAT local search algorithm solves random 2-SAT problems in linear expected time up to the satisfiability threshold, confirming its efficiency in practical and theoretical contexts.

Contribution

It establishes that WalkSAT operates in linear expected time on random 2-SAT instances across all densities up to the satisfiability threshold, answering a previously open question.

Findings

WalkSAT runs in linear expected time for all clause/variable densities up to the satisfiability threshold.

The result confirms the efficiency of WalkSAT on random 2-SAT problems.

Provides theoretical backing for the practical success of WalkSAT in solving 2-SAT instances.

Abstract

In an influential article Papadimitriou [FOCS 1991] proved that a local search algorithm called WalkSAT finds a satisfying assignment of a satisfiable 2-CNF with $n$ variables in $O(n^2)$ expected time. Variants of the WalkSAT algorithm have become a mainstay of practical SAT solving (e.g., [Hoos and St\"utzle 2000]). In the present article we analyse the expected running time of WalkSAT on random 2-SAT instances. Answering a question raised by Alekhnovich and Ben-Sasson [SICOMP 2007], we show that WalkSAT runs in linear expected time for all clause/variable densities up to the random 2-SAT satisfiability threshold.