The search for pairs of orthogonal diagonal latin squares of order 10 in the volunteer computing project SAT@home

In this paper we consider the approach to search for systems of orthogonal Latin Squares, that is based on reducing the corresponding problems to Boolean Satisfiability problem. We constructed the SAT encoding for finding orthogonal diagonal Latin Squares of order 10. Using this encoding and the resources provided by the volunteer computing project SAT@home we managed to find 17 previously unknown pairs. Based on these 17 pairs and on 3 previously published pairs we constructed the pseudotriples of diagonal Latin Squares of order 10. To construct pseudotriples we employed the computing cluster. The last step required us to make parallel implementation of the algorithm for generating diagonal Latin Squares of order 10.