SAT Competition 2017


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 be "interesting": not too easy (solvable by MiniSat in a minute) or too hard (unsolvable by the participants own solver within one hour on a computer similar to the nodes of the StarExec cluster).

Participants should submit benchmarks by emailing them to "" with the subject "SAT Competition 2017 Benchmark Submission" and either a URL link or attachment of a single zip file containing the benchmarks.

Input and Output Format

Benchmarks have to be formatted according to the SAT Competition 2011 Benchmark Submission Guidelines. A benchmark description, using the IEEE Proceedings style, should be submitted with each submitted benchmark family, following the instructions for solver descriptions. The benchmark descriptions will be made available similarly as the solver descriptions (see general rules).

Benchmark Selection

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

The benchmarks for the Incremental Library Track are applications using a SAT solver in an incremental fashion. See the Incremental Library Track Rules section for more information.

Selected Benchmarks

To get the benchmarks used in the competition go to the downloads page