drat-trim

DRAT-trim is a satisfiability proof checking and trimming utility designed to validate proofs for all known satisfiability solving and preprocessing techniques. DRAT-trim can also emit trimmed formulas, optimized proofs, and TraceCheck+ dependency graphs. DRAT-trim has been used as part of the judging process in the annual SAT Competition in recent years, in order to check competing SAT solvers' work when they claim that a SAT instance is unsatisfiable. This package also contains the related tool LRAT-check, which checks a proof format called LRAT which extends DRAT with hint statements to speed up the checking process.