Phase transition for local search on planted SAT

Abstract

The Local Search algorithm (or Hill Climbing, or Iterative Improvement) is one of the simplest heuristics to solve the Satisfiability and Max-Satisfiability problems. Although it is not the best known Satisfiability algorithm even for the class of problems we study, the Local Search is a part of many satisfiability and max-satisfiability solvers, where it is used to find a good starting point for a more sophisticated heuristics, and to improve a candidate solution. In this paper we give an analysis of Local Search on random planted 3-CNF formulas. We show that a sharp transition of efficiency of Local Search occurs at density (equation found). Specifically we show that if there is κ < 7/6 such that the clause-to-variable ratio is less than κ ln n (n is the number of variables in a CNF) then Local Search whp does not find a satisfying assignment, and if there is κ > 7/6 such that the clause-to-variable ratio is greater than κ ln n then the local search whp finds a satisfying assignment. As a byproduct we also show that for any constant ϱ there is γ such that Local Search applied to a random (not necessarily planted) 3-CNF with clause-to-variable ratio ϱ produces an assignment that satisfies at least γn clauses less than the maximal number of satisfiable clauses.