Random uniform k-SAT
That category is
limited to usual uniform random k-SAT instances. Only generator
submissions are allowed here. Any generator must be able to produce
many essentially different benchmarks for the same scaling parameters
(given a different random seed).
Applications
Here we should find instances from various applications, such as model checking,
planning, encryption, etc.
These are series of instances, but NOT generators. The instances
here must encode REAL problems.
That category is intended to
provide a snapshot of the current strength of solvers as engines for
SAT based applications.
Crafted (all others)
The benchmarks especially made to give a hard time to the solver. There
will be an award for the smallest instance that cannot be solved by any
solver.
Both instances or instance generators can be submitted. Here, no
UNKNOWN instances. For both satisfiable and unsatisfiable instances,
a proof must be submitted (e.g., a reference to a paper where the
corresponding theorem is proved).
Benchmarks looking-like
uniform random instances that were crafted to be even harder will have
their place in that category this year.
Series
A series is a set of similar benchmarks. For instance, in the random
category, a series of benchmarks is a set of N benchmarks having the
same ratio #clauses/#variables or the same number of variables for
different ratios. This year, all the series will have the same size
(it was not the case in the previous competitions), presumably 10
benchmarks. The size of the series may change according to the number
of submitted solvers and benchmarks.
Classes of instances
We noticed last year that solvers can be
lucky: the results of a given solver on the same benchmark shuffled
with two different random seeds may be drastically different. This
year, each original series will be completed by 2 new series made of
the original benchmarks shuffled with two different random seeds.
This way, we will have some clues about the robustness of the solvers.