{"id":"arxiv/2605.02132","url":"https://arxiv.org/abs/2605.02132","tags":["cs.DM","math.CO"],"score":0,"title":"Improving SAT Solvers on Orthogonal Latin Square Problems","domain":"cs.DM","source":"arxiv","authors":["Aaron Barnoff","Curtis Bright"],"reviews":0,"subject":"cs.DM","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-05-04","reactions":{}}