On CDCL-Based Proof Systems with the Ordered Decision Strategy

Citations of this article
Mendeley users who have this article in their library.

This artice is free to access.


We prove that CDCL SAT-solvers with the ordered decision strategy and the DECISION learning scheme are equivalent to ordered resolution. We also prove that, by replacing this learning scheme with its opposite, which learns the first possible non-conflict clause, they become equivalent to general resolution. In both results, we allow nondeterminism in the solver’s ability to perform unit propagation, conflict analysis, and restarts in a way that is similar to previous works in the literature. To aid the presentation of our results, and possibly future research, we define a model and language for CDCL-based proof systems – particularly those with nonstandard features – that allow for succinct and precise theorem statements.




Mull, N., Pang, S., & Razborov, A. (2020). On CDCL-Based Proof Systems with the Ordered Decision Strategy. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12178 LNCS, pp. 149–165). Springer. https://doi.org/10.1007/978-3-030-51825-7_12

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free