SAT-Race
2010
Rules
These are the official rules for SAT-Race 2010 (version 1.0, last updated on March 31, 2010).Entrants
An entrant to SAT-Race 2010 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 2010 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 as far as possible.
Note for Track 2 (parallel track): We are aware that for many parallel solver implementations it is hard to achieve reproducable runtimes. We will take this into consideration.
Each entrant to the SAT-Race 2010 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 2010 website.
In contrast to former SAT Competitions, it is not required to make source code or binaries publicly available after SAT-Race 2010.
It is highly recommended to use a pre-processor like SatELite to simplify a SAT instance before passing it to the SAT solver core. Evaluation will be based on the combined running time of pre-processor and SAT solver.
Submitters are encouraged to be physically present at the SAT'10 conference. This is, however, not a requirment to participate or win.
Input and Output Format
The input and output format requirements are the same as those used for the SAT Competitions for solvers of the Main Track and Special Track 1 (CNF-based solvers). For Special Track 2 (AIG-based solvers), adherence to the AIG format specification is mandatory; however, no “witness” is required for the solution in case of a satisfiable instance.
Format of Submission
Solvers must be submitted as a ZIP archive. The archive should contain exactly one folder (called root folder in what follows) with this content:
- Program executable or source code. If source code is submitted, there must be a sub-directory src, which also contains a Makefile. The Makefile has to generate an executable which is placed in the root folder.
- The executable program must be called solver (it may also be a BASH script). For entrants to the parallel track (Special Track 1) the executable should be named solver_par, and an additional executable named solver_seq is allowed for running the solver in sequential mode.
- A README file explaining how to use and (if needed) compile the solver.
- All other files must be placed in a sub-directory called ext.
- The solver must not write to any files outside the root folder when run. (Thus, e.g., writing to /tmp is not allowed.) It may, however, use local temporary files stored within the root folder. No assumptions must be made about the absolute path of the solver.
- For the final submission: a 1-2 page system description in PDF format, as described above.
Execution Environment
Programs submitted to SAT-Race 2010 will be run on a compute cluster at the Karlsruhe Institute of Technology (KIT). Compute nodes have the following specification:- Operating System: OpenSuSE 11.1 Linux (kernel 2.6.27), both 32-bit and 64-bit executables supported.
- Processor(s): 2x Quad-Core Intel Xeon E5430, 2.66 GHz.
- Memory: 32 GB (24 GB memory limit for solver processes enforced).
- Cache: 12 MB L2 per Quad-Core CPU.
- Compilers: GCC 4.3.2, javac 1.6.0_12.
Benchmark Selection
The benchmarks for SAT-Race 2010 (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 participating solvers in a sensible time-frame around the Race's threshold run-time. For the qualification round no such restriction applies.
Qualification Round
Before the race there will be a qualification round. Successful participation (i.e. no wrong results; compliance with I/O format requirements; sufficient performance) is mandatory to qualify for SAT-Race. Detailed information on the qualification round can be found here.The Race
The Race itself will take place during or shortly before the SAT'10 conference. Each solver will have to process 100 SAT instances, and each solver is run exactly once on each instance (this also applies to Special Track 1). Per SAT instance and solver a run-time limit of 15 minutes will be imposed. For parallel solvers (Special Track 1) the measured wall-clock time is considered.
Assessment of Solvers
Solvers will be assessed based on the number of instances solved within the run-time limit. If several solvers successfully process the same number of instances, as a second criterion, the cumulated run-time of all solved instances is used to rank the solvers.