Two years ago, the SAT competition organized a special track on certified unsat answers. Allen Van Gelder designed for that purpose a proof format and a proof checker. Two solvers participated to that special track (namely zChaff and TTS). (See http://www.satcompetition.org/2005/presentation-last.pdf for details). The main issue with certifying unsat proofs was the size of the proofs (several GB for easily solvable unsat benchmarks). As a consequence, a lot of space was needed to run such a special track, a very specific system configuration was needed to allow the SAT solver to manage so huge files, and a huge amount of main memory was needed to check the proofs afterward. Recently, Allen improved drastically his unsat proof framework (he will present that work during the SAT 2007 conference). The size of the proof is an order of magnitude smaller than previously, and thanks to the 64 bits architecture, checking the proof is now much easier. The new proof format (called Reverse Unit Propagation) is supposed to be easy to implement in a SAT solver. (I have to admit I did not try to implement it yet :)) We are seeking people willing to give the unsat proof format a trial in order to: - - push forward a common unsat proof format for SAT solvers - - receive feedback on the implementation of the proposed proof format Allen would like to run those solvers on unsat benchmarks from the SAT competition on a specific computer with enough hard drive and main memory capacity and to report the results of his experiments during the SAT conference. All the details regarding the proof format and several tools to check the proofs are available from: http://www.soe.ucsc.edu/~avg/ProofChecker/ Be sure to download README, fileformat_rup.txt, and RUPkit.tar to start. Submission procedure: Just send an email to unssattrack@satcompetition.org with the Estimated Time of Availability of your solver. A statically compiled solver for 32 bits architecture is the preferred format. For any question related to that call for solver, please send an email to unssattrack@satcompetition.org. Cheers, Daniel