The geometry of gaussoids

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.

Enumerating gaussoids with SAT solvers

The gaussoid axioms (G1)–(G4) are Boolean formulas whose atomic formulas are statements about membership of

-variables in a set mathcal{G}

. For any fixed

, the gaussoids on

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

is given in the following files:

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}$ .

-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

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

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

Gaussoids

Download

Enumerating gaussoids with SAT solvers