Showing cs.CCShow all
2 papers · 1 filter
cs.CC2026
Proofdoors and Efficiency of CDCL Solvers
Sunidhi Singh, Vincent Liew, Marc Vinyals +1
We propose a new parameter called proofdoor in an attempt to explain the efficiency of CDCL SAT solvers over a certain class of formulas derived from circuit (esp., arithmetic) ver…
cs.CC2026
An Exponential Separation between Deterministic CDCL and DPLL Solvers
Sahil Samar, Marc Vinyals, Vijay Ganesh
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 instance…