Abstract
As the name suggests, "extended resolution" builds on the standard resolution proof framework by allowing proofs to introduce new "extension" variables that serve as abbreviations for Boolean formulas over the input and previous extension variables. The DRAT proof format, used by SAT solvers to encode unsatisfiability proofs, supports extended resolution.
Theoreticians find extended resolution interesting, because it enables polynomial-sized proofs of problems that otherwise require exponential ones. On the other hand, practitioners have not made much use of this capability. Standard CDCL solvers insert extension variables into their proofs only during some of their pre- and in-processing steps.
Our recent work demonstrates that extended resolution allows the integration of a variety of other reasoning methods into proof-generating SAT solvers, both to operate on their own and to work cooperatively with CDCL. These include: using Gaussian elimination to reason about parity constraints, pseudo-Boolean solvers to reason about cardinality and other constraints, and integrating Ordered Binary Decision Diagrams (BDDs) into the solver.
Our work demonstrates a capability that we believe could be carried much further, yielding SAT solvers that employ a variety of techniques, while generating proofs of unsatisfiability in the standard DRAT format.