Do merge-based proof systems exactly capture the simulation-cost bottleneck of CDCL SAT solvers?

Conflict-driven clause learning (CDCL) SAT solvers can simulate resolution proofs, but only with provable overhead. Vinyals, Li, Fleming, Kolokolova and Ganesh (SAT 2023) introduced merge-respecting proof systems — RML, RMA, REL and variants — which contain the runs of CDCL solvers with any 1-empowering learning scheme (including 1UIP and standard clause minimization), proved that these systems simulate unrestricted resolution with at most a linear overhead, and exhibited formulas with linear-size resolution refutations that require quadratic-size RMA refutations. The paper explicitly asks whether these systems capture the CDCL simulation-cost bottleneck exactly: can CDCL — possibly using learning or minimization strategies, restarts, or heuristics not modeled by these systems — simulate some flavour of merge resolution with asymptotically less overhead than is required to simulate unrestricted resolution? The problem is open as of 2026, and the adjacent longstanding question whether restarts are necessary for CDCL to simulate resolution also remains open.

Background

Propositional satisfiability (SAT) asks whether a Boolean formula in conjunctive normal form (CNF) — a set of clauses, each a disjunction of literals — admits a satisfying assignment; it is NP-complete. All competitive SAT solvers use conflict-driven clause learning (CDCL): whenever unit propagation (repeatedly forcing assignments from clauses that have become unit) reaches a conflicting clause, the solver analyzes the conflict, learns a new clause, backjumps, and continues; from a refuting run one can extract a resolution refutation. Resolution is the classical propositional proof system whose single rule derives $A\lor B$ from $A\lor x$ and $B\lor\lnot x$. A proof system $P$ polynomially simulates (p-simulates) a system $Q$ if every $Q$-refutation of size $S$ can be efficiently transformed into a $P$-refutation of size polynomial in $S$; the multiplicative blow-up is the simulation overhead. Restarting — abandoning the current partial assignment while keeping learned clauses — is a solver feature whose proof-complexity role remains only partially understood.

Pipatsrisawat and Darwiche (2011) and Atserias, Fichte and Thurley (2011) proved that CDCL with restarts, asserting clause learning, and non-deterministic branching p-simulates resolution: whenever a formula over $n$ variables has a resolution refutation of length $L$, a suitable CDCL run refutes it in time polynomial in $n$ and $L$. The known simulations carried a large multiplicative overhead — $O(n^4L)$ steps in the proof of Pipatsrisawat and Darwiche, improved to $O(n^3L)$ by Beyersdorff and Böhm (2021) — and before 2023 it was not even known whether any overhead was necessary at all.

Vinyals, Li, Fleming, Kolokolova and Ganesh (SAT 2023) isolated one structural property that forces overhead. A merge — a notion going back to Andrews (1968) — is a resolution step whose two premises share a literal besides the resolved variable. Every clause learned by practical learning schemes is, or extends, a 1-empowering clause: a clause that enables a unit propagation impossible before it was learned. The 1UIP (first unique implication point) scheme used by virtually all solvers produces such clauses, as do standard clause-minimization procedures applied on top; and by a lemma of Atserias–Fichte–Thurley / Pipatsrisawat–Darwiche, every 1-empowering clause contains a merge in its derivation. The paper formalizes merge-respecting proof systems: RML (Resolution with Merge Lemmas), a sequence of unit-resolution derivations (each inference has a single-literal premise) in input structure (each derivation is a chain in which all clauses but one anchoring clause are used only once) whose learned lemmas are merges; RMA (Resolution with Merge Ancestors), where any reused clause must have merge ancestry; plus variants including REL (Resolution with Empowering Lemmas), defined directly by the 1-empowerment property, and locally regular variants, in which no resolved-upon variable reappears later within the same derivation. RMA contains the proofs produced by CDCL solvers with any asserting or 1-empowering learning scheme, even with clause minimization applied on top, and 1UIP proofs are already in RML. They proved: (i) these systems simulate unrestricted resolution with at most a linear multiplicative overhead; and (ii) the overhead is necessary — there is a family of formulas over $O(n\log n)$ variables with resolution refutations of linear length whose RMA refutations have quadratic length. Hence merge-respecting CDCL can be asymptotically worse than resolution by a linear factor, whereas in the tree-like setting the analogous merge restriction (Andrews) costs nothing — which is precisely why the DAG-like tightness question is delicate. What the paper could not settle is whether its systems explain all of the overhead that real CDCL solvers pay.

Problem Statement

Let $X$ be the smallest asymptotic overhead with which CDCL, in its full generality — any clause-learning scheme (1-empowering or not), any clause-minimization procedure, any restart policy (with or without restarts), and any branching heuristics — can simulate unrestricted resolution. Let $Y$ be the smallest asymptotic overhead with which CDCL can simulate some flavour of merge resolution (tree-like or DAG-like RML, RMA, REL, or their locally regular variants, as defined by Vinyals–Li–Fleming–Kolokolova–Ganesh 2023). The source paper proves that merge-resolution flavours simulate unrestricted resolution with at most a linear multiplicative overhead, and that a linear overhead is necessary for RMA itself (Theorem 5.1: a formula family with linear-size resolution refutations requiring quadratic-size RMA refutations); since RMA contains CDCL with any 1-empowering/asserting learning scheme together with standard clause minimization, all such CDCL configurations inherit the quadratic lower bound on the separating formula family. The paper's concluding remarks pose the unresolved question: can $Y$ be asymptotically strictly smaller than $X$? Determine which of the following holds:

(a) Escape: exhibit a concrete CDCL behavior — a learning, minimization, restart, or heuristic mechanism — together with a proof that it simulates some flavour of merge resolution with asymptotically strictly less overhead than is required to simulate unrestricted resolution, thereby showing that merge-based proof systems do not capture the CDCL simulation-cost bottleneck exactly; or

(b) Capture: prove that no CDCL behavior in the general model above beats the merge overhead — that simulating merge-resolution flavours is asymptotically no cheaper for CDCL than simulating unrestricted resolution — thereby showing that merge-based systems capture the bottleneck exactly.

The answer must hold for CDCL in the general model above, not merely for 1UIP-like or otherwise merge-respecting learning. The adjacent standing open question flagged by the same paper — whether restarts are necessary for CDCL to simulate general resolution — is related but is not a required deliverable here; a route-(a) escape that exhibits restart- or learning-based mechanisms would also bear on that adjacent question.

References

1. Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, Vijay Ganesh. Limits of CDCL Learning via Merge Resolution. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), Leibniz International Proceedings in Informatics (LIPIcs), vol. 271, pp. 27:1–27:19, 2023. DOI: 10.4230/LIPIcs.SAT.2023.27, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.27 (preprint arXiv:2304.09422, https://arxiv.org/abs/2304.09422)
2. Chunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi, Vijay Ganesh. Towards a Complexity-Theoretic Understanding of Restarts in SAT Solvers. In 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT 2020), Lecture Notes in Computer Science, vol. 12178, pp. 233–249, 2020. DOI: 10.1007/978-3-030-51825-7_17, https://doi.org/10.1007/978-3-030-51825-7_17 (preprint arXiv:2003.02323, https://arxiv.org/abs/2003.02323)
3. Albert Atserias, Moritz Müller. Automating Resolution is NP-Hard. Journal of the ACM, vol. 67, no. 5, pp. 1–17, 2020. DOI: 10.1145/3409472, https://doi.org/10.1145/3409472
4. Olaf Beyersdorff, Benjamin Böhm. Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021), Leibniz International Proceedings in Informatics (LIPIcs), vol. 185, pp. 12:1–12:20, 2021. DOI: 10.4230/LIPIcs.ITCS.2021.12, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2021.12
5. Olaf Beyersdorff, Benjamin Böhm, Meena Mahajan. Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs. Journal of Automated Reasoning, vol. 69, article 30, 2025. DOI: 10.1007/s10817-025-09745-6, https://doi.org/10.1007/s10817-025-09745-6
6. Sunidhi Singh, Vincent Liew, Marc Vinyals, Vijay Ganesh. Proofdoors and Efficiency of CDCL Solvers. Preprint arXiv:2603.26286, 2026, https://arxiv.org/abs/2603.26286
7. Knot Pipatsrisawat, Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence, vol. 175, no. 2, pp. 512–525, 2011. DOI: 10.1016/j.artint.2010.10.002, https://doi.org/10.1016/j.artint.2010.10.002
8. Albert Atserias, Johannes Klaus Fichte, Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. Journal of Artificial Intelligence Research, vol. 40, pp. 353–373, 2011. DOI: 10.1613/jair.3152, https://doi.org/10.1613/jair.3152
9. Peter B. Andrews. Resolution with Merging. Journal of the ACM, vol. 15, no. 3, pp. 367–381, 1968. DOI: 10.1145/321466.321469, https://doi.org/10.1145/321466.321469
10. Nathan Mull, Shuo Pang, Alexander Razborov. On CDCL-Based Proof Systems with the Ordered Decision Strategy. SIAM Journal on Computing, vol. 51, no. 4, pp. 1368–1399, 2022. DOI: 10.1137/20M1362528, https://doi.org/10.1137/20M1362528 (preprint arXiv:1909.04135, https://arxiv.org/abs/1909.04135)
11. Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, Stefan Szeider. Hardness of Random Reordered Encodings of Parity for Resolution and CDCL. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI-24), vol. 38, no. 8, pp. 7978–7986, 2024. DOI: 10.1609/AAAI.V38I8.28635, https://doi.org/10.1609/AAAI.V38I8.28635 (preprint arXiv:2402.00542, https://arxiv.org/abs/2402.00542)
12. Sahil Samar, Marc Vinyals, Vijay Ganesh. An Exponential Separation between Deterministic CDCL and DPLL Solvers. Preprint arXiv:2603.16156, 2026, https://arxiv.org/abs/2603.16156