On CDCL-based proof systems with the ordered decision strategy

Nathan Mull, Shuo Pang, Alexander Razborov

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 th…