DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs

Joint work with Marijn Heule and Warren Hunt, Jr.

ACL2 Seminar, 5/16/2014

Abstract:

The DRAT-trim tool is a satisfiability proof checker based on the new
DRAT proof format. Unlike its predecessor, DRUP-trim, all presently
known SAT solving and preprocessing techniques can be vali- dated
using DRAT-trim. Checking time of a proof is comparable to the running
time of the proof-producing solver. Memory usage is also simi- lar to
solving memory consumption, which overcomes a major hurdle of
resolution-based proof checkers. The DRAT-trim tool can emit trimmed
formulas, optimized proofs, and new TraceCheck+ dependency graphs. We
describe the output that is produced, what optimizations have been
made to check RAT clauses, and potential applications of the tool.