Binary Matrix Isomorphism

Stream: maths

[Gobind Puniani]

Hello, I am new to Lean but want to explore it to see if it can help me with my problem. I tried other mathematical software tools such as SageMath and Nauty, but I couldn't quite figure out how to solve my problem with those tools yet.

I am working with incidence matrix representations of graphs/hypergraphs (binary matrices), and I would like to compare a smaller matrix to a larger one to see if the larger one can "consume" the smaller one (that is, can all of the 1's in the smaller matrix match up directly to some subset of 1's in the larger matrix?). Given the smaller matrix, I would like to "broadcast" it to the size of the larger matrix by padding it with rows and columns of 0's. I would then like to generate all distinct isomorphs of the broadcasted matrix using row/column permutations to see if any of these can match up to the larger matrix. We are trying to take advantage of GPUs for rapid matrix multiplication, so I have been thinking about a group-theoretic approach that would involve creating a cyclic matrix group for each broadcasted matrix so that each unique permutation can be generated via matrix multiplication without any duplicates.

I'm happy to provide additional context and clarification. Any advice or suggestions would be very much appreciated. Thank you!

[Eric Wieser]

Is discarding rows from the larger matrix to obtain the smaller one allowed?

[Eric Wieser]

Or does every nonzero row/column of the large one have to be represented in the small one?

[Gobind Puniani]

Every nonzero row/column of the small one must be represented in the large one (not the other way around). Discarding rows/columns of the large one to obtain the smaller one is one option, but it might be too computationally expensive since we still have to permute the remaining rows/columns of the "minimized" larger matrix (and I think we would have to find every distinct permutation for every minimization).

[Eric Wieser]

So is taking the large matrix as $[1]$ and the "small" matrix as $\left[\begin{smallmatrix}0&0\\0&1\end{smallmatrix}\right]$ allowed? nevermind, I don't think the case I'm trying to construct (two columns of the small matrix being replaced by the same column of the large one) exists

[Eric Wieser]

To un- #xy this, you're looking for an algorithm to determine if a docs#simple_graph.embedding exists between two graphs (starting with the incidence matrix)?

[Eric Wieser]

(@Kyle Miller, I think there's a typo in that docstring, I assume one of the Gs should be a G')

[Gobind Puniani]

Yes, I think that's correct (although I must admit that I'm not too familiar with category theory). Since we are trying to exploit GPUs, the algorithm would ideally be implemented in a way that heavily utilizes matrix multiplication operations.

[Jeremy Salwen]

This seems relevant: https://mathoverflow.net/questions/67963/defining-a-canonical-ordering-of-matrix-rows-columns

If I understand correctly, this seems to be the problem you are trying to solve? https://en.wikipedia.org/wiki/Subgraph_isomorphism_problem

[Gobind Puniani]

Yes, the problem is essentially subgraph isomorphism, but we realize that it's NP-hard. We're hoping that we can find some heuristic for our specific problem by creating a permutation group for each of the smaller matrices such that we can generate all distinct row/column permutations and compare each one to the larger matrix.

[Gobind Puniani]

We need to know which exact permutation actually matches the larger matrix, not just whether any permutation of the smaller matrix matches, which is why a canonical comparison probably would not suffice.

[Kyle Miller]

Something to be aware of is that Lean's mathematical library isn't optimized for computation, but rather for proving abstract things. There might be a SimpleGraph type, but it's really just an interface for an abstract symmetric irreflexive relation.

I'm not aware of anything that compiles Lean to anything that is optimized for GPUs either.

[Kyle Miller]

Even the mathlib matrix type is more of an abstract interface than something you would directly calculate with.

[Kyle Miller]

It's probably best not to think of Lean as being comparable to Sage, at least at the moment, if that's why you're interested in potentially using Lean for your project.

[Gobind Puniani]

I see, thank you for the clarification.

[Kyle Miller]

It can be used for computations, but the experience you should expect is like you are using a functional programming language like Haskell.

[Kyle Miller]

Just for a couple examples, I once wrote a toy raytracer and computed a bunch of Jones-like polynomials of knots, both of which are very CPU heavy. For the second, I needed to write my own implementation of polynomials.

[Gobind Puniani]

Very cool!

[Gobind Puniani]

Would you recommend sticking with Sage for this problem then?

[Scott Morrison]

To be honest from what you've said about the problem so far Sage doesn't terrible, and you probably just want C. :-)

[Gobind Puniani]

Understood! I think Sage would work if I can figure out how to generate the cosets of the automorphism group in the group of all row/column permutations for each specific matrix, or if I can find a systematic/algorithmic method for finding all of the generators for distinct row/column permutations for each matrix. I have been trying to find an algorithm for the second option by playing around with permuting equivalence classes of rows and columns (where identical rows and identical columns are grouped together in the same class), but I am generating too many duplicates and not enough of the possible distinct permutations.