An experimental study of satisfiability search heuristics

Interest in propositional satisfiability (SAT) has been on the rise lately, spurred in part by the recent availability of powerful solvers that are sufficiently efficient and robust to deal with the large-scale SAT problems that typically arise in electronic design automation application. A frequent question that CAD tool developers and users typically ask is which of these various solvers is “best”; the quick answer is, of course, “it depends”. In this paper we attempt to gain some insight into, rather than definitively answer, this question