general.hpp File Reference

Plans for Maxima-components regarding symmetries in satisfiability problems. More...

Go to the source code of this file.

Detailed Description

Plans for Maxima-components regarding symmetries in satisfiability problems.

Create milestones
  • Rename Symmetries.mac to "Isomorphisms.mac".
Relations to other modules
Notions for symmetries
  • Consider a formal clause-set FF = [V,F].
  • A "var-symmetry" f for FF is a var-substitution with V <= dom(F) such that f(F) = F.
  • A "sign-symmetry" for FF is a sign-substitution 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.
Brute-force algorithms
  • Given a formal clause-set FF = [V,F], find all var-symmetries, sign-symmetries 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.
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 clause-literal graph G with vertices
    1. the variables
    2. the literals
    3. the clauses
    4. a vertex symbolising "var(F)", connected with exactly all variables
    5. 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 1-1 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.
  • 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 var-isomorphisms:
    1. Call it "is_varisomorphic_btr_cs_p" etc.
    2. DONE This problem can also be reduced to the isomorphism-problem of the incidence matrices.
  • is_isomorphic_btr_cs function should become an instance of the concept of active clause-sets.
    1. In this way making it possible to apply all of SAT techniques.
    2. We must take some care here that the overheads are acceptable, since this function is basic for many other functions of the library.
    3. The techniques from graph theory (see ComputerAlgebra/Graphs/Lisp/Isomorphisms/plans/general.hpp) should be transferred and generalised.
  • Computing splitting trees:
    1. 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.
    2. This then yields a representation of all isomorphisms (with proof of completeness!).
Exploring symmetries
  • Compute the orbits of literals under the action of the automorphism group of a clause-set.
  • Stronger one could compute simply all permutations combined with sign flips which leave the clause-set 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.
  • Create "Homomorphisms.mac" etc.
  • Perhaps we have a dedicated module "Homomorphisms"; likely this is now a sub-module 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 clause-set (according to [Szeider, 2003] unique up to isomorphism).

Definition in file general.hpp.