BIRS Workshop Lecture Videos

Banff International Research Station Logo

BIRS Workshop Lecture Videos

On CDCL-based Proof Systems with the Ordered Decision Strategy Mull, Nathan


It has been well-established that CDCL SAT solvers with restarts can simulate general resolution. However, these results require that the solver use a highly nondeterministic or sufficiently random decision strategy. Our goal is to understand the impact of more explicit decision strategies on the theoretical strength of CDCL. Since decisions strategies used in practice are somewhat complicated, we instead focus on the simpler ordered decision strategy: when the solver has to choose a variable to assign, it must choose the smallest unassigned variable according to some underlying order. This strategy was studied by Beame et. al. (2002) in the context of DLL without clause learning. It is still possible for unit propagation to assign variables out of order, which is what makes this situation more subtle and non-trivial.

Our motivating question is the following: is there a family of unsatisfiable formulas that possess polynomial size resolution refutations but require super-polynomial time for CDCL using the ordered decision strategy We present preliminary results towards this end. First, we show that CDCL with the ordered decision strategy and the so-called DECISION learning scheme is no more powerful than ordered resolution. Second, we show that CDCL with the ordered decision strategy and a somewhat powerful learning scheme we call FIRST-L (similar to FirstNewCut introduced by Beame et. al. (2004)) is equivalent to general resolution, given it can ignore unit clauses and conflicts. This result may be interpreted as demonstrating that mandatory unit propagation or conflict analysis is, in some sense, necessary to positively answer our the question above.

To aid this work, we also present a model and language for discussing CDCL-based proof systems. This is not meant to be novel and is heavily influenced by previous works. But rather than being faithful to practical SAT-solver implementations, the goal of our model is highlighting possible non-standard sources of nondeterminism. It allows for clear and concise mathematical statements about CDCL-based proof systems and better represents the landscape of potential CDCL variants.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International