Gaussoids

Download

The files linked in the following table contain all gaussoids for n=3,4,5 and orbit representatives modulo the different symmetry groups (Theorem 4.1). The full list for n=5 is bzip2 compressed and expands to about 4.6GB. The convention for these files is that a zero means that this variable is contained in the gaussoid. The files for orbit representatives contain the orbit sizes too. The variable orderings are given in the following files: vars3.txt, vars4.txt, vars5.txt.

n all mod S_n mod mathbb{Z}/2mathbb{Z} rtimes S_n mod (mathbb{Z}/2mathbb{Z})^n rtimes S_n
3 11 5 4 4
4 679 58 42 19
5 60212776 508817 254826 16981

Enumerating gaussoids with SAT solvers

The gaussoid axioms (G1)–(G4) are Boolean formulas whose atomic formulas are statements about membership of a-variables in a set mathcal{G}. For any fixed n, the gaussoids on n are described by introducing a Boolean variable V_{ijtK} for each statement “a_{ijtK} in mathcal{G}” and concatenating the axioms (G1)–(G4) for all choices of i, j, K.

Our convention is that the statement “a_{ijtK} in mathcal{G}” is considered true if and only if the variable V_{ijtK} is zero, i.e. false. This convention becomes more natural in the oriented context. V_{ijtK} being zero should be thought of as the vanishing of the almost-principal minor a_{ijtK}.

The cnf files in DIMACS format allow consecutive numbers starting with 1 to denote variables. Our variable ordering, referred to below as the canonical numbering, for each n is given in the following files:

It is not possible to paste cnf files generated for different n together.

c2d time cachet time sharpSAT time bdd_minisat_all time
cnf3 11 0.00 * 0.01 * 0.00 cnf3-list.txt 0.00
cnf4 679 0.06 * 0.01 * 0.00 cnf4-list.txt 0.00
cnf5 60212776 20.8 * 17.8 * 14.7 cnf5-list.txt.bz2 158
cnf6 OOM - ERR† - - -

The time is in seconds. A * in the table means the computation confirms the result in the previous column, - indicates that no result is available. c2d is a 32-bit binary and OOM in its column means it ran out of the 4 GiB of addressable memory. Note that the time reported for bdd_minisat_all is that reported as “cpu time (solve)” in its output, not counting the time needed to output all models.

† The ERR in the cnf6 row for cachet means that cachet incorrectly reports the CNF as unsatisfiable after about 48 hours of computation, even though the empty gaussoid can be independently verified to satisfy the formula in cnf6.txt (every clause contains an unnegated variable). cachet does not enable big number support by default and we found it to be broken (Segmentation fault after we modified the source code to compile at all). We suspect that cachet reports the formula as unsatisfiable because the number of 6-gaussoids exceeds 2^{64}.

A sample of lines from the output cnf3-list of bdd_minisat_all follows:

-1 -2 -3 -4 -5 -6 0
-1 -2 -3 -4 5 6 0
-1 -2 3 4 -5 -6 0
-1 2 3 4 5 6 0
1 -2 3 4 5 6 0

Each line lists a satisfying assignment of the 6 a-variables. We convert these files to a more compressed listing of “0” and “1” according to the canonical variable numbering:

000000
000011
001100
011111
101111

This conversion is carried out by the following perl script:

minisat2binary.pl
#!/usr/bin/perl -an
pop @F; # forget the trailing "0" on every line
print m/^-/ ? "0" : "1" for @F;
print "\n";

The files linked above were created from the output files cnf*-list from bdd_minisat_all with this line:

$ minisat2binary.pl <cnf5-list >cnf5-list.txt # optionally compress with bzip2