We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

On CDCL-based Proof Systems with the Ordered Decision Strategy

Formale Metadaten

Titel
On CDCL-based Proof Systems with the Ordered Decision Strategy
Serientitel
Anzahl der Teile
28
Autor
Lizenz
CC-Namensnennung - keine kommerzielle Nutzung - keine Bearbeitung 4.0 International:
Sie dürfen das Werk bzw. den Inhalt in unveränderter Form zu jedem legalen und nicht-kommerziellen Zweck nutzen, vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
Identifikatoren
Herausgeber
Erscheinungsjahr
Sprache

Inhaltliche Metadaten

Fachgebiet
Genre
Abstract
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.