Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Proofdoors and Efficiency of CDCL Solvers

Sunidhi Singh, Vincent Liew, Marc Vinyals, Vijay Ganesh

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.

Proofdoors and Efficiency of CDCL Solvers

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.

Paper Structure

This paper contains 18 sections, 18 theorems, 8 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Proofdoors
  4. Proofdoor Theorem
  5. Commutativity of Floating-Point Addition
  6. Partially Ordered Resolution Lower Bounds
  7. Lower bounds via interpolation
  8. Warm-up: Lower bounds for Function Encoding
  9. Lower bounds for arithmetic miter circuits
  10. Undecidability of the Short Proof Family Problem
  11. Conclusion
  12. Proof of Theorem \ref{['thm:cachesat-pathwidth']}
  13. Proof of Lemma \ref{['lem:cdcl-sim']}
  14. Multiplicative Miter Instances as a special case of Theorem \ref{['thm:proofdoor-main']}
  15. DNF lower bound for $\mathrm{EQ}_n$
  16. ...and 3 more sections

Key Result

Theorem 9

Determining whether an unsatisfiable CNF formula $F$, together with a partition $F = A_1 \wedge \dots \wedge A_k$ and integers $c,w,s$, admits a proofdoor with respect to $c,w$, and $s$ is NP-hard.

Figures (3)

  • Figure 1: Structure of a proofdoor.
  • Figure 2: A partially ordered resolution proof for a formula $\Phi = A(X,Z) \wedge B(Y,Z)$. The green boxes along the dashed line are the "boundary clauses". These boundary clauses only contain $Z$-variables, and together they form an interpolant from $A(X,Z)$ to $B(Y,Z)$.
  • Figure 3: A tree-like arithmetic miter circuit encoding the algebraic inequality $\mathbf{x}(\mathbf{w}+\mathbf{y}+\mathbf{z}) \neq \mathbf{xw}+(\mathbf{xy}+\mathbf{xz})$. If $v$ is chosen to be the (total) $+$ node that outputs $\mathbf{xy}+\mathbf{xz}$, then the variables belonging to $V_{\mathrm{before}}$ are colored in black, the variables belonging to $V_{\mathrm{after}}$ are colored in red, and the variables belonging to $V_{\mathrm{shared}}$ are colored in green.

Theorems & Definitions (34)

  • Definition 1
  • Definition 2
  • Definition 3: Interpolant craig1957three
  • Definition 4: Pathwidth robertson1983graphminors
  • Definition 5: Clause Variable Incidence Graph
  • Definition 6: Clause Absorption atserias2011clause
  • Definition 7: Proofdoor Decomposition
  • Definition 8: Proofdoors
  • Theorem 9: Proofdoor computation is NP-hard
  • Definition 10: Small Proofdoors
  • ...and 24 more