SAT Solvers and Ordered Decision Strategies

SAT solvers have become standard tools in many application domains. The techniques dominating the landscape of practical SAT solving today are collectively called “Conflict-Driven Clause Learning” (CDCL) and their tight connections to proof complexity and the resolution proof system in particular make them very amenable to mathematical analysis.
We will start by reviewing the most important features of CDCL-based solvers, such as decision strategy, learning scheme and restart policy. Time permitting, we will talk about the effect the choice of decision strategy may have on the performance of the solvers. Somewhat surprisingly, the answer crucially depends on a priori unrelated feature, learning scheme.
Based on joint work with Nathan Mull and Shuo Pang.