The programs that produce SAT benchmarks, each as a Docker image: the families the competitions used, and others that live outside them, in papers and in solver tuning.

A pilot, and a collective one: please check, correct and contribute. Everything here is generated from the data of the sat-heritage/benchs-generators repository. A generator whose licence is unknown has its recipe published but no image, and a family with no generator is one we could not find or could not run: corrections, missing generators and licence clarifications are welcome as pull requests or issues. Adding your own generator takes four files, or just an issue with a link to your code: see adding a generator. The companion project for solvers is SAT Heritage.

How a generator is checked

An instance is identified by its GBD hash, the MD5 of the normalised CNF, which ignores comments, header and whitespace. We run the image with the parameters recorded for one competition instance and compare.

The levels

N1same GBD hash
N2same up to the order of clauses
N3same up to a renaming of the variables
N4same number of variables and clauses
--no match

A level below N1 is not necessarily the generator's fault: an archived copy can differ from what its author produced, a set can have been shuffled by the organisers, or a script can have changed after the submission. Those cases are recorded on each generator's page.

Where we stand

GeneratorReferencesCheckedExact
AIGER bridge313130
AIGER bridge313130
CNFgen242424
Community Attachment565654
CRUX miters230230230
freeLunch bridge000
genxormiter000
lockchart-to-cnf2053
mdp-benchmark303028
Oddball404040
Round-robin tournament scheduling202020
sgen1303028

Reproduce it yourself

git clone https://github.com/sat-heritage/benchs-generators.git
cd benchs-generators
python3 tools/check_repo.py                  # no Docker needed: the recipes hold together
docker build -t satex-gen/gbd:0.4.2 tools/gbd
docker build -t satex-gen/sgen1:2009 cnf/sgen1
python3 tools/verify.py sgen1

The verifier regenerates every reference instance of the target and prints one line per instance. Hashes are computed with the official gbdc package of GBD.