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.

翻译：拉丁方是$n\times n$矩阵，包含$n种符号，其中每个符号在每行及每列中各出现恰好一次。这类问题由欧拉开启研究，后因数独游戏而广为人知，至今仍是困难组合搜索问题的丰富来源。若两个拉丁方重叠时无重复的有序符号对，则称它们为正交伴侣。除阶数2和6外，每个阶数都存在正交拉丁方对，然而通过计算寻找正交拉丁方极具挑战性。可满足性（SAT）求解器在组合搜索领域表现突出，已被用于解决多种不同类型的正交拉丁方问题。但SAT求解器缺乏拉丁方领域的专业知识，例如用于正交伴侣构造的欧拉-帕克算法。本文提出一种混合方法，将SAT求解器与基于丢番图系统求解器实现的欧拉-帕克算法相结合，实验表明该混合求解器能有效寻找特定类型的正交拉丁方。例如，近期Bright、Keita和Stevens使用SAT求解器发现了存在性25年悬而未决的$10\times10$阶正交拉丁方对。最困难的实例中，SAT求解器CaDiCaL在七天内无法求解，但通过集成外部欧拉-帕克算法后，该求解器能在中位数约5,100秒内完成求解。