sgen1

sgen1 -n VARIABLES (-sat | -unsat) [-s SEED] [-m MODEL_FILE] [-min-variables] [-reorder]

What it is

Authors: Ivor Spence
Source of the author list: author's page (eeecs.qub.ac.uk/~I.Spence/sgen) and the header of sgen1.c
Language: C
Licence: none stated
Competitions: SAT Competition 2009
Repository: https://www.eeecs.qub.ac.uk/~I.Spence/sgen/sgen1.c
Seed: -s, default 1; the generator uses its own linear congruential generator
Notes: main() always returns 1, even on success; the verifier ignores the exit status and checks the output instead
Licence note: no licence in the source nor on the page: the recipe is published, the image is not, until the author agrees

Build it and run it

docker build -t satex-gen/sgen1:2009 cnf/sgen1
docker run --rm satex-gen/sgen1:2009 ...  > instance.cnf

The image is not published: the generator declares no licence, so only this recipe is distributed. Building it locally is fine.

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
unsat, 61 variables	`-unsat -n 61 -s 1`	61	132
unsat, 121 variables	`-unsat -n 121 -s 1`	121	252
unsat, 181 variables	`-unsat -n 181 -s 1`	181	372
sat, 100 variables	`-sat -n 100 -s 1`	100	240
sat, 200 variables	`-sat -n 200 -s 1`	200	480
sat, 300 variables	`-sat -n 300 -s 1`	300	720

Reference instances

28 with the same GBD hash · 2 with the same up to a renaming of the variables. 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
sgen1-sat-100-100.cnf	sgen	`-sat -n 100 -s 100`	c12d5e3213fb… 672 B	N1
sgen1-sat-120-100.cnf	sgen	`-sat -n 120 -s 100`	c31f64e36934… 828 B	N1
sgen1-sat-140-100.cnf	sgen	`-sat -n 140 -s 100`	da842d9bdb36… 936 B 0023b1cb2ab6… the author's copy in sgen1-sat.tar on ee…	N1 the author's copy in sgen1-sat.tar on eeecs.qub.ac.uk/~I.Spence/sgen
sgen1-sat-160-100.cnf	sgen	`-sat -n 160 -s 100`	f9abcc53e363… 1 kB	N1
sgen1-sat-180-100-sc2009.cnf	sgen	`-sat -n 180 -s 100`	5feccc06fd6b… 1 kB	N3
sgen1-sat-180-100.cnf	sgen	`-sat -n 180 -s 100`	41f4cb4992a4… 1 kB	N1
sgen1-sat-200-100.cnf	sgen	`-sat -n 200 -s 100`	f4fc9d5721fe… 1 kB	N1
sgen1-sat-220-100.cnf	sgen	`-sat -n 220 -s 100`	72a076145481… 1 kB	N1
sgen1-sat-230-100.cnf	sgen	`-sat -n 230 -s 100`	05f5567936f5… 1 kB	N1
sgen1-sat-240-100.cnf	sgen	`-sat -n 240 -s 100`	91f7c642053c… 1 kB	N1
sgen1-sat-250-100.cnf	sgen	`-sat -n 250 -s 100`	d2b4aadcd039… 2 kB	N1
sgen1-sat-260-100.cnf	sgen	`-sat -n 260 -s 100`	f1c7fb2d19b3… 2 kB	N1
sgen1-sat-270-100.cnf	sgen	`-sat -n 270 -s 100`	5c0b9c890caf… 2 kB	N1
sgen1-sat-280-100.cnf	sgen	`-sat -n 280 -s 100`	71aceeaec564… 2 kB	N1
sgen1-sat-290-100.cnf	sgen	`-sat -n 290 -s 100`	c4f2774e1215… 2 kB	N1
sgen1-sat-300-100.cnf	sgen	`-sat -n 300 -s 100`	d9fad7d0dba3… 2 kB	N1
sgen1-unsat-103-100.cnf	sgen	`-unsat -n 103 -s 100`	7489dc4e399a… 660 B	N1
sgen1-unsat-109-100-sc2009.cnf	sgen	`-unsat -n 109 -s 100`	a9e528e396f4… 780 B	N3
sgen1-unsat-109-100.cnf	sgen	`-unsat -n 109 -s 100`	b0aa64721146… 688 B	N1
sgen1-unsat-115-100.cnf	sgen	`-unsat -n 115 -s 100`	a14b9718d507… 732 B	N1
sgen1-unsat-121-100.cnf	sgen	`-unsat -n 121 -s 100`	2b60f9be1439… 760 B	N1
sgen1-unsat-127-100.cnf	sgen	`-unsat -n 127 -s 100`	b0da15e2ce92… 820 B	N1
sgen1-unsat-133-100.cnf	sgen	`-unsat -n 133 -s 100`	8f7ae5a737fd… 832 B	N1
sgen1-unsat-139-100.cnf	sgen	`-unsat -n 139 -s 100`	ef901de4fdfe… 868 B	N1
sgen1-unsat-145-100.cnf	sgen	`-unsat -n 145 -s 100`	8a8b184febd7… 908 B	N1
sgen1-unsat-151-100.cnf	sgen	`-unsat -n 151 -s 100`	69b4f3e5329c… 952 B	N1
sgen1-unsat-61-100.cnf	sgen	`-unsat -n 61 -s 100`	a73dfc45bae3… 440 B	N1
sgen1-unsat-73-100.cnf	sgen	`-unsat -n 73 -s 100`	1fdc28d67635… 492 B	N1
sgen1-unsat-85-100.cnf	sgen	`-unsat -n 85 -s 100`	107e43f3e761… 544 B	N1
sgen1-unsat-97-100.cnf	sgen	`-unsat -n 97 -s 100`	56123e4cc587… 588 B	N1

Notes

parameters read from the file name, and from the command line kept in the author's copy
the GBD copy lacks one clause of the author's file, (-25 -23): 335 clauses instead of 336; the image reproduces the author's file exactly
variant published by the SAT Competition 2009 organisers; parameters read from the file name