Complete Local Search for Propositional Satisfiability

13 years 6 months ago
Complete Local Search for Propositional Satisfiability
Algorithms based on following local gradient information are surprisingly effective for certain classes of constraint satisfaction problems. Unfortunately, previous local search algorithms are notoriously incomplete: They are not guaranteed to find a feasible solution if one exists and they cannot be used to determine unsatisfiability. We present an algorithmic framework for complete local search and discuss in detail an instantiation for the propositional satisfiability 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 empirical 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...
Hai Fang, Wheeler Ruml
Added 30 Oct 2010
Updated 30 Oct 2010
Type Conference
Year 2004
Where AAAI
Authors Hai Fang, Wheeler Ruml
Comments (0)