## Oriented gaussoids## DownloadWe enumerated all oriented gaussoids for : ## Enumeration detailsBy definition an oriented gaussoid is an assignment of symbols to signs which is compatible with all edge trinomials. Let 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 we introduce two variables and for every symbol 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 has canonical index , then gets index and gets . An alternate encoding uses three variables , , and 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 The variables , , and here get indices , 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 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 |