SAT Race 2019
Certified UNSAT
Certificates of unsatisfiability have been required for the UNSAT tracks since SAT Competition 2013. This year we will require certificates of unsatisfiablity for all participants.
Although resolution proof formats have been supported in the past,
SAT Race 2019 will only support clausal proofs. The main reason
for this restriction is that no participant in recent years showed any
interest in providing resolution proofs as such proofs as too complicated to
produce and they cost too much space to store.
The proof format of SAT Race 2019 is the same as in 2018, i.e., DRAT (Delete Resolution Asymmetric Tautologies) which is backwards compatible with both RUP (Reverse Unit Propagation) and DRUP. During SAT Competition 2014, a few runs produced proofs of over 100GB, the local storage limit. In order to avoid this issue in 2019, we will also support a binary DRAT format. Details and the checker will be made available on the DRAT website.
The proof should be written into a (text/binary) file called "proof.out", 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 UNSAT a proof in the DRAT format should be written into "proof.out"
- Solution line "s SATISFIABLE" or "s UNSATISFIABLE"
Certified UNSAT solver output example
c this is a solver output example c computing .... c statistics ... s UNSATISFIABLE
Format
Below is 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
A RUP proof is a sequence of clauses that are redundant with respect to the input formula. To 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 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 of verifying 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 the 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 which denotes deletion, or have no prefix expression which stands for clause addition.
Binary Format
Mapping DIMACS Literals to Unsigned Integers
The first step of the binary encoding is mapping literals in the DIMACS format to unsigned integers. The following mapping function is used: map(l) := (l > 0)? 2*l : -2*l + 1. The mapping for some DIMACS literals are shown below. DIMACS literals unsigned integers
-63 127
129 258
-8191 16383
-8193 16387
Variable-Byte Encoding of Unsigned Integers
Assume that 'w0, ..., wi' are 7-bit words, 'w1' to 'wi' all non zero and the unsigned number 'x' can be represented asx = w0 + 2^7*w1 + 2^14*w2 + ... + 2^(7*i)*wi
The variable-byte encoding of DRAT (also used in AIGER) is the sequence of i bytes b0, ... bi:
1w0, 1w1, 1w2, ..., 0wi
/Users/mbassms6/Desktop/satcomp/downloads.html The MSB of a byte in this sequence signals whether this byte is the last byte in the sequence, or whether there are still more bytes to follow. Here are some examples:
unsigned integer byte sequence of encoding (in hexadecimal)
x b0 b1 b2 b3 b4
0 00
1 01
2^7-1 = 127 7f
2^7 = 128 80 01
2^8 + 2 = 258 82 02
2^14 - 1 = 16383 ff 7f
2^14 + 3 = 16387 83 80 01
2^28 - 1 ff ff ff 7f
2^28 + 7 87 80 80 80 01
Bringing it together
In the binary DRAT format, each clause consists of at least two bytes. The first byte expresses whether the lemma is added (character 'a' or 61 in hexadecimal) or deleted (character 'd' or 64 in hexadecimal). The last byte of each lemma is the zero byte (00 in hexadecimal). In between these two bytes, the literals of the lemma are shown as unsigned integers in the variable-byte encoding.In the example below, the plain DRAT format requires 26 bytes (including the new line characters and excluding the redundant spaces in the second lemma), while the binary DRAT format of the same proof requires only 12 bytes. Emiting proofs in the binary format reduces the size on disk by approximatedly a factor of three compared to the conventional (plain) DRAT format.
plain DRAT binary DRAT (in hexadecimal)
d -63 -8193 0 64 7f 83 80 01 00 61 82 02 ff 7f 00
129 -8191 0
Demo
A modified Glucose 3.0 which outputs the proof in a binary format is available. Run it using the command./glucose unsat-benchmark.cnf -vbyte -certified -certified-output=proof.outto produce a binary proof.