SAT benchmark generators, from the competitions and beyond
A benchmark is only reproducible if the program that produced it still runs. This repository packages those programs as Docker images, pins their sources to one commit, and checks each image by regenerating known instances: same GBD hash, same instance. Many of these families were used by the competitions; others were never submitted to one, and serve in papers, in solver tuning or in cube and conquer experiments.
Generators
They make instances out of parameters alone.
CNFgen
Community Attachment
CRUX miters
genxormiter
lockchart-to-cnf
mdp-benchmark
Oddball
Round-robin tournament scheduling
sgen1
Bridges
They encode what another competition distributes, and never redistribute it. See bridges.
Instances nobody submitted
Reproducing what a competition used is one half of the work; making new instances is the other. Every generator page carries sample runs across its parameters, with the size of the formula each one produces, so that a family can be taken further than the dozen instances a competition happened to keep. Those instances are in no database, ours included: they are made on demand.
Generators and bridges
A generator makes an instance out of parameters alone. A bridge starts from an artefact another competition distributes, a circuit of the hardware model checking competition for instance, and encodes it into CNF with a pinned toolchain. We keep the manifest of each upstream collection, with its checksums and its terms, and fetch the files into a local cache: the benchmarks of another competition are never redistributed here.
Where the rankings come from
For the years whose detailed results are published, every solver's runtime on every instance is known, keyed by the same GBD hash we use. That gives, for each benchmark family, the ranking the solvers would have had on that family alone, which is regularly not the overall ranking. See the families.
Years covered: 2023, 2024, 2026 · 42 families with at least eight instances · measure: PAR-2 per instance: the runtime when solved, twice the time limit otherwise.