Special gaussoids

This page provides lists of the special gaussoids in small dimension from Table 1 of Construction Methods for Gaussoids.

For each class of special gaussoids, we provide a verification of the count from Table 1 as well as a listing of all members for small dimensions. Some listings are bzip2-compressed and those inflate to between 3 and 6 GiB. The source CNF file is linked in the first column.

Download

	DSHARP	time	nbc_minisat_all	time
ELUBF3	11	0.00	cnf3-list.txt	0.00
ELUBF4	679	0.01	cnf4-list.txt	0.01
ELUBF5	60212776	81.38	cnf5-list.txt.bz2	1242
ELUB3	10	0.00	ELUB3-list.txt	0.00
ELUB4	640	0.01	ELUB4-list.txt	0.01
ELUB5	59348930	72.75	ELUB5-list.txt.bz2	1223
ELUF3	8	0.00	ELUF3-list.txt	0.00
ELUF4	522	0.00	ELUF4-list.txt	0.00
ELUF5	48633672	13.12	ELUF5-list.txt.bz2	1002
ELU3	7	0.00	ELU3-list.txt	0.00
ELU4	513	0.00	ELU4-list.txt	0.00
ELU5	47867881	10.39	ELU5-list.txt.bz2	984
LUB3	9	0.00	LUB3-list.txt	0.00
LUB4	111	0.01	LUB4-list.txt	0.00
LUB5	0	0.60	LUB5-list.txt	0.54
LUF3	7	0.00	LUF3-list.txt	0.00
LUF4	61	0.00	LUF4-list.txt	0.00
LUF5	1	0.06	LUF5-list.txt	0.10
LU3	6	0.00	LU3-list.txt	0.00
LU4	60	0.00	LU4-list.txt	0.00
LU5	0	0.05	LU5-list.txt	0.10
UB3	6	0.00	UB3-list.txt	0.00
UB4	15	0.00	UB4-list.txt	0.00
UB5	0	0.01	UB5-list.txt	0.00
UF3	4	0.00	UF3-list.txt	0.00
UF4	1	0.00	UF4-list.txt	0.00
UF5	1	0.00	UF5-list.txt	0.00
EF3	2	0.00	EF3-list.txt	0.00
EF4	2	0.00	EF4-list.txt	0.00
EF5	2	0.00	EF5-list.txt	0.00
EUBF3	8	0.00	EUBF3-list.txt	0.00
EUBF4	64	0.00	EUBF4-list.txt	0.00
EUBF5	1024	0.31	EUBF5-list.txt	0.11
EUBF6	32768	59.86	EUBF6-list.txt	8.28
EUB3	7	0.00	EUB3-list.txt	0.00
EUB4	41	0.00	EUB4-list.txt	0.00
EUB5	388	0.17	EUB5-list.txt	0.05
EUB6	5789	8.22	EUB6-list.txt	1.38
UBF3	7	0.00	UBF3-list.txt	0.00
UBF4	34	0.00	UBF4-list.txt	0.00
UBF5	206	0.16	UBF5-list.txt	0.04
UBF6	1486	12.05	UBF6-list.txt	0.81
EUF3	5	0.00	EUF3-list.txt	0.00
EUF4	15	0.00	EUF4-list.txt	0.00
EUF5	52	0.02	EUF5-list.txt	0.01
EUF6	203	0.34	EUF6-list.txt	0.07
EU3	4	0.00	EU3-list.txt	0.00
EU4	10	0.00	EU4-list.txt	0.00
EU5	26	0.00	EU5-list.txt	0.00
EU6	76	0.00	EU6-list.txt	0.02
EBF3	5	0.00	EBF3-list.txt	0.00
EBF4	15	0.00	EBF4-list.txt	0.00
EBF5	52	0.05	EBF5-list.txt	0.01
EBF6	203	1.46	EBF6-list.txt	0.16
BF3	4	0.00	BF3-list.txt	0.00
BF4	10	0.00	BF4-list.txt	0.00
BF5	26	0.03	BF5-list.txt	0.01
BF6	76	0.45	BF6-list.txt	0.08
EB3	4	0.00	EB3-list.txt	0.00
EB4	8	0.00	EB4-list.txt	0.00
EB5	16	0.05	EB5-list.txt	0.00
EB6	32	1.16	EB6-list.txt	0.05
LUBF3	10	0.00	LUBF3-list.txt	0.00
LUBF4	142	0.01	LUBF4-list.txt	0.00
LUBF5	1166	2.37	LUBF5-list.txt	0.83
LUBF6	12796	137	LUBF6-list.txt	17.06
LUBF7	183772	255	LUBF7-list.txt	274
LUBF8	3221660	>14h	LUBF8-list.txt.bz2	129

Note: DSHARP did not terminate after 14 hours for LUBF8-cnf.txt. The count there was verified by cachet (ca. 4h) and the listing from nbc_minisat_all.

LUBF-gaussoids modulo symmetry

We also provide precomputed lists of LUBF-gaussoids modulo the symmetric group S_n . The files contain a representative of each symmetry orbit (the lexicographically maximal string in the orbit) followed by a tab character followed by the size of the orbit.

	Symmetry classes	Size reduction
LUBF3	4	60%
LUBF4	15	89%
LUBF5	23	98%
LUBF6	47	99.63%
LUBF7	95	99.948%
LUBF8	222	99.993%

Using the reduced lists it is not hard to determine the number of non-orientable LUBF-gaussoids shown in the table in the last section of the paper: Since orientability is S_n -invariant, it suffices to write down a formula for the orientations of each representative only and sum over the orbit sizes of unsatisfiable formulas.

Enumeration details

The description of the special classes is via compulsory minors. The axiomatization uses the complementary class of forbidden minors. CNF files are created by first taking the gaussoid axioms from Enumerating Gaussoids and then for every forbidden minor appending a small set of axioms which forbid this minor. For example a disjunction over all 2-faces of the 3-cube forbids texttt E , or requiring that for every 2-face, its opposite face has to be inside the gaussoid, forbids singletons.

Acknowledgements

To produce the listings, we used Takahisa Toda's and Takehide Soh's AllSAT solvers on the resulting CNF files and condensed its output using the minisat2binary.pl script from Enumerating Gaussoids.

The number of entries in each listing was verified by independently running the SAT counters sharpSAT (in the paper) and DSHARP (in preparation for publishing the data) on the same CNF files.

MiniSAT was used for satisfiability checking.