DRABT Proof Checker

This site provides access to our DRABT proof checker for the DRAT proof format. It can be considered an indepedent reimplementation of DRAT-trim with almost the same funcationality including the use command line options, except that currently DRABT only supports forward DRUP proof checking without core extraction.

However, DRABT directly supports compositional proof checking as described in our 2015 LPAR-20 paper Compositional Propropositional Proofs and further provides has much more verbose diagnostic messages for failing proofs.

The latest public release, supports the binary proof format version of DRABT. It will also work with clauses with duplicated literals, but gives a warning if the CNF has clauses with duplicated literals. Finally it has support for 'xz' compressed DIMACS or DRAT files.

For this paper you might also want to check out the complete set of experimental data available at http://www.cs.utexas.edu/~marijn/cpp.

[ drabt-004.tar.bz2 | NEWS  | USAGE  | README  | LICENSE ]

As background material to proof checking for SAT solvers please refer to our APPA'14 paper Proofs for Satisfiability Problems, the DRAT-trim or TraceCheck pages.