SAT Competition 2016


Selected Benchmarks

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

Input and Output Format

The input and output format requirements are the same as those used for the SAT Competitions.

Benchmark Submission

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

The submission of benchmarks is done via email to Please pack your benchmarks files or generator in a zip archive and attach it to your email. Please also include a short description of the submitted benchmark set and indicate which of the following six labels is most fitting for your benchmark set

Benchmark Selection

In the 2016 SAT Competition we will use 600 benchmark problems selected from newly submitted and previous competition benchmarks in the following way.

  1. We split the benchmarks into the following six categories
    • Software verification
    • Hardware verification
    • A.I. Apllications (planning, scheduling, ...)
    • Obstruction (small hard crafted problems)
    • Combinatorial Challenges
    • Theorem proving
  2. We will select 100 benchmarks from each category such that:
    • around half of the benchmarks is satisfiable
    • there are no too easy benchmarks (solvable by MiniSat 2.2.0 under 600 seconds)
    • around half of the benchmarks is not too hard (A benchmark is not too hard if it can be solved under 600 seconds by at least one of the winners of the 2015 SAT Race Parallel Track (Glucose-Syrup, Treengeling, Plingeling) using 8 cores).

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.