CNFgen

cnfgen FAMILY PARAMETERS...; cnfgen --help lists the families

What it is

Authors: Massimo Lauria and contributors
Source of the author list: project page massimolauria.net/cnfgen and PyPI
Language: Python
Licence: GPL-3.0
Competitions: —
Repository: https://pypi.org/project/cnfgen/0.9.6/
Seed: random families take a seed option; Python's random module does not promise identical draws across Python versions
Licence note: GPL-3.0: the image is publishable provided its sources travel with it, which the pinned PyPI release and the recorded version give

Build it and run it

docker build -t satex-gen/cnfgen:0.9.6 cnf/cnfgen
docker run --rm satex-gen/cnfgen:0.9.6 ...  > 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
pigeonhole 10 on 9	`-S 1 php 10 9`	90	415
pigeonhole 14 on 13	`-S 1 php 14 13`	182	1,197
pigeonhole 18 on 17	`-S 1 php 18 17`	306	2,619
Tseitin, 4-regular, 40 vertices	`-S 1 tseitin 40 4`	80	320
Tseitin, 4-regular, 80 vertices	`-S 1 tseitin 80 4`	160	640

Reference instances

24 with the same GBD hash. 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
bphp_p23_h22.sanitized.cnf	binary-pigeon-hole	`-S 1 bphp 23 22`	fa5c6d6736a4… 9 kB	N1
bphp_p51_h50.sanitized.cnf	binary-pigeon-hole	`-S 1 bphp 51 50`	d6bb07788867… 65 kB	N1
bphp_p67_h66.sanitized.cnf	binary-pigeon-hole	`-S 1 bphp 67 66`	a2cec4c897b3… 130 kB	N1
bphp_p75_h74.sanitized.cnf	binary-pigeon-hole	`-S 1 bphp 75 74`	9ce3632c9e43… 162 kB	N1
bphp_p99_h98.sanitized.cnf	binary-pigeon-hole	`-S 1 bphp 99 98`	6a0f28c023b5… 319 kB	N1
rphp_p100_r100.cnf	relativized-pigeon-hole	`-S 1 rphp 100 100 99`	02a5d44d0559… 591 kB	N1
rphp_p105_r105.cnf	relativized-pigeon-hole	`-S 1 rphp 105 105 104`	e4f345877ba5… 573 kB	N1
rphp_p110_r110.cnf	relativized-pigeon-hole	`-S 1 rphp 110 110 109`	a8667fe48e25… 775 kB	N1
rphp_p115_r115.cnf	relativized-pigeon-hole	`-S 1 rphp 115 115 114`	ecd26dfc88ce… 753 kB	N1
rphp_p14_r14.cnf	relativized-pigeon-hole	`-S 1 rphp 14 14 13`	9f7ec7ef3a90… 4 kB	N1
rphp_p6_r28.cnf	relativized-pigeon-hole	`-S 1 rphp 6 28 5`	d518d21a9d85… 4 kB	N1
rphp_p6_r300.cnf	relativized-pigeon-hole	`-S 1 rphp 6 300 5`	3b158899d5a3… 187 kB	N1
rphp_p6_r540.cnf	relativized-pigeon-hole	`-S 1 rphp 6 540 5`	7e3df5ae1e84… 588 kB	N1
rphp_p8_r160.sanitized.cnf	relativized-pigeon-hole	`-S 1 rphp 8 160 7`	2dd4b14a8a82… 93 kB	N1
rphp_p8_r170.sanitized.cnf	relativized-pigeon-hole	`-S 1 rphp 8 170 7`	1156429862d3… 72 kB	N1
rphp_p90_r90.cnf	relativized-pigeon-hole	`-S 1 rphp 90 90 89`	928436a6e8ed… 478 kB	N1
rphp_p95_r95.cnf	relativized-pigeon-hole	`-S 1 rphp 95 95 94`	2d01c7744a99… 469 kB	N1
rphp_p20_r20.cnf	relativized-pigeon-hole	`-S 1 rphp 20 20 19`	189e5991b041… 8 kB	N1
rphp_p25_r25.cnf	relativized-pigeon-hole	`-S 1 rphp 25 25 24`	e430acf720b6… 15 kB	N1
rphp_p30_r30.cnf	relativized-pigeon-hole	`-S 1 rphp 30 30 29`	54ab5a53d2fd… 24 kB	N1
rphp_p35_r35.cnf	relativized-pigeon-hole	`-S 1 rphp 35 35 34`	5351fa0e4423… 37 kB	N1
rphp_p60_r60.cnf	relativized-pigeon-hole	`-S 1 rphp 60 60 59`	23c4e178c94c… 108 kB	N1
rphp_p8_r25.cnf	relativized-pigeon-hole	`-S 1 rphp 8 25 7`	f56c3e42f82d… 4 kB	N1
rphp_p8_r250.cnf	relativized-pigeon-hole	`-S 1 rphp 8 250 7`	eaf2f0803dd2… 162 kB	N1

Notes

parameters read from the file name; rphp uses P-1 holes, found by matching the variable and clause counts