Last update: $LastChangedDate: 2009-01-13 13:00:45 +0100 (mar. 13 janv. 2009) $.

Benchmarks submitters are invited to provide a detailed description of the benchmarks, including:

- complete description of the initial problem
- description of the SAT encoding
- expected behavior of the solvers on those benchmarks
- partition of benchmarks into series (when possible)

- In the Industrial and Hand-Made categories, benchmarks are randomly selected according to their hardness (easy, medium, hard). The chance to pick a benchmark of a given hardness will be chosen by the judges and the organizers (for instance 60% chance if it is hard, 30% chance if if is medium and 10% chance if it is easy). This hardness is computed with the help of the performances of a selection of solvers on them (this year, Minisat, RSat and Picosat, in the version of the 2007 SAT Contest, will be used for the industrial category. In the handmade category, Satzilla Crafted, MarchKS and Minisat will be used for this). Final benchmarks will be chosen from a relatively large superset of benchmarks, selected (not randomly) from old and new benchmarks by the judges according to submitter descriptions.
- In the Random category, parameters will be chosen by judges, with the help of organizers. Parameters will take into account recent progress in solver performances. In particular, random SAT formulae will be substantially larger than UNSAT formulae. Effort will be done in trying to ensure that there will as many SAT random instances than UNSAT at the end. Series of instances will contains only benchmarks of different size with the same parameters (K,m,n). The generator will be the classical one, used in previous contests.

Parameters:

Given a set of benchmark C, splitted into series S1, ... SN.

Each benchmark Bi occurs in one and only one series and is scored by its hardness Hi (in "Easy", "Medium" and "Hard").

Pr("Easy") (resp. Pr("Medium") and Pr("Hard")) is a given integer in 0..100 that gives the probability of taking a benchmark scored with this hardness.

O(C) is the ordered set of benchmarks, ordered by their decreasing hardness (Pr(Hi)). Ties are broken at random. Sum(Bi) is the sum of Pr(Hj) s.t. Bj < Bi in this order. Sum(C) is Sum(Bi) s.t. Bi is maximum in the order.

while(final benchmark set is not full)

get a random number N between 0 and Sum(C)

get the first Bi in the order s.t. Sum(Bi) >= N

delete Bi from C and update O(C) and sums accordingly

end while

There are two options to participate in the SAT Competition: by participating in the competition itself or by participating in the system demonstration.

In both cases, a **2 page description** of the solvers
describing the
techniques used, technical issues and **the expected behavior of
the solver**
(e.g., does it only solve satisfiable formulas) should be submitted
together with the solver.

A paper describing the solver might simultaneously be submitted to the SAT 2009 conference or the JSAT journal, unless a published description already exists. However, submission of a paper is independent of submission of a solver and should follow those guidelines.

**Organizers and Technical Advisors of the competiton are allowed
to participate to the competition division provided that they release
the MD5 sum of their solver before the benchmarks submission and
solvers submissions open (1st of march).
They are allowed to participate to the demonstration division with the
same restrictions. **

Solvers in the competition division will be tested in identical execution environments, rated, and compared with each other. There will be winners in various categories.

To enter the competition division, the SAT solver must be submitted in source and with a build script (normally Makefile) that allows the organizers to easily build the SAT solver from source (see solvers requirements for more details). For solvers written in another language than C/C++ or Java, or if you need a specific compiler, please Contact The Organisers.

**The authors must allow the SAT competition organizers to
release the
source code of their solver for research purpose on its web site or
must provide a URL to that source code.**

*Rationale: Every material submitted to the SAT competition will
be available for research purposes after the competition.*

The demonstration division is intended to provide greater flexibility for exposure of solvers when the authors cannot or wish not to comply with the requirements for the competition division.

Solvers in the demonstration division will be tested
in identical execution environments;
they will *not* be rated or compared with other solvers.
There will be *no* winners.
Their results will be recorded and publicized.

To enter the demonstration division, the SAT solver normally should be submitted either as source, with the same guidelines as the competition division, or as a statically linked binary for linux (flag -static).

**The authors normally should allow the SAT competition to
release the binary of their solver for research purpose on its web site
or should provide a URL to that source code.**
**If source is also submitted in the demonstration division, it
is not released without the authors' explicit permission.**

Entries for which the authors do not wish to release either source or binaries for research purposes may be accepted in the demonstration division under special circumstances, at the discretion of the organizers, if it appears that participation will benefit the research community. One possibility is that tests will be run remotely with communication over the internet, at the authors' site. Please ContactTheOrganisers to make special arrangements.

A *Competition category* is the combination of one *Solver
category*
and one *Benchmark category*.

*Solver categories*: SAT, UNSAT, SAT+UNSAT

*Benchmark categories*: Industrial, Hand_crafted, Random.

Series fall within Benchmark categories. Problems fall within Series. "Problems" are synonomous with "Formulas".

OPEN PROBLEMS may be accepted as though they are UNSAT at the discretion of the organizers -- primarily, they should have some kind of theoretical interest, not just be difficult. OPEN PROBLEMS might become a Series.

**For each Competition category, we award the solvers with the
three highest scores (bronze, silver, gold medals).**