isomorphism testing in large magmas

Stream: Equational

[Kevin M]

In the eqn 1485 thread we have some size 18 models that I don't currently have a "fast" algorithm for detecting isomorphic operation tables.

In the other investigations, has there already been a tool developed that can exploit known structure to speed up the check?

If not, then:
There is some structure in the known finite examples, and I'd like to brainstorm an algorithm to exploit this.

Structure of 'weak' central groupoids (that are not central groupoids) in all finite examples seen so far.

1. squaring is surjective
2. has an even number of elements
3. for 2n elements, table can be permuted so that there is an nxn block structure:

   * let A = the set of the first n elements, let B = the set of the second n elements.
   * for all x,y in A, (x ◇ y) is in B
   * for all x,y in B, (x ◇ y) is in A

This problem likely has no truly efficient algorithm, but if we could get this to work for size 16 and size 18 models, that would be sufficient for our current use case.

We could potentially even get away with heuristics with "rare" false negatives, as long as there are no false positives of isomorphism.

[Kevin M]

There appears to be some kind of "semi-direct product" like thing that can occur with eqn 1485.
So even if we cannot fully simplify our collection of models, the hope would be to reduce them to a manageable number, to allow investigation of these examples.

[Eric Taucher]

Could Nauty be used here?

https://users.cecs.anu.edu.au/~bdm/nauty/

https://www3.cs.stonybrook.edu/~algorith/implement/nauty/implement.shtml

Don't remember it working as easy as I hoped when I used a few years ago but do remember that it was accurate and fast, really fast.

[Kevin M]

That's a good idea if we can find a "faithful" graph to represent the magma, since the graph problem is almost linear in the "average case".

The natural graph here is the directed graph, where there is an edge x to y iff there is some element z such that x ◇ z = y. Unfortunately, if there are multiple paths of length two between vertices, it is unclear how to "recover" the magma. So this is lossy.

Is there another graph choice?

[Kevin M]

I guess we could "color" the edges, to make the correct length two paths obvious.

[Kevin M]

I wonder if nauty supports that. If not it could in principle be done by adding more vertices and little graph "widgets" to stand for the color.

[Kevin M]

No wait, that would not work, because we'd want the "colors" to be allowed to be permuted as well. So we cannot just tack on distinct widgets.

[Kevin M]

Somehow extra structure needs to be added such that the "good" length 2 paths are clear, and this added structure looks the same for all "good" paths.

[Kevin M]

From what I saw in a skim of the manual, nauty does not support colored edges.

[Kevin M]

== Idea ==
What if each (x ◇ y) = z is encoded by adding two vertices a, b with edges: x -> a -> y -> b -> z and a -> b.
The n vertices encoding magma elements will then have at least an out degree of n. So as long as n>2, the "coloring" vertices a,b will then be structurally distinct from the magma elements.

An $n$ element magma would result in an $n + 2 n^2$ vertex graph, with $5 n^2$ edges. While I do not have much experience with graph algorithms, I think this might still be reasonable for graph comparisons.

This graph is then faithful to the magma, correct?

[Eric Taucher]

Kevin M said:

This graph is then faithful to the magma, correct?

Before we get to far, please realize that I am software developer with a BS in Computer Science so I do get some of the math in this topic but much of it is still past my understanding. However graphs with vertices and edges I tend to get.

Just before you noted that statement I posted this to ChatGPT 40 model

Prompt

Can nauty by Brendan McKay support colored edges? Is so can you demonstrate with an example?

Reply

Nauty, developed by Brendan McKay, is a software package designed to compute automorphism groups of graphs and determine graph isomorphism. While Nauty primarily handles vertex-colored graphs, it does not natively support edge-colored graphs. However, you can represent edge-colored graphs by transforming them into vertex-colored graphs, enabling Nauty to process them.

Transforming Edge-Colored Graphs for Nauty

To handle edge-colored graphs with Nauty, you can convert each edge into a vertex, effectively transforming the original graph into a bipartite graph. Here's how:

1. Original Graph: Start with a graph where edges have assigned colors.

2. Transformation:

   • For each edge in the original graph, introduce a new vertex representing that edge.
   • Connect this new vertex to the two original vertices that the edge was incident upon.
   • Assign a unique color to each new vertex corresponding to the original edge's color.

This transformation results in a bipartite graph where one set of vertices represents the original vertices, and the other set represents the edges, now treated as vertices with specific colors. Nauty can then process this vertex-colored bipartite graph to analyze automorphisms or test for isomorphism.

Example

Consider a simple graph with vertices \( A \) and \( B \) connected by an edge colored 'red'.

• Original Graph:

  • Vertices: \( A \), \( B \)
  • Edge: \( (A, B) \) with color 'red'

• Transformed Graph:

  • Vertices: \( A \), \( B \), \( E_{AB} \)
    • \( E_{AB} \) is a new vertex representing the edge \( (A, B) \)
  • Edges:
    • \( (A, E_{AB}) \)
    • \( (B, E_{AB}) \)
  • Vertex Colors:
    • \( A \): uncolored or assigned a default color
    • \( B \): uncolored or assigned a default color
    • \( E_{AB} \): color 'red'

In this transformed graph, \( E_{AB} \) connects to \( A \) and \( B \), and its color reflects the original edge's color. This structure allows Nauty to process the graph, considering the vertex colors to account for the original edge colors.

Alternative Approach

Another method involves using multiple layers to represent different edge colors. Each layer corresponds to a specific color, and an edge's presence in a layer indicates its color. This approach is discussed in the context of graph isomorphism with colored edges. citeturn0search1

Note: While these transformations enable Nauty to handle edge-colored graphs, they may increase the graph's size and complexity. It's essential to consider the implications on performance and feasibility for large graphs.

ChatGPT shared link

---

---

Also a hypergraph might be of value either for this or some other problems in this topic. In particular this diagram pops into mind during reading some of the descriptions.

Image from Wikipedia article.

I will note that I have no experience with hypergraphs but not afraid to tackle the challenge if needed.

[Alex Meiburg]

To answer the question: yes, encoding magma isomorphism as graph isomorphism is a fairly "standard" and "solved" problem. Mostly people talk about group isomorphism, of which magma isomorphism is of course a special case. (At least for this case, where the input is the multiplication table). There's a nice picture+proof here: https://www.cs.cmu.edu/~glmiller/Publications/Papers/Mi79.pdf

The exact same approach works here with Nauty.

[Alex Meiburg]

The overhead is pretty minimal (~O(n) extra vertices), and conversely graph isomorphism can be recast as magma isomorphism (with O(1) overhead), so these really are very closely equivalent. And I think you will have a hard time finding something that does _better_ than Nauty on this encoding, even if you try to write a custom magma isomorphism checker. The encoding is that efficient and Nauty is that good.

[Kim Morrison]

nauty is really lovely and awesome, and I would love to see generic Lean bindings for it. It does a number of things, but one basic thing that could be read back into Lean and cheaply verified is to produce the isomorphism between two given graphs.

It will also produce generators for the automorphism group of the graph. One could read that into Lean and cheaply verify that that group of permutations injects into the automorphism group of the graph. But for the fact that you've found all the automorphisms, you just have to trust nauty (i.e. it doesn't obviously help you construct that proof).