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

seems too easy, or
seems syntactically too hard (say, has 10¹⁰ 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 previous SAT2002 and SAT2003 competitions (so-called challenging benchmarks) will be submitted automatically.

We divide instances into the following three categories:

randomly generated uniform k-SAT,

applications (old "industrial" category)

crafted (all others)

See benchmarks format specification for the details of submitting benchmarks to each category.

How to submit?

Go to the submission page!

Who are the winners?

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