Resumen
In the paper we study the applicability of modern algorithms of computational logic to problems of finding some combinatorial designs. In particular, we consider the well-known open problem ? to answer whether there exist three mutually orthogonal Latin squares of order 10. We propose an iterative procedure to search for such a triple. At each iteration, it constructs the so-called quasi?orthogonal systems. We use the orthogonality index metric that makes it possible to measure how close is the quasi?orthogonal system to the orthogonal one. To construct quasi-orthogonal systems with specified orthogonality index we employ the state-of-the-art algorithms for solving Boolean satisfiability problem (SAT). The results of our computational experiments show that the SAT-solvers can successfully be used to search for new combinatorial designs based on Latin squares.