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

freeLunch bridge

freelunch-bridge DOMAIN.pddl PROBLEM.pddl METHOD MAKESPAN | freelunch-bridge TASK.sas METHOD MAKESPAN | freelunch-bridge --list

What it is

Authors
Tomas Balyo and Vojtech Bardiovsky
Source of the author list
the headers of the freeLunch sources and the repository biotomas/freelunch
Language
Java, with the Fast Downward translator in Python
Licence
GPL-3.0
Competitions
SAT Competition 2016 and 2017, as the planning family of Tomas Balyo
Repository
https://github.com/biotomas/freelunch.git
Pinned commit
4f2c89ac3af95408baae4724028ed9d533bb3524
Pinned git tree
3f08fc32c58205df94eceaa52c8c6ecd4e15af2f
Seed
none: the encoding of a given task at a given makespan is deterministic, and two runs give the same formula
Notes
takes a planning problem and asks whether a plan of a given length exists. Give it two PDDL files and Fast Downward's translator turns them into the SAS+ format first; give it a SAS+ task and it encodes it directly. The makespan is the parameter that makes the family scale, as the depth does for an unrolling: on the gripper problem it goes from 1649 clauses at four steps to 4313 at twelve. Methods: the competition instances use exist, written ex in their names, and compactReinforced, written cr. Open question: the planning instances of the competitions cannot be reproduced here. Their tasks were submitted in 2016 and 2017, the public history of freeLunch starts in December 2017, and the exist encoder of the current code fails on the three tasks we have with a null pointer. The compactReinforced encoder works, but no competition instance uses it on a task the repository carries.

Build it and run it

docker build -t satex-gen/freelunch:2022 bridges/freelunch
docker run --rm satex-gen/freelunch:2022 ...  > 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
barman, a plan of 5 steps--builtin barman-pfile06-022.sas cr 5 16,410585,379
barman, a plan of 7 steps--builtin barman-pfile06-022.sas cr 7 21,880780,591
barman, a plan of 9 steps--builtin barman-pfile06-022.sas cr 9 27,350975,803

Reference instances

. 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