Showing cs.CCShow all
3 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…
cs.CC2024
Proving Unsatisfiability with Hitting Formulas
Yuval Filmus, Edward A. Hirsch, Artur Riazanov +2
Hitting formulas have been studied in many different contexts at least since [Iwama,89]. A hitting formula is a set of Boolean clauses such that any two of them cannot be simultane…