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.

Bridges

A bridge does not invent instances: it encodes artefacts that another competition distributes, a circuit of a hardware verification competition for example, with a pinned toolchain. The parameter of the encoding, the depth of an unrolling, is what lets the family scale beyond the handful of instances a SAT competition kept.

Your own files work too

A bridge reads whatever file of its format you give it: mount your directory on /data and it encodes your circuit, not only the ones a competition kept. See your problem.

What we never do

We do not redistribute the benchmarks of another competition. The repository keeps a manifest per collection, with its address, its checksum and its terms, and the files are fetched into a local cache when a bridge runs. The sizes below are what a download costs, not what this project stores.

BridgeCollectionUpstream distributionArchiveExact / checkedTerms
AIGER bridge hwmcc10 Hardware Model Checking Competition 2010 benchmarks 3 MB30 / 31 distributed by the competition; the Intel models are excluded from this archive for licence reasons
AIGER bridge smtqfbv AIGs of the SMT-LIB quantifier-free bit-vector benchmarks 272 MB30 / 31 published by the FMV group next to the AIGER tools, derived from the SMT-LIB benchmarks
freeLunch bridge — — —0 / 0