SAT Competition 2003: 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
- The file can start with comments, that is lines begining with the character c.
- Right after the comments, there is the line p cnf nbvar nbclauses indicating that the instance is in CNF format; nbvar is an upper bound on the largest index of a variable appearing in the file; nbclauses is the exact number of clauses contained in the file.
- Then the clauses follow. Each clause is a sequence of distinct non-null numbers between -nbvar and nbvar ending with 0 on the same line; it cannot contain the opposite literals i and -i simultaneously. Positive numbers denote the corresponding variables. Negative numbers denote the negations of the corresponding variables.
Categories
The benchmarks will be submitted in one of the following categories:
- Random
- Hand-Made
- Applications
Each instance should be submitted as SATISFIABLE,
UNSATISFIABLE or UNKNOWN.
Random
This category will include usual random 3-SAT, backbone controlled, etc.
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).
Hand Made
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).
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.