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.
Overview · Generators

Round-robin tournament scheduling

rr-gen rr TEAMS ROUNDS | rr-gen mv TEAMS ROUNDS VENUES

What it is

Authors
Joseph Reeves
Source of the author list
repository Aeacu2/RR-Benchmarks and the SAT Competition 2025 benchmark description
Language
Python
Licence
MIT
Competitions
SAT Competition 2025
Repository
https://github.com/Aeacu2/RR-Benchmarks.git
Pinned commit
6735ee973a0f2b0489a2b13fabe3455e90042728
Pinned git tree
2e897d2a1e34376ac8a883176ca00368e9518cb1
Seed
none, the encoding is deterministic
Notes
the submitted scripts keep their instance list at the top of the file; the entry point substitutes the single instance asked for and runs the encoder verbatim

Build it and run it

docker build -t satex-gen/roundrobin:2025 cnf/roundrobin
docker run --rm satex-gen/roundrobin:2025 ...  > instance.cnf

The image can be published: the licence allows it.

What it can produce

A generator is not limited to the instances a competition happened to keep: these are sample runs across its parameters, measured on the built image. Each command was run twice, to see whether it gives the same formula every time.

SampleCommand argumentsVariablesClauses
15 teams, 13 roundsrr 15 13 1,36526,040
18 teams, 16 roundsrr 18 16 2,44857,681
21 teams, 19 roundsrr 21 19 3,990111,930

Reference instances

20 with the same GBD hash. Each line regenerates one known instance, from a competition or from the set its author published; the level says how close the result is. See verification.

InstanceFamilyCommand argumentsGBD hashLevel
MVRoundRobin_n12_d10_v2.cnfscheduling mv 12 10 2 e44a8781cf3e… 40 kB N1
MVRoundRobin_n12_d10_v3.cnfscheduling mv 12 10 3 f1c6af11e777… 64 kB N1
MVRoundRobin_n12_d10_v4.cnfscheduling mv 12 10 4 bf6a49b7bec5… 80 kB N1
MVRoundRobin_n14_d10_v2.cnfscheduling mv 14 10 2 35ec95b9b239… 70 kB N1
MVRoundRobin_n14_d10_v3.cnfscheduling mv 14 10 3 4f0b1a0922f8… 88 kB N1
MVRoundRobin_n14_d10_v4.cnfscheduling mv 14 10 4 008b8c7864ae… 121 kB N1
MVRoundRobin_n16_d10_v2.cnfscheduling mv 16 10 2 c05d4d3ecd06… 108 kB N1
MVRoundRobin_n16_d10_v3.cnfscheduling mv 16 10 3 3a1f1b4b9a52… 132 kB N1
MVRoundRobin_n20_d10_v2.cnfscheduling mv 20 10 2 908433870bee… 203 kB N1
MVRoundRobin_n20_d10_v3.cnfscheduling mv 20 10 3 a07a2796a8a6… 271 kB N1
RoundRobin_n15_d13.cnfscheduling rr 15 13 822cf4daaa4e… 26 kB N1
RoundRobin_n16_d13.cnfscheduling rr 16 13 6cb995b1c550… 29 kB N1
RoundRobin_n16_d14.cnfscheduling rr 16 14 12820b981e6b… 33 kB N1
RoundRobin_n17_d13.cnfscheduling rr 17 13 cb66276897e4… 34 kB N1
RoundRobin_n17_d14.cnfscheduling rr 17 14 78e8f5b0d595… 37 kB N1
RoundRobin_n17_d15.cnfscheduling rr 17 15 53e347648553… 40 kB N1
RoundRobin_n18_d13.cnfscheduling rr 18 13 d66a2e73c7d6… 39 kB N1
RoundRobin_n18_d14.cnfscheduling rr 18 14 46beda38f893… 42 kB N1
RoundRobin_n18_d15.cnfscheduling rr 18 15 6f6a20cd6547… 43 kB N1
RoundRobin_n18_d16.cnfscheduling rr 18 16 a09eb02bbaa7… 49 kB N1

Notes