Orthogonal Latin Squares of Order Ten with Two Relations: A SAT Investigation
Curtis Bright, Amadou Keita, Brett Stevens
TL;DR
This work addresses the existence and enumeration of all $2\operatorname{MOLS}(10)$, equivalently $4$-nets$(10)$, that possess two nontrivial $\,\mathbb{F}_2$-linear relations. It recasts the problem as a SAT instance by encoding Latin-square constraints, orthogonality via a composition-square construction, the two-relations structure, and Delisle’s symmetry-breaking into CNF, and then exhaustively enumerates all solutions with an IPASIR-UP–CaDiCaL setup while producing DRAT certificates for verification. The authors report that the SAT-based approach completes the enumeration in under a desktop-hour, producing $3{,}904$ solutions in case 1 and $22{,}320$ in case 5 (with cases 2–4 yielding none), and confirming $91$ solutions up to main-class equivalence with a rank distribution of six at $34$ and the rest at $35$. This demonstrates a substantial speed and trust advantage over previous backtracking methods and provides verifiable exhaustiveness certificates, enabling reliable extensions to related combinatorial-design questions and higher-order nets.
Abstract
A $k$-net($n$) is a combinatorial design equivalent to $k-2$ mutually orthogonal Latin squares of order $n$. A relation in a net is a linear dependency over $\mathbb{F}_2$ in the incidence matrix of the net. A computational enumeration of all orthogonal pairs of Latin squares of order 10 whose corresponding nets have at least two nontrivial relations was achieved by Delisle in 2010 and verified by an independent search of Myrvold. In this paper, we confirm the correctness of their exhaustive enumerations with a satisfiability (SAT) solver approach instead of using custom-written backtracking code. Performing the enumeration using a SAT solver has at least three advantages. First, it reduces the amount of trust necessary, as SAT solvers produce independently-verifiable certificates that their enumerations are complete. These certificates can be checked by formal proof verifiers that are relatively simple pieces of software, and therefore easier to trust. Second, it is typically more straightforward and less error-prone to use a SAT solver over writing search code. Third, it can be more efficient to use a SAT-based approach, as SAT solvers are highly optimized pieces of software incorporating backtracking-with-learning for improving the efficiency of the backtracking search. For example, the SAT solver completely enumerates all orthogonal pairs of Latin squares of order ten with two nontrivial relations in under 2 hours on a desktop machine, while Delisle's 2010 search used 11,700 CPU hours. Although computer hardware was slower in 2010, this alone cannot explain the improvement in the efficiency of our SAT-based search.