genxormiter
genxormiter [-l | -s | -r | -v] INPUTS [SEED]
What it is
- Authors
- Armin Biere
- Source of the author list
- repository arminbiere/genxormiter
- Language
- C
- Licence
- MIT
- Competitions
- —
- Repository
- https://github.com/arminbiere/genxormiter.git
- Pinned commit
- bc0c9600387a7d8d6b70a84ee17194601092ea70
- Pinned git tree
- 1362e07edbbbfb61db572735efdb91d91094bc16
- Seed
- the second positional argument; without it the generator seeds itself from the clock and the instance cannot be reproduced
- Notes
- the miter between two parity circuits over shared inputs: solvable by XOR reasoning, trivially with -s, and still solvable with -r; -l disables the randomisation of the variable order. Beware of the seed: in this version parse_seed assigns instead of accumulating, so only the last digit of a multi-digit seed is used, and 2, 42, 12 and 102 all give the same instance. Use single-digit seeds until it is fixed upstream.
Build it and run it
docker build -t satex-gen/genxormiter:2025 cnf/genxormiter docker run --rm satex-gen/genxormiter:2025 ... > 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 | ||
|---|---|---|---|---|---|
| 20 shared inputs | 20 7 |
58 | 154 | ||
| 40 shared inputs | 40 7 |
118 | 314 | ||
| 80 shared inputs | 80 7 |
238 | 634 |
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.
| Instance | Family | Command arguments | GBD hash | Level |
|---|