Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

WalkSAT is linear on random 2-SAT

Petra Berenbrink, Amin Coja-Oghlan, Colin Cooper, Thorsten Götte, Lukas Hintze, Pavel Zakharov

TL;DR

This work analyzes WalkSAT on random 2-CNF formulas and proves that, for any clause-to-variable density α in [0,1), the expected running time conditioned on the instance is linear in the number of variables, specifically E[T(Φ)|Φ] ≤ C n /(1-α)^2 with high probability. The authors introduce a novel two-part approach: they build implication sub-formulas via Unit Clause Propagation to lock WalkSAT’s progress, and they bound the total size of these sub-formulas to bound the number of flips. They show a locking property that once a sub-formula is satisfied WalkSAT stops flipping its variables, and they bound per-variable flips by the square of the sub-formula size, which together yield the linear-time result. This directly proves the long-standing conjecture that WalkSAT runs in linear expected time on random 2-SAT up to the satisfiability threshold α = 1, aligning with physics-based predictions and advancing understanding of local search performance on random CSPs.

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ützle 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.

WalkSAT is linear on random 2-SAT

TL;DR

This work analyzes WalkSAT on random 2-CNF formulas and proves that, for any clause-to-variable density α in [0,1), the expected running time conditioned on the instance is linear in the number of variables, specifically E[T(Φ)|Φ] ≤ C n /(1-α)^2 with high probability. The authors introduce a novel two-part approach: they build implication sub-formulas via Unit Clause Propagation to lock WalkSAT’s progress, and they bound the total size of these sub-formulas to bound the number of flips. They show a locking property that once a sub-formula is satisfied WalkSAT stops flipping its variables, and they bound per-variable flips by the square of the sub-formula size, which together yield the linear-time result. This directly proves the long-standing conjecture that WalkSAT runs in linear expected time on random 2-SAT up to the satisfiability threshold α = 1, aligning with physics-based predictions and advancing understanding of local search performance on random CSPs.

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 variables in expected time. Variants of the WalkSAT algorithm have become a mainstay of practical SAT solving (e.g., [Hoos and Stützle 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.

Paper Structure

This paper contains 12 sections, 11 theorems, 33 equations, 1 figure, 2 algorithms.

Table of Contents

  1. Introduction
  2. Background and motivation
  3. The main result
  4. Preliminaries and notation
  5. Proof strategy
  6. Unit Clause Propagation and implication sub-formulas
  7. Locking WalkSAT in
  8. The expected running time
  9. Discussion
  10. Proof of Proposition \ref{['prop_l2']}
  11. Proof of Proposition \ref{['prop_flips_per_var']}
  12. Proof of Proposition \ref{['prop_upper_bound_small_subformula']}

Key Result

Theorem 1.1

There exists a constant $C>0$ such that for all $0\leq\alpha<1$ we have

Figures (1)

  • Figure 1: Empirical runtime of WalkSAT, normalized by $n$. Each point represents one run of WalkSAT on a random $2$-SAT instance with $m=\alpha n$ clauses.

Theorems & Definitions (19)

  • Theorem 1.1
  • Proposition 2.1
  • proof
  • Proposition 2.3
  • proof
  • Proposition 2.5
  • proof : Proof of Theorem \ref{['thm_main']}
  • Lemma 3.1
  • Lemma 3.2: 2satclt
  • Theorem 3.3: AS
  • ...and 9 more