Mandatory participation requirements for SAT solvers
- The source code of submitted SAT solvers must be made available (licensed for research purposes).
- A 1-2 page description (IEEE format, as per SC2012) must be submitted together with the solver (see template).
- SAT solvers must conform to DIMACS input/output requirements (see SC11 for details).
- SAT solvers that are planning to participate in pure UNSAT tracks must be able to produce certificate in tracecheck or RUP (reverse unit propagation) format.
Mandatory participation requirements for benchmarks
Submitted benchmarks must be accompanied by a 1-3 page description (IEEE format, SC 2013 specific template with instructions on contents is available here). This should include a list of all authors of the system and their present institutional affiliations. It should also provide details of any non-standard algorithmic techniques (e.g., heuristics, simplification/learning techniques, etc.) and data structures. The system description must be formatted in IEEE Proceedings style, and submitted as PDF. The system descriptions will be posted on the SAT Challenge 2012 website. Following SAT Challenge 2012, the organizers are considering publishing the collection of system description as a report under the report series of Department of Computer Science, University of Helsinki (with ISSN and ISBN numbers).
Qualification
There will be no qualification round, but only a testing round to ensure that solvers are running properly on the evaluation system. The test set of instances will consist in a random selection of instances from the last SAT Competitions. The organizers reserve the right to disqualify poorly performing solvers.
Disqualification
A SAT solver will be disqualified if the solver produces a wrong answer. Specifically, if a solver reports UNSAT on an instance that was proven to be SAT by some other solver, or SAT and provides a wrong certificate. A solver disqualified from the competition is not eligible to win any award. Disqualified solvers will be marked as such on the competition results page.
Note that there is a dedicated period when the participants can check their results to ensure that no problems are caused by the competition framework.
Certified UNSAT tracks
In contrast to earlier SAT competitions, the sequential UNSAT tracks for core solvers are certified. In order to participate in these tracks, solvers are required to emit an unsatisfiability proof. The tracks will support the two most popular unsatisfiability proof formats: tracecheck and RUP (reverse unit propagation). In the UNSAT tracks, only benchmarks are counted for which the solver emitted a proof that can be verified by a checker provided by the organization. A proof that is discarded by the checker will not result in disqualification of the solver.
Withdrawal
A solver can be withdrawn from the SAT Competition 2013 only before the deadline for the submission of the final versions (30 April). After this deadline no further changes or withdrawals of the solvers are possible.
Participation of the organizers
Organizers that want to participate must publish a MD5 hash number of the archive of their source code strictly before April 21.
The version entering the contest must be the same. The goal is to prove publicly that organizers submitted their solver before having access to any solver or benchmark submitted to the competition.
Number of submissions
In each track, an author may not submit more than 2 different solvers. Two solvers are different as soon as their sources differ or as soon as the command line arguments used for running the solver or the compilation options used to compile it are different.