# drat-trim

The proof checker [DRAT-trim](https://github.com/marijnheule/drat-trim) can be
used to check whether a propositional formula in the DIMACS format is
unsatisfiable.  Given a propositional formula and a clausal proof, DRAT-trim
validates that the proof is a certificate of unsatisfiability of the formula.
Clausal proofs should be in the DRAT format which is used to validate the
results of the SAT competitions.