Improving SAT Solvers on Orthogonal Latin Square Problems

Aaron Barnoff, Curtis Bright

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…