Preliminary Call for Benchmarks
SAT Competition 2003
February - May, 2003
This is a draft version of the Call For Participation
to the SAT2003 competition. Last modification: September 25, 2002.
A new SAT competition is going to start on February 2003 and continue
until May 2003. The results of the competition will be given at the SAT 2003
conference (Italy). That competition follows the SAT Competition 2002 started
on March 10, 2002 and continued until (and during)
SAT 2002 Symposium (May 6-9, 2002, Cincinatti, Ohio, USA).
Contents:
Everyone except Laurent Simon (who can submit before the submission server
is open). .
Any instance of Boolean satisfiability problem that seems to be challenging,
or a set of instances, or a benchmark generator. The format of submission
is described
here. The organizing committee keeps the right of Laurent Simon to reject
any benchmark that
- seems too easy, or
- seems syntactically too hard (say, has 106 variables), or
- seems to be too similar to a well-known benchmark that some solvers
are already able to solve, or
- seems to be too similar to another submitted benchmark (then, the
authors will be asked to merge their submissions).
Note that the following benchmarks remained unsolved during the SAT2002
competition will be submitted automatically.
We divide instances into the following three categories:
- randomly generated,
- handmade (crafted),
- industrial.
See
benchmarks format specification for the details of submitting benchmarks
to each category.
Go to the submission page!
The authors of the smallest benchmarks (in terms of the total number of
literal occurrences) that were not solved by any solver will be declared
winners. There will be two winners: one for a satisfiable benchmark, and
one for an unsatisfiable one. We do not award benchmarks submitted as "unknown"
ones.
The following benchmarks will be excluded from the consideration here:
- Benchmarks based on formulas described in scientific papers
(or other publicly available sources) not authored by the person submitting
these benchmarks, if the description was aimed at presenting hard
formulas for algorithms or proof systems for (UN)SAT or another (co-)NP-hard
problem.
- Benchmarks used in the previous SAT competitions (DIMACS, Bejing, Paderborn,
SAT2002) or benchmarks too similar to these.
- Benchmarks that are publicly available and known to be solved by at
least one solver (even not participating in the competition).
A beautiful certificate, unless some people are willing to provide prizes
to motivate the competition (then please contact the organizers).
- February, 14: deadline for submitting solvers.
- February, 21 (UPDATED): deadline for submitting benchmarks.
- February, 28: buggy solvers returned to the authors.
- March, 7: buggy solvers resubmitted.
- March, 14: 1st stage of the competition starts.
- April, 14 (or earlier): 2nd stage of the competition starts.
- May: results during SAT2003 conference, awards.
Organizing Committee
Laurent Simon (simon@lri.fr) and
Daniel Le Berre (leberre@cril.univ-artois.fr)
Contact: SATcompetition@satlive.org
http://www.satlive.org/SATCompetition/
[SAT Competition 2003 ] [
SAT 2002 ] [SAT-Ex
] [ SATLIB] [
SAT Live!]