Systematic vs. Local Search for SAT

Abstract. 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-3SAT local search is clearly superior, more structured instances are often, but not always, more e...

• Type: Conference
• Year: 1999
• Where: KI
• Authors: Holger H. Hoos, Thomas Stützle
• Keywords: Artificial Intelligence, KI 1999, Local Search, Sat Instances, Systematic Search Algorithms