Deciding whether two clausesets are isomorphic by reductions to (generalised) SAT problems.
More...
Deciding whether two clausesets are isomorphic by reductions to (generalised) SAT problems.
Given two clausesets F_1, F_2, the variable sets var(F_1), var(F_2) are partioned into equivalence classes of variables with the same domain size, and bijections between corresponding equivalence classes of F_1 and F_2 are sought together with bijections between the associated domains, such that F_1 is transported into F_2.
 Todo:
 Relations to other modules
 Todo:
 Reduction to graph isomorphisms

The basic reduction is to the graph isomorphism problem (with "coloured" vertices), using the variablesliteralsclauses graph. For Pliterals the variablevaluesliteralsclauses graph is to be used.

These graphs must be easily accessible for clausesets, directly usable for the graphisomorphismalgorithms.
 Todo:
 We also need the determination of the automorphism group of a clauseset, either explicitely listing all elements or giving a more compact representation (using some group theory software).
 Todo:
 Applications

An important application should be to detect symmetries for SAT decision: Given interesting branchings (phi_1, ..., phi_m) for F, check for isomorphisms among the phi_i * F (isomorphic branches don't need to be repeated).

To phi_i * F any kind of reduction can be applied as long as it is compatible with isomorphisms, since isomorphism checking here is only a means to an end.

For this application the main goal is to avoid repeated computations.

And also incomplete isomorphism tests can be used (potentially not finding an isomorphism if there is one).
Definition in file CLSIsomorphisms.hpp.