Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Daimy Van Caudenberg, Bart Bogaerts, Leandro Vendramin

TL;DR

This paper addresses the problem of enumerating non-isomorphic set-theoretic solutions to the $YBE$ by extending the SAT Modulo Symmetries framework to the Yang–Baxter setting. It introduces two minimality-check implementations—a backtracking approach and a novel incremental SAT-based method—and demonstrates that the incremental method yields substantial speedups, enabling new results up to $|X|=11$. The approach relies on encoding cycle-set properties as CNF, fixing diagonals to reduce symmetry, and using canonical (lex-leader) constraints to prune search. The work provides a faster, scalable methodology for building databases of solutions, with potential extensions to related combinatorial structures such as racks, quandles, and non-involutive or relaxed-degeneracy cases; it also discusses challenges in achieving proofs of correctness and future directions for validation and certification.

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.

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

TL;DR

This paper addresses the problem of enumerating non-isomorphic set-theoretic solutions to the by extending the SAT Modulo Symmetries framework to the Yang–Baxter setting. It introduces two minimality-check implementations—a backtracking approach and a novel incremental SAT-based method—and demonstrates that the incremental method yields substantial speedups, enabling new results up to . The approach relies on encoding cycle-set properties as CNF, fixing diagonals to reduce symmetry, and using canonical (lex-leader) constraints to prune search. The work provides a faster, scalable methodology for building databases of solutions, with potential extensions to related combinatorial structures such as racks, quandles, and non-involutive or relaxed-degeneracy cases; it also discusses challenges in achieving proofs of correctness and future directions for validation and certification.

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.
Paper Structure (14 sections, 3 equations)

This paper contains 14 sections, 3 equations.

Table of Contents

  1. Introduction
  2. The Yang-Baxter Equation
  3. SAT Modulo Symmetries
  4. Our contributions
  5. Preliminaries
  6. Yang-Baxter Equation and Cycle Sets
  7. Boolean Satisfiability (SAT)
  8. Symmetry in SAT
  9. SAT Modulo Symmetries for the Yang-Baxter Equation
  10. SAT Encoding
  11. Fixing the Diagonal
  12. Isomorphisms and Symmetries
  13. Minimality Check
  14. Partial Cycle Sets

Theorems & Definitions (1)

  • definition thmcounterdefinition