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.

You have a problem; what do you run?

The bridges here are not tied to the competitions: they encode any file of the formats they understand, yours included. Encode your problem, then pick the solver that does best on problems of that kind rather than the one that won overall.

Step one: turn it into CNF

What you haveHow
A circuit in AIGER format, combinationalreadybridges/aiger 
docker run --rm -v "$PWD:/data" satex-gen/aiger:2021 cnf mycircuit.aig > mine.cnf
A sequential model to unroll over k steps, bounded model checkingreadybridges/aiger 
docker run --rm -v "$PWD:/data" satex-gen/aiger:2021 unroll 20 mymodel.aig > mine.cnf
Two circuits whose equivalence you want to checkreadybridges/aiger 
docker run --rm -v "$PWD:/data" satex-gen/aiger:2021 miter a.aig b.aig > mine.cnf
A planning problem in PDDL, domain and problemreadybridges/freelunch, through Fast Downward's translator 
docker run --rm -v "$PWD:/data" satex-gen/freelunch:2022 domain.pddl problem.pddl cr 12 > mine.cnf
A planning task already in SAS+readybridges/freelunch 
docker run --rm -v "$PWD:/data" satex-gen/freelunch:2022 task.sas cr 12 > mine.cnf
A constraint problem in XCSP3 or MiniZincplanneda bridge over Savile Row or a Picat encoding
A bit-vector formula in SMT-LIBpartlythe circuits of the SMT-LIB benchmarks are already there; encoding your own formula needs Boolector or Bitwuzla in the chain, as the CRUX recipe does

Mount the directory holding your file on /data and the image reads it there. Nothing is uploaded anywhere: the whole chain runs on your machine.

Step two: pick a solver

The best three of the SAT Competition 2026 overall, as images of the companion project.

SolverSolvedCommand
anders_satsuma-iter-kissat276 of 400 
docker run --rm -v "$PWD:/data" satex/satsuma-iter-kissat:2026 mine.cnf
anders_satsuma-iter-ae-kissat-mab269 of 400 
docker run --rm -v "$PWD:/data" satex/satsuma-iter-ae-kissat-mab:2026 mine.cnf
zheng_kissat-mab-hypre257 of 400 
docker run --rm -v "$PWD:/data" satex/kissat-mab-hypre:2026 mine.cnf

Step three, the one that pays: find your family

A solver that wins overall is not the one to run on every kind of problem. On the Ascon cryptography family of 2023, SeqFROST solved all twenty instances while the overall winner did not; on the 2024 scheduling family, AMSAT solved more than the winner. If your problem resembles one of the families of the competitions, the families page gives the ranking on that family alone and the command for each solver.

If your problem resembles nothing there, that is interesting in itself: a new family is exactly what a competition is short of, and the issues are the place to say so.