Systematic vs. Local Search for SAT

Due to its prominence in artificial intelligence and theoretical computer science, the propositional satisfiability problem (SAT) has received considerable attention in the past. Traditionally, this problem was attacked with systematic search algorithms, but more recently, local search methods were shown to be very effective for solving large and hard SAT instances. Especially in the light of recent, significant improvements in both approaches, it is not very well understood which type of algorithm performs best on a specific type of SAT instances. In this article, we present the results of a comprehensive empirical study, comparing the performance of some of the best known stochastic local search and systematic search algorithms for SAT on a wide range of problem instances, including Random-3-SAT and SAT-encoded problems from different domains. We show that while for Random-3-SAT local search is clearly superior, more structured instances are often, but not always, more efficiently solved by systematic search algorithms. This suggests that considering the specific strengths and weaknesses of both approaches, hybrid algorithms or portfolio combinations might be most effective for solving SAT problems in practice.