CDCL SAT solvers compute small proofdoors on linearly scaling BMC families but large non-absorbed ones on exponential families, as shown by empirical measurements on a 76k+ instance benchmark where prior parameters fail to discriminate regimes.
Clause-learning algorithms with many restarts and bounded-width resolution
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
fields
cs.LO 2representative citing papers
New ERCL algorithm using dual implication points in CDCL SAT solvers shows performance gains over baselines on Tseitin and XORified formulas.
citing papers explorer
-
Understanding CDCL Solvers via Scalability Studies and Proofdoors
CDCL SAT solvers compute small proofdoors on linearly scaling BMC families but large non-absorbed ones on exponential families, as shown by empirical measurements on a 76k+ instance benchmark where prior parameters fail to discriminate regimes.
-
Extended Resolution Clause Learning via Dual Implication Points
New ERCL algorithm using dual implication points in CDCL SAT solvers shows performance gains over baselines on Tseitin and XORified formulas.