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 in the Main track.
Although resolution proof formats have been supported in the past, this SAT Competition will only support clausal proofs. The main reason for this restriction is that no participant in recent years showed any interest in providing resolution as such proofs as too complicated to produce and they cost too much space to store.
The proof format of this SAT Competition is the same as in 2014, 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. Thus, 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:

The solution line can appear anywhere in the output of the solver, though the solution "v ..." in case of SAT should appear after the solution line "s SATISFIABLE" as it is the case in the original specification

Certified UNSAT solver output example

	c this is a solver output example
	c computing ....
	c statistics ...
	s UNSATISFIABLE

Format

Below, 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.

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 as

    x = 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

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