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:
  • The lastest version of our fast DRUP checker (drup-trim.c). It combines backward RUP checking with watch literals to realize efficient performance. Additionally, DRUP-check can exploit clause deletion information in the proof. The description below explains how to add this information to a RUP proof.
  • A compact implementation of a RUP checker (rup-forward.c). This checker is slightly more than 100 lines of code. In contrast to drup-check, rup-forward does not support clause deletion information. Also, it implements forward checking which can be useful for debugging purposes.
Additionally, we implemented a patch for the solvers Glucose version 2.2 and Minisat version 2.2. These patches enable the solvers to emit a DRUP proof (for both the core and simp solvers). To apply the Glucose patch (or Minisat patch), place it in the root directory of Glucose 2.2 (or Minisat 2.2) and run:

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 []:
  1. Negate R_i = [L_{ij}] producing one or more unit clauses, [-L_{ij}].
    For example, the negation of [x, y, z] is [-x], [-y], [-z].
    (When i = r, there are no unit clauses produced.)
  2. Add these unit clauses [-L_{ij}] and R_1 through R_{i-1} to F.
    (When i = r, there are no unit clauses to add.)
  3. Perform unit-clause propagation.
The conflict clauses clauses produced by conflict-driven clause learning (CDCL) solvers have the RUP property. Therefore, one can construct a RUP proof for unsatisfiable formulas by listing all conflict clauses (in the order of learning).

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.


Send updates to: firstname at cs dot utexas dot edu