## Gaussoids## DownloadThe files linked in the following table contain all gaussoids for 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 solversThe gaussoid axioms (G1)–(G4) are Boolean formulas whose atomic formulas are statements about membership of -variables in a set . For any fixed , the gaussoids on are described by introducing a Boolean variable for each statement “” and concatenating the axioms (G1)–(G4) for all choices of . Our convention is that the statement “” is considered true if and only if the variable is zero, i.e. false. This convention becomes more natural in the oriented context. being zero should be thought of as the vanishing of the almost-principal minor . The cnf files in It is not possible to paste cnf files generated for different together.
The time is in seconds. A † The A sample of lines from the output -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: 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 |