Description
Proof checker for unSAT proofs.
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.