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.

Generators

A generator makes an instance out of parameters alone. One image each, built from the author's own sources at a pinned commit. The programs that start from someone else's artefacts are on the bridges page.

GeneratorAuthorsYearLanguageLicenceImage publishedExact / checkedFamilies
CNFgen Massimo Lauria and contributors2013Python GPL-3.0yes 24 / 24 binary-pigeon-hole, relativized-pigeon-hole
Community Attachment Jesus Giraldez-Cru, Jordi Levy2015C++ none statedno 54 / 56 random-modularity
CRUX miters Armin Biere2021C, then Boolector and aiger none statedno 230 / 230 no competition family recorded
genxormiter Armin Biere2025C MITyes 0 / 0 no competition family recorded
lockchart-to-cnf Nikolaus Riedl-Ehrenreich2025Python CC0-1.0yes 3 / 5 mechanical-master-key
mdp-benchmark Randal E. Bryant2022Python MITyes 28 / 30 minimum-disagreement-parity
Oddball Andrew Mihal2025Python none statedno 40 / 40 oddball-weighing
Round-robin tournament scheduling Joseph Reeves2025Python MITyes 20 / 20 scheduling
sgen1 Ivor Spence2009C none statedno 28 / 30 sgen