Improving SAT Solvers on Orthogonal Latin Square Problems

TL;DR

This paper introduces a hybrid approach combining SAT solvers with the Euler-Parker algorithm to efficiently find orthogonal Latin squares, solving previously intractable cases.

Contribution

It presents a novel hybrid method that integrates domain-specific algorithms with SAT solvers to improve solving efficiency for orthogonal Latin squares.

Findings

Hybrid solver solves difficult 10x10 Latin square problems faster.

CaDiCaL with Euler-Parker solves cases in median 5,100 seconds.

Previously unsolved cases are now solvable with the new method.

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.