Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation

TL;DR

This paper advances the enumeration of solutions to the Yang-Baxter equation by extending SAT-based methods, enabling faster computation and larger set sizes than previously possible, with applications across multiple scientific fields.

Contribution

It introduces an incremental, SAT-based approach within the SMS framework, significantly improving the efficiency and scope of enumerating Yang-Baxter solutions.

Findings

Reproduces known solutions faster

Enables enumeration for larger set sizes

Extends the boundaries of known solutions

Abstract

We tackle the problem of enumerating set-theoretic solutions to the Yang-Baxter equation. This equation originates from statistical and quantum mechanics, but also has applications in knot theory, cryptography, quantum computation and group theory. Non-degenerate, involutive solutions have been enumerated for sets up to size 10 using constraint programming with partial static symmetry breaking; for general non-involutive solutions, a similar approach was used to enumerate solutions for sets up to size 8. In this paper, we use and extend the SAT Modulo Symmetries framework (SMS), to expand the boundaries for which solutions are known. The SMS framework relies on a minimality check; we present two solutions to this, one that stays close to the original one designed for enumerating graphs and a new incremental, SAT-based approach. With our new method, we can reproduce previously known results much faster and also report on results for sizes that have remained out of reach so far. This is an extended version of a paper to appear in the proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems.