Aim

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:

• balancing the solver effort from CPU time to proof length
• introducing new variables (extended resolution)
• reducing the among of information given by the solver
• cleaning the proof while the solver is running
• etc.

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.

Who is elligible?

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 sat2016@easychair.org before wednesday, 6th of July, 5pm (Paris time).

What is the prize?

Money! A €1500 prize will be given to the winning team, to be shared equally among its members.

How to win?

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.

Which tools can I use?

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.