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.

Packs

A pack is a set of instances we produce and distribute ourselves, because nobody else does. It exists for a stated reason: a paper that needs them, or a collection worth having in CNF as a whole, such as every circuit of a hardware verification competition or every task of a planning one.

Two rules

We never republish what GBD already serves. An instance whose hash is in GBD is linked, not copied. A pack holds what nobody else has: other parameters, other depths, other plan lengths.

The hash is the one GBD uses, the MD5 of the normalised CNF. An instance of a pack is named exactly as a competition instance is, which is what lets the two sit side by side.

The planning competitions of 1998 and 2000 as CNF

The planning competitions distribute PDDL, not formulas, so every SAT author who wants to work on planning rebuilds the same translation and the same encoding. This pack is those instances as CNF, at several plan lengths, produced by one pinned chain: Fast Downward's translator, then the freeLunch encoder. The plan length is what the published SAT competition instances fix to one or two values, and what a solver author needs to vary.

141
instances, none of them in GBD
68 MB
compressed
284
clauses in the smallest
1,573,996
clauses in the largest
curl -LO https://github.com/sat-heritage/benchs-generators/releases/download/packs-2026/ipc-cnf-1998-2000.tar
tar xf ipc-cnf-1998-2000.tar

Produced by Fast Downward translator, then freeLunch compactReinforced, pinned in this repository. The archive carries an index.json giving, for every file, the hash GBD uses, the command that produced it and its size. measured on a sample: a gripper instance at ten steps is 23 thousand clauses, a depots one 399 thousand, and a hundred-block task 61 million. A full pack needs the instances chosen with their size in mind.

The HWMCC 2010 circuits as CNF proposed

A hardware verification competition distributes circuits, not formulas. Every SAT solver author who wants to work on them has to rebuild the same unrolling and the same encoding, and the handful of depths the SAT competitions kept are not enough to study how a solver scales with the depth. This pack is that collection in CNF, at several depths, produced by one pinned chain.

to ask: the circuits are distributed by the competition, the CNF is derived from them by a pinned toolchain