SAT 2004 Competition: Call for Benchmarks
SAT Competition 2004
February - May, 2004
Last modification: January 30, 2003.
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
Note that the following benchmarks remained unsolved during the
previous SAT2002 and SAT2003 competitions (so-called challenging
benchmarks) will be submitted automatically.
- seems too easy, or
- seems syntactically too hard (say, has 1010 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).
We divide instances into the following three categories:
See benchmarks format specification
for the details of submitting benchmarks to each category.
- randomly generated uniform k-SAT,
- applications (old "industrial" category)
- crafted (all others)
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"
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,
SAT2003) 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,10 : solver/benchmark registration (register here)
- February, 23 : deadline for submitting solvers. (updated)
- February, 23 : deadline for submitting benchmarks.(updated)
- February, 24 : 1st stage of the competition starts.(updated)
- April, 8th (or earlier): 2nd stage of the competition starts.
- May 10-13: results during SAT2004 conference, awards.
Laurent Simon (email@example.com) and
Daniel Le Berre (firstname.lastname@example.org)
[SAT Competition 2004] [
SAT 2004 Conference ] [
SAT-Ex] [ SATLIB] [