基于增量SAT枚举Yang-Baxter方程的解
计算机科学中的逻辑
2025-05-06 v1 离散数学
摘要
我们解决了枚举Yang-Baxter方程集合论解的问题。该方程来源于统计和量子力学，也在图论、密码学、量子计算和群论中具有应用。针对非退化、介介解，已使用带部分静态对称破坏的约束编程方法枚举至集合大小为10；针对一般非介介解，类似方法枚举至集合大小为8。在本文中，我们使用并扩展了基于SAT的对称枚举框架(SMS)，以扩大已知解的覆盖范围。SMS框架依赖最小性检查；我们提出两种解决方案，其中一种接近原为枚举图而设计的方案，另一种为新的增量式SAT方法。通过新方法，我们能够大大加快以前已知结果的重现速度，并报告了迄今为止尚未达到的规模的结果。这一工作是该论文在31届国际工具与系统构建与分析系统工具会议 proceedings 中将呈现的扩展版本。
关键词
引用
@article{arxiv.2501.14363,
title = {Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation},
author = {Daimy Van Caudenberg and Bart Bogaerts and Leandro Vendramin},
journal= {arXiv preprint arXiv:2501.14363},
year = {2025}
}