The Impact of Branching Heuristics in Propositional Satisfiability Algorithms
João P. Marques-Silva · 1999
. This paper studies the practical impact of the branching heuristics used in Propositional Satisability (SAT) algorithms, when applied to solving real-world instances of SAT. In addition, dierent SAT algorithms are experimentally evaluated. The main conclusion of this study is that even though branching heuristics are crucial for solving SAT, other aspects of the organization of SAT algorithms are also essential. Moreover, we provide empirical evidence that for practical instances of SAT, the search pruning techniques included in the most competitive SAT algorithms may be of more fundamental signicance than branching heuristics. Keywords: Propositional Satisability, Backtrack Search, Branching Heuristics. 1 Introduction Propositional Satisability (SAT) is a core problem in Articial Intelligence, as well as in many other areas of Computer Science and Engineering. Recent years have seen dramatic improvements in the real world performance of SAT algorithms. On one hand, local sear...