Complete Local Search for Propositional Satisfiability

Abstract

Algorithms based on following local gradient information are surprisingly effective for certain classes of constraint satis-faction problems. Unfortunately, previous local search algo-rithms are notoriously incomplete: They are not guaranteed to nd a feasible solution if one exists and they cannot be used to determine unsatisability. We present an algorithmic frame-work for complete local search and discuss in detail an instan-tiation for the propositional satisability problem (SAT). The fundamental idea is to use constraint learning in combination with a novel objective function that converges during search to a surface without local minima. Although the algorithm has worst-case exponential space complexity, we present em-pirical results on challenging SAT competition benchmarks that suggest that our implementation can perform as well as state-of-the-art solvers based on more mature techniques. Our framework suggests a range of possible algorithms lying between tree-based search and local search.