mdp-benchmark
mdp-gen -n BITS -t THRESHOLD -s SEED
What it is
- Authors
- Randal E. Bryant
- Source of the author list
- repository rebryant/mdp-benchmark and the SAT Competition 2022 benchmark description
- Language
- Python
- Licence
- MIT
- Competitions
- SAT Competition 2022
- Repository
- https://github.com/rebryant/mdp-benchmark.git
- Pinned commit
- 9d7199acc6ae7cedb9f9581c5a0a147351228a84
- Pinned git tree
- 61abbdd6b0cde3f001040e8f2e9a4e9ff3614977
- Seed
- -s; the repository ships src/generate.sh, the script that produced the submitted instances
Build it and run it
docker build -t satex-gen/mdp:2022 cnf/mdp docker run --rm satex-gen/mdp: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.
| Sample | Command arguments | Variables | Clauses | ||
|---|---|---|---|---|---|
| 28 bits, satisfiable | -n 28 -t 7 -s 1 |
803 | 4,478 | ||
| 36 bits, satisfiable | -n 36 -t 9 -s 1 |
1,297 | 7,362 | ||
| 44 bits, satisfiable | -n 44 -t 11 -s 1 |
1,918 | 11,046 |
Reference instances
1 with the no match · 28 with the same GBD hash · 1 with the same number of variables and clauses. 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.
Notes
- parameters from src/generate.sh of the repository: t = n/4 for the satisfiable instance, t = n/4 - 1 for the unsatisfiable one