SAT solvers now have the ability to produce UNSAT proofs than can be checked efficiently using the DRAT format and associated tools. However, those proofs can still be of challenging size for many instances, essentially because the developpements of SAT solvers was targeting speed and not proof conciseness. The 200TB proof of the Pythagorean triples problem for instance is the larger proof checked so far, even if that proof was not stored directly.
The aim of this challenge is to find a way to reduce the size of those DRAT proofs given by SAT solvers, independently of the problem to solve. The CPU time spent will not be the main crucial resource here. There are several possibilities:
Several of those features are already available in the tool DRAT-trim. Can we go further?
The only constraint of the challenge is that the produced proof must be checkable using the existing checkers DRAT-trim. The proof length will be its size in bytes, represented in the DRAT format, text version (see previous link). Lines starting with deletion tag ('d') will not be considered in the length. Roughly speaking, the measure used will be somehow equivalent to simply use
grep -v '^d' proof.out | wc -c where
proof.out is the proof in text format. Using compressing tools like gzip is ok but only the unflatted proof will be considered for the measure.
The challenge starts at the beginning of the conference (July 5, 9am) and stops at the end of the conference (July 8, 5pm, Paris Time). The winning team will be declared the week after the conference.
Any student (master, PhD) registered to the SAT 2016 conference. Registration to the challenge is done in team of 1 to 3 students. A student may participate to at most one team. In order to participate, students must send an email to
email@example.com before wednesday, 6th of July, 5pm (Paris time).
Money! A €1500 prize will be given to the winning team, to be shared equally among its members.
The teams will provide to the organizers a zip file / tarball containing the source code of a SAT solver able to produce small unsat proofs with all the required dependencies to build it on a linux computer (the SAT solver can be composed by a series of SH scripts to handle the proofs). The tool will be evaluated between July 11 and July 13 on this set of unsat benchmarks taken from the SAT competition 2016. The aim is to still be able to check the produced proofs, but with a much smaller storage footprint.
The team producing the smallest cumulated size of checkable proofs, in KB, will be declared winner. Lines in the proof specifying learnt clause deletion will not be taken into account.
The program can make use of any open source library or tools (e.g. for compression purposes) and any SAT solver available in source for academic purposes compilable in a standard linux computer.
Labri -- Laboratoire Bordelais de Recherche en Informatique
351, cours de la Libération,