We implemented an improved checker, called DRAT-trim, which is backwards compatible with DRUP-trim, faster than DRUP-trim, and contains several new features. For example, DRAT-trim can validate proofs with extended resolution. We advice users of DRUP-trim to upgrade to DRAT-trim. |
DRUP checker
Reverse unit propation (in short RUP) is a popular method to verify
refutations produced by satisfiability (SAT) solvers. The idea is originates from [1].
RUP proofs can easily be obtained from most conflict-driven clause learning SAT solvers.
Certifying UNSAT proof tracks have been organized for the SAT competitions in
2007,
2009, and
2011.
Probably the most important disadvantage of the RUP approach is the computational costs to validate a given proof. In order to reduce this disadvantage, we propose to add clause deletion information to the proof. Clause deletion is one of the features that allow SAT solvers to have strong performance. By communicating this information to a RUP proof checker, one can significantly reduce the costs to validate a proof. We refer to our proposed format as DRUP (delete RUP). Details about the format are described below. [1] E.Goldberg, Y.Novikov. Verification of proofs of unsatisfiability for CNF formulas. Design, Automation and Test in Europe. March 2003, pp. 886--891. |
Citing this work
If you would like to reference DRUP or DRUP-trim in a publication, please cite the following paper:
Heule, M.J.H., Hunt, Jr., W.A., and Wetzler, N. Trimming while checking clausal proofs. Formal Methods in Computer-Aided Design (FMCAD). IEEE (2013) 181-188 |
Downloads
We implemented two checkers for (D)RUP proofs:
patch -p1 < DRUPglucose.patch or for Minisat patch -p1 < DRUPminisat.patch After applying the patch, one can output a DRUP proof as follows: ./glucose FORMULA PROOF or for Minisat ./minisat FORMULA PROOF |
Usage
To make the executable, download the file above and compile it:
gcc drup-trim.c -O2 -o drup-trim To run the checker: ./drup-trim FORMULA PROOF [CORE] with FORMULA being a CNF formula in DIMACS format and PROOF a proof for FORMULA in the DRUP format (see details below). Additionally one can specify a file CORE containing the unsatisfiable core in DIMACS format. |
Example
Below, a brief description of the DRUP format based on an example formula. The spacing in the examples is to improve readability. Consider the following formula in the DIMACS format. |
p cnf 4 8
1 2 -3 0
-1 -2 3 0
2 3 -4 0
-2 -3 4 0
1 3 4 0
-1 -3 -4 0
-1 2 4 0
1 -2 -4 0
A compact RUP proof for the above formula is: |
1 2 0
1 0
2 0
0
The method of deriving the redundant clauses in the proof is not important.
It might be by resolution or some other means.
It is only necessary that the soundness of the redundant clauses can be
verified by a procedure called REVERSE UNIT-PROPAGATION (RUP for
short). In the discussion, clauses are delimited by square brackets. Suppose that F is the input formula and R_1, ..., R_r are the redundant clauses that have been produced by the solver, with R_r = [] (the empty clause). The sequence R_1, ..., R_r is an RUP refutation of F if and only if: For each i from 1 through r, steps 1--3 below derive []:
One important disadvantage of checking RUP proofs is the cost to verify a proof. To counter this disadvantage, we propose the DRUP format (delete reverse unit propagation). The DRUP format extends the RUP format by allowing it to express clause elimination information within the proof format. |
1 2 0
d 1 2 -3 0
1 0
d 1 2 0
d 1 3 4 0
d 1 -2 -4 0
2 0
0
Apart from the redundant RUP clauses, a DRUP proof may contain lines with a 'd' prefix. These lines refer to clauses (original or learned) that can be deleted without influencing the proof checking. In the above example, all the deleted clauses are subsumed by added RUP clauses. In practice, however, the clauses that one wants to include in a DRUP proof are the clauses that are removed while reducing the (learned) clause database. |