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.

Benchmark families

Every family of the covered competitions with at least eight instances, the solver that did best on it in the most recent of those years, and the generator that reproduces it when we have one.

42
families
2
with a generator here
40
still without one
FamilyYearsInstancesBest solver on itGenerator
allowable-seqence 202616 oertel_satsuma-lex-ae-kissat-mab 14 solvednone here yet
argumentation 2023, 2024, 202621 yalun_kissat-eda-1 15 solvednone here yet
boxfolding 202616 anders_satsuma-iter-kissat 13 solvednone here yet
brent-equations 202319 Cadical_rel_1.5.3.Scavel 19 solvednone here yet
cryptography 20249 Kissat_MAB_ESA 8 solvednone here yet
cryptography-ascon 202320 SeqFROST 20 solvednone here yet
cryptography-simon 2023, 202417 kissat-sc2024 10 solvednone here yet
cyclic-anti-bandwidth 202616 zheng_kissat-mab-hypre 11 solvednone here yet
ecc-equivalence-checking 202610 zhenwei_mergesat 10 solvednone here yet
exam-scheduling 202612 zheng_kissat-mab-hypre 12 solvednone here yet
graph-coloring 202625 anders_satsuma-iter-kissat 22 solvednone here yet
grs-fp-comm 202317 hKissatInc-unsat 15 solvednone here yet
hardware-miter 202442 kissat-sc2024 35 solvednone here yet
hardware-verification 20238 hKissatInc-unsat 7 solvednone here yet
hashtable-safety 202320 Kissat_MAB_prop 20 solvednone here yet
heule-folkman 202411 kissat-sc2024 11 solvednone here yet
heule-nol 202411 AMSAT 11 solvednone here yet
independent-set 202415 hKis-bva 7 solvednone here yet
interval-matching 202320 Kissat_MAB_prop_pr-no_sym 20 solvednone here yet
knights-tour 202440 kissat-sc2024 40 solvednone here yet
linear-equations 202612 anders_satsuma-iter-kissat 0 solvednone here yet
maxsat-optimum 202413 Kissat_MAB_ESA 13 solvednone here yet
minimum-disagreement-parity 202417 hCaD-bva 7 solvedmdp-benchmark
miter 202311 Kissat_MAB_prop 8 solvednone here yet
multiplier-circuit-miters 202612 yalun_kissat-eda-4 12 solvednone here yet
mutilated-chessboard 202312 Kissat_MAB_prop_pr-no_sym 11 solvednone here yet
ntil 202616 anders_satsuma-iter-ae-kissat-mab 10 solvednone here yet
profitable-robust-production 202320 CaDiCaL_vivinst 17 solvednone here yet
quantum-kochen-specker 202410 kissat-sc2024 10 solvednone here yet
random-circuits 202415 kissat-sc2024 14 solvednone here yet
register-allocation 202320 Kissat_MAB_prop-no_sym 20 solvednone here yet
satcoin 202315 SeqFROST-NoExtend 15 solvednone here yet
scheduling 202450 AMSAT 35 solvedRound-robin tournament scheduling
school-timetabling 2023, 202619 yalun_kissat-eda-1 10 solvednone here yet
set-covering 202320 AMSAT_ 20 solvednone here yet
social-golfer 202320 SeqFROST 7 solvednone here yet
software-verification 202415 Kissat_MAB-DC 15 solvednone here yet
stable-semantics 202612 oertel_satsuma-lex-ae-kissat-mab 12 solvednone here yet
syndrome-decoding 202612 anders_satsuma-iter-ae-kissat-mab 9 solvednone here yet
tseitin 202310 MiniSat+XorEngine 7 solvednone here yet
van-der-waerden 202612 oertel_satsuma-lex-kissat 8 solvednone here yet
xor-shifting 202611 zheng_kissat-mab-hypre 1 solvednone here yet