SAT Competition 2002: Automatically submitted benchmarks
The pool of benchmarks used in the competition will be
automatically enriched after the deadline. Depending on the number of
new submitted benchmarks, a greater or smaller number of
good-old benchmarks will be added to the pool.
Families of benchmarks to be added
-
Uniform Random-3-SAT, around the phase-transition
treshold (see for instance "David Mitchell, Bart Selman, and Hector
Levesque. Hard and easy distribution of SAT problems. In Proceedings
of the Tenth National Conference on Artificial Intelligence
(AAAI'92), pages 440-446, 1992", paper can be
found here). Note that we'll use our own generator. Examples and
description of those instances can be found with the
uf/uuf satlib series (note that satex doesn't (currently)
include those benchs). The size of the considered instances will be
substantially larger than those reported in satlib (350 variables at
the treshold is a starting point).
-
"Morphed" Graph Colouring Problems,
Satlib download (some results from satex and
Satlib description )
- DES-encryption, download from F. Massacci original
description, or, preferably, from sim-page,
a compact representation ( results from satex).
- formal-verification
- Hardest benchmarks of satex: In addition to the
previous list of benchmarks, the comittee is free to take the
decision to add a given number of benchmarks, depending on the number
of (new) submitted benchmarks to the competition, in order to obtain
a large enough pool of benchmarks. The precise number will be thus
known after the submission deadline.
As one of the motivation of
such competition is to solve previously unsolved instances, the
comittee will focus on the hardest benchmarks currently represented
in satex, hardness of which will be measured accordingly to current
(i.e. represented in satex) solver performances. More formally, we
may add:
- all the
challenging benchmarks of satex at the date of the benchmark
submission;
- the N hardest benchmarks of satex (N to be fixed after the
deadline, depending on the number of benchmark submission). The
hardness of a given benchmark will be determined by the first
quartile of the cpu-time of all solvers on the considered
bench. This measure expresses that the fastest solvers (namely, the
25% fastest solvers) on this particular benchmark have a cpu time
below this value. Intuitively, this allows to consider only the cpu
time of the fastest solvers (thus forgetting some old/unoptimized
solvers).
Many thanks to satlib, SIM and Joao and Miroslav web pages!
http://www.satlive.org/SATCompetition/
[SAT Competition 2002]
[SAT 2002]
[SAT-Ex]
[SATLIB]
[SAT Live!]