3 papers
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…
math.GR2026
On the trivial units property and the unique product property
Heiko Dietrich, Melissa Lee, Andre Nies +1
We report on some computational experiments related to the trivial units property and unique product property for group rings of torsion-free groups. These properties are related t…
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…