Improving SAT Solvers on Orthogonal Latin Square Problems

Summary · qwen2.5:32b

The paper introduces a hybrid method combining SAT solvers with the Euler-Parker algorithm to improve the search for orthogonal Latin squares, which are challenging combinatorial problems. This approach effectively finds certain pairs of orthogonal Latin squares that were previously unknown, demonstrating a significant reduction in computational time compared to using SAT solvers alone; for instance, CaDiCaL augmented with the Euler-Parker algorithm solves the hardest cases in about 5,100 seconds on average.

Suggested post angle

Exploring a new approach to solve orthogonal Latin square problems using SAT solvers and Diophantine system solvers.

Excerpt

arXiv:2605.02132v2 Announce Type: replace-cross Abstract: Latin squares are $n\times n$ matrices containing $n$ symbols, where each symbol appears exactly once in each row and column. They were studied by Euler, later popularized through Sudoku, and remain a rich source of difficult combinatorial search problems. Two Latin squares are orthogonal mates if, when overlaid, no ordered pair of symbols repeats. Pairs of orthogonal Latin squares exist for every order except 2 and 6, but finding orthogonal Latin squares computationally can be challenging. Satisfiability (SAT) solvers are strong at combinatorial search and have been used to resolve a number of various kinds of orthogonal Latin square problems. On the other hand, SAT solvers lack domain knowledge about Latin squares, such as the Euler-Parker algorithm for orthogonal mate construction. In this paper, we propose a hybrid method combining a SAT solver with the Euler-Parker algorithm (implemented using a Diophantine system solver) and show that the resulting solver is effective at finding certain kinds of orthogonal Latin squares. For example, certain pairs of $10\times10$ orthogonal Latin squares whose existence was unknown for over 25 years were recently found by Bright, Keita, and Stevens using a SAT solver. The hardest cases could not be solved by the SAT solver CaDiCaL within seven days, but CaDiCaL augmented with an external Euler-Parker algorithm solves these cases in a median of around 5,100 seconds.