On CDCL-based proof systems with the ordered decision strategy

TL;DR

This paper establishes a theoretical connection between CDCL-based SAT solvers with specific decision strategies and classical resolution proof systems, revealing how different learning schemes influence their equivalence to resolution.

Contribution

It provides the first formal analysis of how particular decision strategies and clause learning schemes in CDCL solvers relate to ordered and general resolution.

Findings

Ordered decision strategy with DECISION learning is equivalent to ordered resolution.

Replacing the learning scheme with a stopping rule yields equivalence to general resolution.

Introduces a formal model for analyzing CDCL-based proof systems.

Abstract

We prove that conflict-driven clause learning 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 that stops after the first new clause when backtracking, they become equivalent to general resolution. To the best of our knowledge, 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 allows for succinct and precise theorem statements.