Understanding CDCL Solvers via Scalability Studies and Proofdoors

Abstract

Over the past several decades, Conflict-Driven Clause Learning (CDCL) SAT solvers have proven remarkably effective on large industrial formulas, despite SAT being NP-complete and widely believed to be intractable. While considerable empirical research has been done on solver performance over benchmarks like the SAT competition, as well as scaling studies on random and crafted families, surprisingly little effort has gone into systematic scaling studies over industrial instances. To address this gap, we collect a large benchmark of Bounded Model Checking (BMC) instances (76,600 across 766 families) and perform a systematic scaling study of solver performance. We observe a spectrum: some families scale linearly, others polynomially or exponentially. Building on this foundation, we study the structural parameters that have been proposed in an attempt to explain this phenomenon. We first show that previously proposed parameters— clause-variable ratio, treewidth, and community structure—fail to discriminate between the linear and exponential regimes. By contrast, properties of the recently proposed proofdoor parameter correlate well with CDCL solver performance. Informally, a proofdoor is a sequence of interpolants between chunks of a formula, where each interpolant represents the solver’s memoization of reasoning effort on chunks it has already analyzed. In support of the proofdoor hypothesis, we make three key contributions. First, we empirically show that CDCL solvers usually do compute small proofdoors for linearly-scaling BMC instances. Second, we show that for exponentially-scaling instances, sampled proofdoors scale exponentially and are typically not incrementally absorbed. Third, we show that scrambling linearly-scaling instances yields larger proofdoor sizes relative to pre-scrambling, relating poor branching orders to larger proofdoor sizes and degradation in solver performance.