Download RUPkit.tar (13230080 bytes) for tools to verify RUP proofs
generated by your SAT solver.

Or go to the directory RUPkit to look at what's in the tar file,
and download them individually or with wget.

Besides the programs, it contains several sample files, csh scripts,
and 3 test files, with outputs.
testeq.cnf is small enough to examine completely and check by hand.

Notice that the *.rup in this directory do NOT have the 256-byte header
specified in the fileformat_rup.txt document.  rupToRes accepts this,
but it's a good idea to provide that header to avoid mixups.
Here is a command to make a newline terminated file exactly 256 bytes
(be careful to use single and double quotes as shown -- assumes csh or tcsh syntax):

cat hdr_any | awk '{f=f $0;}END{printf "%-255s\n",substr(f,1,255);}' > hdr256

This is all tested on Linux Red Hat, but rupToRes could have some bugs
in cases that did not arise during my tests.
I will try to help resolve any problems you encounter, if you are
participating in the verification track of SAT 2007.

See BUG.LIST in this directory for bugs and work-arounds.

Because the verification track is very experimental, I will be more
flexible than the main tracks about the forms of submission.

If you want to submit a solver that uses one of the 2005 formats,
that's OK too.  The specs are in this directory.
Please note that the 2005 format makes much longer files than the new
RUP format.  In C you might need to use cbigopen.{c,h} to create a file
more than 2 GB.  These files are in RUPkit.tar and are used by checker3.c.

--Allen Van Gelder