SAT Competition 2004: Benchmark Submission Guidelines

Submission format

The submission can be a set of instances or a generator of instances. The set of instances should be representative of the problem to be solved at various scale. Generators should provide some parameters to scale the instances.

Generator format

The generator is a program to be launched on a Linux environment with some scaling parameters and a random seed if applicable. (for instance, a random 3-SAT generator will have two scaling parameters (nbvar,nbclauses) and a random seed parameter). It will output the instance on the standard output, using the file format below. The command line parameters will appear in the first commented lines of the instance.

File format

The benchmark file format will be in a simplified version of the DIMACS format:
c
c start with comments
c
c
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

Categories

The benchmarks will be submitted in one of the following categories: Each instance should be submitted as SATISFIABLE, UNSATISFIABLE or UNKNOWN.

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.

Organizing Committee

Laurent Simon (simon@lri.fr) and Daniel Le Berre (leberre@cril.univ-artois.fr)

Contact: SATcompetition@satlive.org

Competition homepage

http://www.satlive.org/SATCompetition/


[SAT Competition 2004] [ SAT 2004 Conference ] [ SAT-Ex] [ SATLIB] [ SAT Live!]