On CDCL-Based Proof Systems with the Ordered Decision Strategy

We prove that conflict-driven clause learning (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 stops after the first nonconflict clause when backtracking, they become equivalent to general resolution. To the best of our knowledge, along with [M. Vinyals, ``Hard Examples for Common Variable Decision Heuristics, "" in Proceedings of the 34th AAAI Conference on Artificial Intelligence, 2020, pp. 1652-1659], this is the first theoretical study of the interplay between specific decision strategies and clause learning. For 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 discussing CDCL-based proof systems that allow for succinct and precise theorem statements.