Call for Benchmarks
SAT Competition 2002
March 10 - May 8, 2002
NEW DEADLINE for benchmark submission: 24 March!
SAT Competition 2002 is going to start on March 10, 2002 and continue
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
good old, but still challenging benchmarks
will be submitted automatically.
We divide instances into the following three categories:
- randomly generated,
- handmade,
- 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 and Paderborn) 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).
To motivate participation an award of US Dollar 2500 (provided by the
computational logic group at Delft) will be allocated to a selection of
solvers and benchmarks. Namely, an award of $350 will be given
to each of the two winners described above.
The allocation of the
remaining money is described in the Call for Solvers.
If there are strictly less than three author groups submitting pools of
satisfiable (resp.,
unsatisfiable) benchmarks eligible for the award,
the award is not given and its pieces will be added to the awards
for the other category. If this happens with the both categories,
the award will be transferred to solvers.
- March, 24: deadline for submitting benchmarks.
- March, 10: deadline for submitting solvers.
- March, 24: buggy solvers returned to the authors.
- March, 31: buggy solvers resubmitted.
- April, 6: 1st stage of the competition starts.
- May, 6 (or earlier): 2nd stage of the competition starts.
- May, 9: results, awards.
http://www.satlive.org/SATCompetition/
[SAT Competition 2002]
[SAT 2002]
[SAT-Ex]
[SATLIB]
[SAT Live!]