Marijn Heule (joint work with Warren Hunt and Nathan Wetzler,
              to appear in FMCAD 2013)
Trimming while Checking Clausal Proofs
ACL2 Seminar, Oct. 11, 2013

Conflict-driven clause learning (CDCL) satisfiability solvers can emit more
than a satisfiability result; they can also emit clausal proofs, resolution
proofs, unsatisfiable cores, and Craig interpolants. Such additional
results may require substantial modifications to a solver, especially if
preprocessing and inprocessing techniques are used; however, CDCL solvers
can easily emit clausal proofs with very low overhead. We present a new
approach with an associated tool that efficiently validates clausal proofs
and can distill additional results from clausal proofs. Our tool
architecture makes it easy to obtain such results from any CDCL solver.
Experimental evaluation shows that our tool can validate clausal proofs
faster than existing tools. Additionally, the quality of the additional
results, such as unsatisfiable cores, is higher when compared to modified
SAT solvers.