Proofdoors and Efficiency of CDCL Solvers

TL;DR

This paper introduces the proofdoor parameter to explain the efficiency of CDCL SAT solvers on circuit verification problems, linking small proofdoors to short resolution proofs and solver efficiency.

Contribution

It formalizes proofdoors as a new framework to analyze CDCL solver performance and demonstrates their explanatory power through theoretical results and specific formula classes.

Findings

Formulas with small proofdoors have short resolution proofs.

Certain CDCL configurations can find proofs in polynomial time for small proofdoor formulas.

Miter formulas over floating-point addition have small proofdoors and short proofs despite large pathwidth.

Abstract

We propose a new parameter called proofdoor in an attempt to explain the efficiency of CDCL SAT solvers over formulas derived from circuit (esp., arithmetic) verification applications. Informally, given an unsatisfiable CNF formula F over n variables, a proofdoor decomposition consists of a chunking of the clauses into A1, . . . , Ak together with a sequence of interpolants connecting these chunks. Intuitively, a proofdoor captures the idea that an unsatisfiable formula can be refuted by reasoning chunk by chunk, while maintaining only a summary of the information (i.e., interpolants) gained so far for subsequent reasoning steps. We prove several theorems in support of the proposition that proofdoors can explain the efficiency of CDCL solvers for some class of circuit verification problems. First, we show that formulas with small proofdoors (i.e., where each interpolant is O(n) sized, each chunk Ai has small pathwidth, and each interpolant clause has at most O(log(n)) backward dependency on the previous interpolant) have short resolution (Res) proofs. Second, we show that certain configurations of CDCL solvers can compute such proofs in time polynomial in n. Third, we show that commutativity (miter) formulas over floating-point addition have small proofdoors and hence short Res proofs, even though they have large pathwidth. Fourth, we characterize the limits of the proofdoor framework by connecting proofdoors to the partially ordered resolution proof system: we show that a poor decomposition of arithmetic miter instances can force exponentially large partially ordered resolution proofs, even when a different decomposition (i.e., small proofdoors) permits short proofs.