SAT Competition 2013 required UNSAT proofs for the certified UNSAT tracks. Although several formats were supported, all participants chose a format based on RUP (Reverse Unit Propagation). This year we will support only one format, called DRAT (Delete Resolution Asymmetric Tautologies) which is backwards compatible with both DRUP, last years most popular format, and RUP.
All solver outputs should be on stdout, which is redirected in EDACC to file, which is then passed to the verifier.
The output of the solver though should conform to the following rules:
- Comment lines are to be prepended by "c "
- In case of certified UNSAT a proof in the DRAT format
- Solution line "s SATISFIABLE" or "s UNSATISFIABLE"
Certified UNSAT solver output example
c this is a solver output example c computing .... 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 s UNSATISFIABLE
FormatBelow, a brief description of the proof format based on an example formula. The new proof format DRAT is backwards compatible with both the DRUP and RUP formats. More details about DRUP can be found here. 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 proof of the above formula in the RUP (and thus DRAT) format is:
1 2 0 1 0 2 0 0
RUP proofs are a sequence of clauses that are redundant with respect to the input formula. The check that a clause C is redundant, all literals l in C are assigned to false followed by unit propagation. In order to verify redundancy, unit propagation should result in a conflict. The redundant clause is added to the formula in case the check is successful. The conflict clauses clauses produced by conflict-driven clause learning (CDCL) solvers have the RUP property. Therefore, a sequence of all conflict clauses (in the order of learning) is a RUP proof for unsatisfiable formulas.
One important disadvantage of checking RUP proofs is the cost to verify a proof. The DRUP format (Delete Reverse Unit Propagation) was developed to counter this disadvantage. 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.
Some state-of-the-art SAT solvers use techniques, such as extended resolution, that cannot be validated using RUP. The DRAT format (Delete Resolution Asymmetric Tautologies) was developed to deal with this.
1 0 d 1 2 -3 0 d 1 2 0 d 1 3 4 0 d 1 -2 -4 0 2 0 0
The syntax of DRAT proofs is identical to DRUP proofs. Lines contain either a 'd' expression deletion, or have no prefix expression clause addition.