SAT-Race Logo

SAT-Race
2008

Overview
Rules
Important Dates
Organizers
Qualification
Solvers
Results
Result Analysis
Downloads

Rules

These are the official rules for SAT-Race 2008 (version 1.1, last updated on 03/04/2008).

Entrants

An entrant to the SAT-Race 2008 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 2008 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 1 (parallel track): For many parallel solver implementations it is very hard to achieve reproducable runtimes. Therefore, this requirement does not apply to the parallel track.

Each entrant to the SAT-Race 2008 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 2008 website.

In contrast to former SAT Competitions, it is not required to make source code or binaries publicly available after SAT-Race 2008.

Submitters are encouraged to be physically present at the SAT'08 conference, but are not required to be so 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.

Execution Environment

During SAT-Race 2008 all programs will run on machines with the following specification:
  • Operating System: Scientific Linux 2.6.18, both 32-bit and 64-bit executables supported.
  • Processor(s): 2x Dual-Core Intel Xeon 5150, 2.66 GHz.
  • Memory: 8 GB (7 GB memory limit for solver processes enforced).
  • Cache: 4 MB L2 (shared).
  • Compilers: GCC 4.1.1, javac 1.5.0_11.
In the Main Track and Special Track 2 (sequential solvers) only one core of one processor must be used. Solvers participating in Special Track 1 (parallel solvers) are allowed to use all four cores of the system.

Benchmark Selection

The benchmarks for SAT-Race 2008 (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 rounds no such restriction applies.

Qualification Rounds

Before the race there will be two qualification rounds. Successful participation (i.e. no wrong results; compliance with I/O format requirements; sufficient performance) in at least one of them is mandatory to qualify for the SAT-Race.

The Race

The Race itself will take place during or shortly before the SAT'08 conference. Each solver will have to process 100 SAT instances. Per SAT instance and solver a run-time limit of 15 minutes will be imposed.

Assessment of Solvers

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:

  • For each solved instance a prover gets 1 solution point.

  • For each solved instance—depending on the time the solver needed—additional speed points are distributed: For each instance x points are equally split up among all successful solvers. The resulting number is the maximal speed score (pmax) a solver can obtain, i.e.

    pmax = x / #successful_solvers .

    Then, in a second step, the number of speed points ps each successful solver s obtains is computed by

    ps = pmax · (1 – ts / T) .

    Here ts is the time that solver s needs to solve the instance, and T is the run-time threshold (i.e. 15 minutes). Thus, a solver gets pmax speed points if it solves the instance immediately and 0 points if it solves it at or above the run-time threshold, with linear interpolation in between.

    We will set x in such a way that at most one speed point per solver and instance can be obtained.

    Speed points are motivated by and related to the speed purses of 2005's SAT Competition.

The total score a solver obtains is the sum of its solution and speed points summed over all instances.

Prizes

The solver that achieves the highest score in the Main Track obtains the title "SAT-Race World Champion 2008". Moreover, there will be prizes for the three solvers with highest scores in the Main Track, and for the leading solver of each Special Track. There will also be a special prize for the best solver submitted by a (team of) (PhD) student(s).

Restrictions

Due to limited computational resources, the organizers reserve the right not to accept more than one version (defined as sharing 50% or more of its source code) of the same solver. The organizers also reserve the right to submit their own systems—or other systems of interest—to the competition.