The geometry of gaussoids

By definition an oriented gaussoid is an assignment of symbols $a_{ijtK}$ to signs {0,+,-}

which is compatible with all edge trinomials. Let a - b - ccdot d

be an edge trinomial with

-variables removed. Compatibility with this trinomial can be expressed with the formula

 ((a=0&b=0)->(c=0|d=0))&
(((a=0&b=+)|(a=-&b=0)|(a=-&b=+))->((c=+&d=-)|(c=-&d=+)))&
(((a=0&b=-)|(a=+&b=0)|(a=+&b=-))->((c=+&d=+)|(c=-&d=-)))

which is a compressed listing of all compatible assignments as a case distinction on the values of

and

. Another formula for compatibility is

(a=+|b=-|(c=+&d=-)|(c=-&d=+))<->(a=-|b=+|(c=+&d=+)|(c=-&d=-))

which reads: there is a positive term if and only if there is a negative term. The latter formula is shorter and more symmetric but the former was solved faster most of the time in our tests.

To encode the three values {0,+,-}

we introduce two variables $V_{ijtK}$ and $V_{ijtK}'$ for every symbol $a_{ijtK}$ and use the following translation table:

The fourth assignment of Boolean variables is forbidden explicitly in the cnf file. Since there are twice as many variables as with gaussoids, we have to choose another ordering. If the symbol $a_{ijtK}$ has canonical index

, then $V_{ijtK}$ gets index 2M-1

and $V_{ijtK}'$ gets

An alternate encoding uses three variables $V_{ijtK}^0$ , $V_{ijtK}^+$ , and $V_{ijtK}^-$ for each symbol and the table:

With this encoding, we can exploit the built-in support for E-clauses of the c2d solver. An E-clause is a clause in a cnf formula which must be satisfied by satisfying exactly one literal. Note that some solvers, in particular cachet, throw a parser error when they encounter an eclauses line in a DIMACS file while others, in particular sharpSAT, ignore it and compute unintended results.

The variables $V_{ijtK}^0$ , $V_{ijtK}^+$ , and $V_{ijtK}^-$ here get indices 3M-2

and

respectively.

There are four possibilities to combine formula and variable encoding. The suffix “f” indicates that the second formula was used and the suffix “v” that the second variable encoding was used.

The following perl script implements the translation table for the first variable encoding, which was used in ocnf{3,4,5}:

binary2oriented.pl

#!/usr/bin/perl -an
my %conv = ('11' => '0', '10' => '+', '01' => '-');
chomp;
print $conv{$_} for m/../g;
print "\n";

We obtain a string composed of 0, + and - which encodes the orientation of the supporting gaussoid under the canonical numbering of

-variables. The listings linked in the table were obtained with:

$ minisat2binary.pl <ocnf3-list | binary2oriented.pl >ocnf3-list.txt

Oriented gaussoids

Download

Enumeration details