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 47365and 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!
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.
Submission has opened: SAT Competition 2013 Submission System
.
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
- create a folder /binary
- compile or build the code
- copy all necessary executables including scripts to the folder binary
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
50d0d0a7f055da0e72ba9aa089f45640a605c6854dbf0897729b48836da745f2
b9b1d8d1705e35ff47a18ff08ce44ddc