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 · Families

minimum-disagreement-parity

Solver rankings on this family, and the generator that reproduces it.

What to run on a problem of this kind

The solvers that did best on this family in the SAT Competition 2024, as images of the companion project. They are a better bet on such a problem than the overall winner of that year, which this family often disagrees with.

SolverSolvedCommand
hCaD-bva7 / 17 
docker run --rm -v "$PWD:/data" satex/hcad-bva:2024 your-instance.cnf
hKis-bva7 / 17 
docker run --rm -v "$PWD:/data" satex/hkis-bva:2024 your-instance.cnf
CaDiCaL7 / 17 
docker run --rm -v "$PWD:/data" satex/cadical:2024 your-instance.cnf

Generator: mdp-benchmark

mdp-gen -n BITS -t THRESHOLD -s SEED

28 of 30 instances of this family regenerated exactly. Details and commands.

SAT Competition 2024 · 17 instances

Ranked by PAR-2 on this family alone. Winner of the whole main track that year: kissat-sc2024.

#SolverSolvedPAR-2 per instance
1hCaD-bva 7 / 176362 s
2hKis-bva 7 / 176386 s
3CaDiCaL 7 / 176398 s
4kissat-sc2024 7 / 176548 s
5BreakID-Kissat 7 / 176756 s
6Kissat_MAB_ESA 7 / 176759 s
7Cadical_ESA 7 / 176813 s
8AMSAT 6 / 176870 s
9AMSAT_RGC 6 / 176882 s
10Kissat_MAB_Binary 7 / 177050 s
11hCaD-pbva 6 / 177222 s
12Kissat_MAB-DC 6 / 177326 s