Between SAT and UNSAT: The Fundamental Difference in CDCL SAT

摘要

The way CDCL SAT solvers find a satisfying assignment is very different from the way they prove unsatisfiability. We propose an explanation to the difference by identifying direct connections to the workings of some of the most important elements in CDCL solvers: the effects of restarts and VSIDS, and the roles of learned clauses. We give a wide range of concrete evidence that highlights the varying effects and roles of these elements. As a result, this paper also sheds a new light on the internal workings of CDCL. Based on our reasoning on the difference in solver behaviors, we present several ideas for optimizing SAT solvers for either SAT or UNSAT instances. We then show that we can achieve improvements on both SAT and UNSAT at the same time by judiciously exploiting the difference. We have implemented a hybrid idea mixing two different restart strategies on top of our new solver COMiniSatPS and observed substantial performance improvement.