International Conference «Mathematical and Information Technologies, MIT-2016»

28 August – 5 September 2016

Vrnjacka Banja, Serbia – Budva, Montenegro

Kochemazov S.E.   Zaikin O.S.   Semenov A.A.  

The comparison of different SAT encodings for the problem of search for systems of orthogonal Latin squares

Reporter: Zaikin O.S.

In this report we present several different propositional encodings for finding systems of orthogonal Latin squares, evaluate their effectiveness using state-of-the-art parameterized algorithms for solving Boolean satisfiability problem (SAT) and discuss their strengths and weaknesses regarding possible applications for solving several relevant combinatorial problems. 

Latin square of order n is a square table n x n filled with elements from the set {1,…,n} in such a way that each element appears in each column and each row exactly once. Two Latin squares A and B are called orthogonal if all pairs of the kind (a_ij,b_ij ),a_ij\in A,b_ij \in B, i,j \in {1,…,n} are different. One of the most widely known currently unsolved combinatorial problems consists in answering the question whether there exist three mutually orthogonal Latin squares of order 10. The fact that this problem is very hard lead to the consideration of several similar but more realistic problems, such as to construct such triples of  Latin squares of order 10, in which first square is orthogonal to two others, but the remaining two are orthogonal only over limited set of cells.

Since the problem of constructing pairs of orthogonal Latin squares of order 10 has quite high combinatorial complexity, it is reasonable to apply SAT approach to the construction of systems of such squares. The SAT approach consists in reducing the underlying problem to SAT and applying state-of-the-art sequential and parallel SAT solving algorithms to the considered problem instances. Despite the fact that SAT is NP-complete, many practical problems from various areas of science and industry can be effectively reduced to it and solved relatively fast. Thanks to the remarkable progress seen in the recent years regarding the effectiveness of state-of-the-art SAT solving algorithms, the scope of problems solved via SAT is gradually increasing.

Without the loss of generality let us consider the problem of finding pairs of orthogonal Latin squares. What makes it interesting is that we can reduce it to SAT via several different methods. Thus, we can consider this problem stated for related combinatorial designs. For example, a pair of orthogonal Latin squares can be represented in the form of orthogonal array, or as a set of disjoint transversals.  It means that when reducing this problem to SAT we can do it at least in three different ways depending on how we represent Latin squares. Since SAT is considered for Boolean formulas over sets of Boolean variables, we need to represent elements of Latin square or related combinatorial design via Boolean variables. There are two main approaches to this. In the first approach we encode the number from 1 to n with the help of n Boolean variables. In the second approach we encode it as a binary number using \floor{log n}+1 Boolean variables. The propositional encoding for the problems of finding systems of orthogonal Latin squares uses many constraints of the kind At-Most-One (AMO) and At-Least-One (ALO). Depending on the chosen way for representing numbers we can apply different methods to encode such constraints.

As a result we can construct many different variants of SAT encodings for finding various systems of orthogonal Latin squares of order 10. We compare their size in terms of number of literals and clauses in the corresponding Boolean formulas, and evaluate their effectiveness using state-of-the-art parallel parameterized SAT algorithms.

To reports list

© 1996-2019, Institute of computational technologies of SB RAS, Novosibirsk