An Exponential Separation between Deterministic CDCL and DPLL Solvers
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918393364348928 |
|---|---|
| author | Samar, Sahil Vinyals, Marc Ganesh, Vijay |
| author_facet | Samar, Sahil Vinyals, Marc Ganesh, Vijay |
| contents | We prove that there exists a deterministic configuration of Conflict Driven Clause Learning (CDCL) SAT solvers using a variant of the VSIDS branching heuristic that solves instances of the Ordering Principle (OP) CNF formulas in time polynomial in n, where n is the number of variables in such formulas. Since tree-like resolution is known to have an exponential lower bound for proof size for OP formulas, it follows that CDCL under this configuration has an exponential separation with any solver that is polynomially equivalent to tree-like resolution and therefore any configuration of DPLL SAT solvers. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_16156 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | An Exponential Separation between Deterministic CDCL and DPLL Solvers Samar, Sahil Vinyals, Marc Ganesh, Vijay Computational Complexity We prove that there exists a deterministic configuration of Conflict Driven Clause Learning (CDCL) SAT solvers using a variant of the VSIDS branching heuristic that solves instances of the Ordering Principle (OP) CNF formulas in time polynomial in n, where n is the number of variables in such formulas. Since tree-like resolution is known to have an exponential lower bound for proof size for OP formulas, it follows that CDCL under this configuration has an exponential separation with any solver that is polynomially equivalent to tree-like resolution and therefore any configuration of DPLL SAT solvers. |
| title | An Exponential Separation between Deterministic CDCL and DPLL Solvers |
| topic | Computational Complexity |
| url | https://arxiv.org/abs/2603.16156 |