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