lockchart-to-cnf

lockchart-gen -l LOCKS [-p POSITIONS] [-d DEPTHS] [-r DENSITY]

What it is

Authors: Nikolaus Riedl-Ehrenreich
Source of the author list: repository nrilu/lockchart-to-cnf and the SAT Competition 2025 benchmark description
Language: Python
Licence: CC0-1.0
Competitions: SAT Competition 2025
Repository: https://github.com/nrilu/lockchart-to-cnf.git
Pinned commit: 6ba6ec0539bab3e690c5e65419315d0dcebf917b
Pinned git tree: 4b7926400c08ba03675770796777e5ec8253f22d
Seed: none; with -r the lock-chart is randomised from the clock and cannot be reproduced
Notes: the script draws the lock-chart after writing the formula, which needs LaTeX and fails in the image; the formula is already complete at that point

Build it and run it

docker build -t satex-gen/lockchart:2025 cnf/lockchart
docker run --rm satex-gen/lockchart: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
11 locks, 4 positions, 3 depths	`-l 11 -p 4 -d 3`	3,432	6,248
15 locks, 4 positions, 3 depths	`-l 15 -p 4 -d 3`	5,736	10,718
20 locks, 4 positions, 3 depths	`-l 20 -p 4 -d 3`	9,300	17,732

Reference instances

3 with the same GBD hash · 2 with the same number of variables and clauses · 15 not checked. 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
lockchart-group1-L190-K276-p8d4j1.normalised.cnf	mechanical-master-key	`-l 190 -p 8 -d 4`	d2af3fde615d… 2.8 MB	not checked
lockchart-group1-L200-K289-p8d4j1.normalised.cnf	mechanical-master-key	`-l 200 -p 8 -d 4`	30f64b3b0870… 3.0 MB	not checked
lockchart-group1-L210-K303-p8d4j1.normalised.cnf	mechanical-master-key	`-l 210 -p 8 -d 4`	89002102bdb8… 3.3 MB	not checked
lockchart-group1-L220-K317-p8d4j1.normalised.cnf	mechanical-master-key	`-l 220 -p 8 -d 4`	fe9b9a35531e… 3.5 MB	not checked
lockchart-group1-L230-K331-p8d4j1.normalised.cnf	mechanical-master-key	`-l 230 -p 8 -d 4`	d99f6ac16292… 3.9 MB	not checked
lockchart-group1-L235-K339-p8d4j1.normalised.cnf	mechanical-master-key	`-l 235 -p 8 -d 4`	a4269b1a0c59… 4.0 MB	not checked
lockchart-group1-L240-K345-p8d4j1.normalised.cnf	mechanical-master-key	`-l 240 -p 8 -d 4`	ee602653c2d6… 2.0 MB	not checked
lockchart-group1-L245-K352-p8d4j1.normalised.cnf	mechanical-master-key	`-l 245 -p 8 -d 4`	955d77fddd1f… 4.6 MB	not checked
lockchart-group1-L250-K359-p8d4j1.normalised.cnf	mechanical-master-key	`-l 250 -p 8 -d 4`	c1dab6f771dd… 5.1 MB	not checked
lockchart-group1-L255-K366-p8d4j1.normalised.cnf	mechanical-master-key	`-l 255 -p 8 -d 4`	a1121f9e7bb4… 5.1 MB	not checked
lockchart-group2-rnd0.3-L18-K36-P8D4J1.cnf	mechanical-master-key	`-l 18 -p 8 -d 4 -r 0.3`	4c0373688643… 49 kB	not checked
lockchart-group2-rnd0.3-L19-K38-P8D4J1_1.normalised.cnf	mechanical-master-key	`-l 19 -p 8 -d 4 -r 0.3`	395829127ec2… 55 kB	not checked
lockchart-group2-rnd0.3-L19-K38-P8D4J1_2.cnf	mechanical-master-key	`-l 19 -p 8 -d 4 -r 0.3`	5d62e4d7ab11… 55 kB	not checked
lockchart-group2-rnd0.3-L19-K38-P8D4J1_3.cnf	mechanical-master-key	`-l 19 -p 8 -d 4 -r 0.3`	3cda1cbfbcab… 56 kB	not checked
lockchart-group2-rnd0.3-L19-K38-P8D4J1_4.cnf	mechanical-master-key	`-l 19 -p 8 -d 4 -r 0.3`	f1973c0a4e96… 54 kB	not checked
lockchart-group3-L11-K23-p4d3j1.normalised.cnf	mechanical-master-key	`-l 11 -p 4 -d 3`	dbb42e010bed… 11 kB	N1
lockchart-group3-L12-K24-p4d3j1.normalised.cnf	mechanical-master-key	`-l 12 -p 4 -d 3`	5321e066293f… 11 kB	N4
lockchart-group3-L13-K26-p4d3j1.normalised.cnf	mechanical-master-key	`-l 13 -p 4 -d 3`	96977e8e00a3… 13 kB	N1
lockchart-group3-L14-K27-p4d3j1.normalised.cnf	mechanical-master-key	`-l 14 -p 4 -d 3`	9c499a4d1fd0… 13 kB	N1
lockchart-group3-L15-K29-p4d3j1.normalised.cnf	mechanical-master-key	`-l 15 -p 4 -d 3`	b99ba7e91132… 15 kB	N4

Notes

parameters read from the file name; the number of keys K follows from the number of locks
parameters read from the file name; the number of keys K follows from the number of locks; the reference file is tens of megabytes
randomised lock-chart: the script seeds Python's random module from the clock, so this instance cannot be reproduced