Overview of the competition

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

Benchmarks submission rules

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

Selection of benchmarks for the contest

Judges set the total number of benchmarks in each categories. Benchmarks that enter the contest are a mix of old benchmarks and newly submitted ones, randomly selected if needed. The series of random numbers will be reproducible. The initial random seed will be composed by the three random seeds of the judges. If, during the first phase, there is time to enlarge the set of benchmarks, then new benchmarks will be added following the same rules. There will be no shuffling of benchmarks this year. Sat Contest Benchmarks Wheel selection:

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

Solvers submission rules

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.

Competition division

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.

Demonstration division

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.

Who are the winners

Award categories

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).