Proof checker for DIMACS proofs
The proof checker 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.
You can contact the maintainers of this package via email at
drat-trim dash maintainers at fedoraproject dot org.