Benchmarks

Benchmark Submission

We would like to invite and encourage submissions of benchmarks and benchmark generators for all the tracks of the competition.

Each Main Track participant (team) is required to submit 20 new benchmark instances (not seen in previous competitions). At least 10 of those benchmarks should neither be too easy (solvable by MiniSat in a minute) or too hard (unsolvable by the participants own solver within one hour).

A 1-2 page benchmark description document, using the IEEE Proceedings style, must be submitted with each submitted benchmark family. The benchmark descriptions will be made available similarly as the solver descriptions (see general rules).

Benchmark Format

The benchmark file can start with comment lines, i.e. lines beginning with the character c. After the comments, there is the line p cnf nbvar nbclauses that indicates that the instance is in CNF format, where nbvar is the exact number of variables appearing in the file, and 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. A clause must not contain the opposite literals i and -i simultaneously. Positive numbers denote the corresponding variables. Negative numbers denote the negations of the corresponding variables.

Benchmark Selection

The benchmark problems will be selected randomly from the set of benchmarks submitted by the participants and by the organizers.