SAT Competition 2013
affiliated with the SAT 2013 conference, July 8-12 in Helsinki, Finland
jointly organized by Ulm University, University of Helsinki,
University College Dublin, University of Texas at Austin,

Important Updates GCC

We have received the information that gcc 4.5.2.(which is the latest version provided by our cluster), might produce buggy code for Minisat and its derivatives (reporting UNSATISFIABLE for SATISFIABLE instances). Further details about the bug:GCC bug 47365
and its effect on the Minisat derivatives: GCC bug triggering wrong behaviour of Minisat
We have installed the newest version of GCC 4.8.0 locally and will use it for the compilation (as it seems to produce also slightly faster code).
If you still want to use the 4.5.2 version of GCC please let us know so that we can compile your solver properly. We could also use an older version 4.3.5 if your code can not be compiled with 4.8.0 and would exhibit the bug under 4.5.2.

Important Updates

  • Please test your build.sh script localy before submitting the code! Buggy build scripts will delay the testing of your solver considerably.
  • Do not compile your code with -m32 if you do not have a strong reason for that.
  • For participants that have or will submit solvers that can provide UNSAT certificates:
    • All solver outputs, including the certification proofs should be written to stdout
    • Add the following line before the output of the proof: "o proof [format]" where format can be one of DRUP, BDRUP or TC (for trace check)
    • Please download the EDACC verifier to test if your solvers output can be correctly processed.

Submission System

Before proceeding with the submission please carefully read the instructions below how to prepare a submission for the competition!

Submission has opened: SAT Competition 2013 Submission System

.
You have to apply for an account on the EDACC system. Once the account has been verified (which can take up to 24h) you are able to perform your solver and benchmarks submission.

Where to submit?

Incomplete solvers (i.e. can not provide UNSAT answers): SAT tracks.
Complete solvers (i.e. can provide UNSAT answers): SAT+UNSAT tracks.
A solver submitted to the SAT+UNSAT tracks, will be automatically eligible to win the according SAT track even if not directly submitted there, because the SAT+UNSAT track entails the SAT track.

Preparation of Solver Submissions

Submission that do not conform to the structure and content mentioned below will not be tested!

Solvers are to be submitted only as source code as stated by the Rules. For a successful submission you will need a pdf file with the solver description and a zip file with the source code of the solver with the following structure and content:
  • /code
  • build.sh
  • readme.txt
  • license.txt
The folder /code should contain the source code of the solver and all necessary scripts to build it. The build.sh script has to accomplish the following tasks:
  • create a folder /binary
  • compile or build the code
  • copy all necessary executables including scripts to the folder binary
The content of the binary folder will be uploaded to the execution system and tested on the test set of the tracks where the solver has been submitted.

The readme.txt file should contain details about the solver (e.g. name, version, authors) and how to build and use the solver, as well as any kind of extra information needed to use the solver.

The licence.txt file should contain the license information. We do not require any particular type of licence, but the minimum requirement for the license is to contain the permission to use the solver for evaluation and research purposes. If you are using source code of other solvers please be sure to also include their license information in your license file.

Preparation of Benchmark Submissions

For a successful benchmark submission we encourage you to first check the instances with a CNF checker which tests the conformity to the DIMACS format. We are providing a checker here. If the instances intended for submission pass the CNF check you are able to directly submit them together with the mandatory benchmarks description (prepared as described in the Rules) as an archive (accepted files: .zip, .tar.gz, .tar.bz2, .7z, .rar, .xz, .tgz) within the submission system. We have a size limitation of 500MB per upload. If your benchmark archive exceeds this limit please create multiple archives and add the benchmark description only to the first one.

MD5 of Organizers Solvers

50d0d0a7f055da0e72ba9aa089f45640
a605c6854dbf0897729b48836da745f2
b9b1d8d1705e35ff47a18ff08ce44ddc