Plans for Maximacomponents regarding symmetries in satisfiability problems.
More...
Go to the source code of this file.
Detailed Description
Plans for Maximacomponents regarding symmetries in satisfiability problems.
 Todo:
 Create milestones
 Todo:
 Organisation

Rename Symmetries.mac to "Isomorphisms.mac".
 Todo:
 Relations to other modules
 Todo:
 Notions for symmetries

Consider a formal clauseset FF = [V,F].

A "varsymmetry" f for FF is a varsubstitution with V <= dom(F) such that f(F) = F.

A "signsymmetry" for FF is a signsubstitution with V <= dom(F) such that f(F) = F.

A "symmetry" for FF is a literal substitution with V <= dom(F) such that f(F) = F.
 Todo:
 Bruteforce algorithms

Given a formal clauseset FF = [V,F], find all varsymmetries, signsymmetries or symmetries for FF.

We should also allow a parameter W, a subset of V, such that only substitutions are considered affecting W, i.e., the literal substitution are identical outside of W.
 Todo:
 Reduction to graph isomorphisms

What is the standard here for available implementations: (undirected) graphs or directed graphs?

It appears that directed graphs are better here, since they allow to express more structure directly.

Considering undirected graphs, for FF the symmetries of FF should "almost always" be the symmetries of the extended clauseliteral graph G with vertices

the variables

the literals

the clauses

a vertex symbolising "var(F)", connected with exactly all variables

a vertex symbolising "F", connected with exactly all clauses.

When fixing for the automorphisms of G the vertex "var(F)", then it should always be guaranteed that they correspond 11 to the symmetries of FF.

DONE (see is_isomorphic_fcs in ComputerAlgebra/Satisfiability/Lisp/Symmetries/Symmetries.mac) If directed graphs are considered, then one could fix the direction "var(F) > variables > literals > clauses > F" (or vice versa), and get in this way rid off any unwanted graph automorphisms.
 Todo:
 is_isomorphic_btr_cs

We should rename the current "is_isomorphic_cs" etc., so that these names reflect the reduction to graph isomorphisms.

And the current "is_isomorphic_btr_cs" should become "is_isomorphic_btr_cs_p", while "is_isomorphic_btr_cs" should return instead of true the isomorphism found.

Actually, then the prefix "is" could be dropped? But perhaps here we keep it  other choices aren't much better.

We need a version for varisomorphisms:

Call it "is_varisomorphic_btr_cs_p" etc.

DONE This problem can also be reduced to the isomorphismproblem of the incidence matrices.

is_isomorphic_btr_cs function should become an instance of the concept of active clausesets.

In this way making it possible to apply all of SAT techniques.

We must take some care here that the overheads are acceptable, since this function is basic for many other functions of the library.

The techniques from graph theory (see ComputerAlgebra/Graphs/Lisp/Isomorphisms/plans/general.hpp) should be transferred and generalised.

Computing splitting trees:

As a first step towards making is_isomorphic_btr_cs an instance of a generalised SAT algorithms, create a variant which computes the whole splitting tree.

This then yields a representation of all isomorphisms (with proof of completeness!).
 Todo:
 Exploring symmetries

Compute the orbits of literals under the action of the automorphism group of a clauseset.

Stronger one could compute simply all permutations combined with sign flips which leave the clauseset invariant, i.e., the full automorphism group in the trivial representation.

Then one needs to look for more intelligent representations of the automorphism group.

Likely, Maxima is only for simple and initial attempts towards symmetries, and Gap is the real tool here.
 Todo:
 Homomorphisms

Create "Homomorphisms.mac" etc.

Perhaps we have a dedicated module "Homomorphisms"; likely this is now a submodule of ClauseSets/Categories.

Since homomorphisms are special substitutions, first this notion needs to be fixed.

A basic task is to find the core of a clauseset (according to [Szeider, 2003] unique up to isomorphism).
Definition in file general.hpp.