Rules

These are the official rules for the SAT Challenge 2012 (Version 1.0, last updated on February 27, 2012).

Entrants

An entrant to the SAT Challenge 2012 is a SAT solver submitted in either source code or binary format using the WWW registration form. Binary format submissions must be compatible with the competition hardware and operating system. Each SAT Challenge 2012 entrant submitted as source code must include a README file explaining how to compile the solver. Execution of solvers must not require root access. Binaries should be statically linked.

In order to obtain reproducible results, SAT solvers should refrain from using non-deterministic program constructs as far as possible. It is allowed to set a random seed value on the command line, however.

Each entrant to the SAT Challenge 2012 must include a short (at least 1, at most 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 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. Furthermore, given that the quality and number of system descriptions is high enough, 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).

In contrast to SAT Competitions, it is not required to make source code or binaries publicly available after the SAT Challenge 2012. We nevertheless encourage all participants to do so.

Submitters are strongly encouraged to be physically present at the SAT'12 conference. This is, however, not a requirement to participate or win.

Input and Output Format

The input and output format requirements are the same as those used for the SAT Competitions and SAT-Races in previous years. More specifically, the requirements of solvers are as specified in the 2011 SAT Competition Rules, Sections 4.1 and 5.1/5.2. Solvers must provide a satisfying truth assignment for satisfiable instances.

Format of Submission

Submissions of solvers have to be either in the form of an executable program or as source code. Details on the submission procedure can be found on the submission page.

Benchmarks have to be formatted according to the SAT Competition 2011 Benchmark Submission Guidelines. A benchmark description, using the IEEE Proceedings style, should be submitted with each submitted benchmark family, following the instructions for solver descriptions. The benchmark descriptions will be made available similarly as the solver descriptions.

Execution Environment

Solvers submitted to the SAT Challenge 2012 will be run on the bwGRiD cluster of the State of Baden-Württemberg, Germany. The cluster nodes have the following specification:

  • Operating System: Scientific Linux (kernel 2.6.18, glibc 2.5), both 32-bit and 64-bit executables supported.
  • Processor(s): 2x Quad-Core Intel Xeon E5440, 2.83 GHz.
  • Memory: 16 GB per node (see also notes below).
  • Cache: 12 MB L2 per Quad-Core CPU.
  • Compilers: GCC 4.1.2, javac 1.6.0.

Available main memory (RAM) and number of CPU cores depend on the Track a solver is registered for:

  • In the three Main Tracks and the Sequential Portfolio Solvers Track: 1 core of 1 CPU and 6 GB of main memory can be used. Two solvers will be run in parallel on each computing node (i.e. one solver per physical CPU). A runtime limit of 900 seconds CPU time will be enforced.
  • In the Parallel Solvers Track 8 cores and 12 GB of main memory will be available. Only one solver will run on each computing node. A runtime limit of 900 seconds wall-clock time will be enforced.

Benchmark Selection

The benchmarks for the SAT Challenge 2012 will be selected randomly out of a pool of SAT instances. This pool will include instances from previous SAT-Races and SAT Competitions, but may also contain additional instances.

For details on how to submit new benchmark problems, see the submission page.

Assessment of Solvers / Ranking

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 (CPU time for sequential solvers, wall-clock time for parallel solvers) of all solved instances is used to rank the solvers.

Prizes

The best solver in each track is awarded a prize. The organizing committee reserves the right to acknowledge additional solvers that produce exceptional results (on pure SAT or UNSAT instances, for instance).

Restrictions

The organization committee reserves the right to restrict participation of a solver to certain tracks, and to allow only a limited number of solvers submitted by the same person. The organizers also reserve the right to submit their own systems or other systems of interest to the competition.

Systems submitted by one of the organizers are not considered in the official ranking and are not able to win a prize.