RulesThese are the official rules for the SAT-Race 2006 (version 1.0, last updated on 08/08/2006).
An entrant to the SAT-Race 2006 is a SAT solver submitted in either source code or binary format using the Web registration form. Binary format submissions must be compatible with the competition hardware and operating system. Each SAT-Race 2006 entrant must include a README file explaining how to (compile and) install the solver. Installation and execution of solvers must not require root access. Binaries should be statically linked. The organizers will make reasonable efforts to install each system, including communication with the submitters of the system in case of difficulties. Nevertheless, the organizers reserve the right to reject an entrant if its compilation or installation process proves overly difficult. In order to obtain reproducible results, SAT solvers should refrain from using non-deterministic program constructs.
Each entrant to the SAT-Race 2006 must include a short (1-2 pages) description of the system. This should include a list of all authors of the system and their present institutional affiliations. It should also describe any algorithms or data structures that are not standardly used in such systems. System descriptions will be posted on the SAT-Race 2006 website.
In contrast to former SAT Competitions, it is not required to make source code or binaries publicly available after SAT-Race 2006.
We have set up a discussion forum for the SAT-Race and strongly encourage participants to use this forum, e.g. to find answers to frequently asked questions or to discuss with co-competitors.
Submitters are encouraged to be physically present at SAT-Race 2006, but are not required to be so to participate or win.input and output format requirements are the same as those used for the SAT Competitions.
The benchmarks for the SAT-Race 2006 (as well as for the qualification rounds) will be selected randomly out of a pool of SAT instances. This pool mainly consists of instances from the industrial category of previous SAT Competitions, but may also contain a smaller fraction of new instances stemming from applications with industrial relevance.
To obtain benchmarks of suitable difficulty we select only such instances that can be solved by at least one of the top ten SAT-Solvers of last year's SAT Competition (industrial category) in a sensible time-frame around the Race's threshold run-time.
Solvers will be assessed based on a score that takes into account (1) the number of instances solved within the run-time limit and (2) the total time needed to solve all instances.
The exact assessment scheme is as follows: