Theoretical analysis of practical heuristics for satisfiability

The Satisfiability problem (SAT) is one of the central subjects of research in modern computing science. This problem provides a rich language to model practical problems. Moreover modern SAT solvers are capable of solving large instances of SAT and can be successfully applied to industrial scale problems. Since SAT is NP-complete the success of the practical SAT algorithms apparently contradicts the belief that NP-complete problems are hard to solve. Understanding of this phenomenon is far from complete. One of the most promising approaches to explaining this phenomenon is the typical case analysis. Local search principles are actively used for practical SAT solving, as well as for many other important problems. In this work we perform a typical case analysis of the basic Local Search algorithm on Random Planted 3-SAT. We show that a phase transition of the effectiveness of the Local Search on Random Planted 3-SAT occurs at density ρ = 7/6 ln n. That is, for any constant ε the algorithm with high probability solves instances of density (7/6 + ε) ln n and with high probability fails for instances of density (7/6 - ε )ln n. The first successful practical algorithm based on local search principles, GSAT, was proposed in 1991 by Selman, Levesque and Mitchell. In fact this algorithm is nothing more than basic Local Search enhanced with plateau moves. At the time the algorithm was proposed, it was outperforming state of the art systematic search solvers and it continues serving a basis for development of efficient local search algorithms. We analyze GSAT theoretically on Random Planted 3-SAT and show that it can solve Random Planted 3-SAT of any density ρ such that ρ >κ ln n for some constant κ. This theoretical result agrees with, and partially explains, the empirical observation that adding plateau moves dramatically improves Local Search. Finally we propose a Weighted Random Walk algorithm. The algorithm is obtained by adding a simple weighting scheme to the well known Random Walk algorithm. We prove that Weighted Random Walk with high probability gives a good approximation. Moreover, in experiments this simple algorithm solves Random Planted 3-SAT for any constant density.