Mathematical and Information Technologies, MIT-2016 β€” Information technologies The Comparison of Different SAT Encodings for the Problem of Search for Systems of Orthogonal Latin Squares Stepan Kochemazov, Oleg Zaikin, and Alexander Semenov Matrosov Institute for System Dynamics and Control Theory SB RAS, Irkutsk, Russia {veinamond,zaikin.icc}@gmail.com,biclop.rambler@yandex.ru Abstract. In this report we present several different propositional en- codings for finding systems of mutually orthogonal Latin squares, and evaluate their effectiveness using state-of-the-art parallel and sequential algorithms for solving Boolean satisfiability problem (SAT). We also ap- ply the widely used SMAC tool to study the possibility of improving the effectiveness of lingeling SAT solver on the considered tests and discuss the results of corresponding computational experiments. Keywords: latin squares, MOLS, SAT, combinatorial designs. 1 Introduction A Latin square 𝐴 = (π‘Žπ‘–π‘— ) of order 𝑛 is an 𝑛×𝑛 table filled with symbols from the set 𝑁 = {0, 1, ..., 𝑛 βˆ’ 1}, in such a way that each symbol occurs precisely once in each row and each column [5]. Diagonal Latin square is a Latin square, in which each symbol from 𝑁 occurs precisely once in its main diagonal and in its main antidiagonal. Two Latin squares 𝐴 = (π‘Žπ‘–π‘— ) and 𝐡 = (𝑏𝑖𝑗 ) are orthogonal if all ordered pairs (π‘Žπ‘–π‘— , 𝑏𝑖𝑗 ) are distinct. A set of Latin squares, each two of them orthogonal, is called a set of mutually orthogonal Latin squares (MOLS). A set of diagonal Latin squares, each two of them orthogonal, is called a set of mutually orthogonal diagonal Latin squares (MODLS). Latin squares represent a well studied combinatorial design with rich history dating several centuries back. They have a number of useful properties that make it possible to use them in various areas, such as experimental design, error correcting codes, etc. Also Latin squares are often used as a basis for mathematical puzzles, such as Sudoku and Magical squares. That being said, there remain several hard combinatorial problems related to Latin squares that have not been solved yet. One of the most complex and widely known problem is the one that consists in answering the question if there exists a triple of MOLS of order 10. Even relatively simple problems, such as finding pairs of orthogonal (diagonal) Latin squares of order 10 are relatively hard and there are no known effective methods for solving them. 155 Mathematical and Information Technologies, MIT-2016 β€” Information technologies In this context it is interesting to apply to this class of problems state-of- the-art combinatorial algorithms. One class of such algorithms is formed by the algorithms for solving Boolean satisfiability problem (SAT) [4]. Boolean satisfia- bility problem is usually formulated as follows: for an arbitrary Boolean formula to answer the question if it is satisfiable. SAT is historically the first NP-complete problem [6], thus it is possible to reduce many combinatorial problems to SAT. What makes it different from many other NP-complete problems is the fact that in the last twenty years there was achieved a remarkable progress in the effective- ness of SAT solving algorithms. Annual SAT competitions [2] make it possible to quickly evaluate new heuristics and ideas using relatively wide class of tests. Today there exist both sequential and multi-threaded implementations of SAT solving algorithms (the corresponding software complexes are usually referred to as SAT solvers). Interesting feature of these algorithms is that since they incor- porate many heuristics, each SAT solver has a number of numeric parameters, that can be easily varied. Given a specific solver, on some classes of tests by carefully choosing proper values of parameters it is possible to achieve quite sig- nificant performance gain. In this paper we apply state-of-the-art SAT solving algorithms to the problem of finding pairs and triples of MOLS and evaluate their effectiveness. Let us present the brief outline of the paper. In the next section we provide basic terms about SAT and consider how the problem of finding MOLS can be reduced to SAT. In the third section we describe state-of-the-art tools for finding effective combinations of SAT solver parameters and describe our experimental setup. In the fourth section we present the results of our computational experi- ments and their discussion. In the last section we make conclusions and outline our plans for the future. 2 Constructing SAT Encodings for Finding MOLS Interesting and often forgotten fact about SAT encodings is that usually for the same problem we can construct several different variants of them. For example, it can be done via representing the original problem by some equivalent problem. Latin squares can serve as a good example of such approach, because a Latin square of order 𝑛 as a combinatorial design is equivalent to orthogonal array, a set of 𝑛 disjoint transversals, a set of 3 orthogonal matrices, etc. It means that in practice to search for Latin squares with specific properties we can search for any of equivalent objects with desired properties adapted to their form. An- other way to construct different SAT encodings for the same problem consists in employing different methods for reducing specific constraints to SAT form. A good parallel here can be drawn with sorting methods: in practice we can sort a numerical array via many different methods, and the context defines which one is better. In the present paper we will follow this path. Note, that the problem of finding MOLS with specific properties via SAT was already considered in a number of papers, for example in [14]. However, previous works did not study several significantly different encodings for the same problem and also did not 156 Mathematical and Information Technologies, MIT-2016 β€” Information technologies apply parametrization algorithms to tune solver performance. In the following subsection let us briefly introduce basic notation related to SAT. 2.1 SAT Basics Boolean formula is constructed from Boolean variables 𝑋 = {π‘₯1 , . . . , π‘₯𝑛 }, logical operators {Β¬, ∨, ∧} and parentheses. A literal is either a Boolean variable or its negation. A formula is called satisfiable if we can find such an assignment of logical values {TRUE, FALSE} (for simplicity it is usually assumed that TRUE is equivalent to 1 and FALSE is equivalent to 0) to its variables that the result is TRUE. Otherwise the formula is called unsatisfiable. An assignment of logical values that makes formula TRUE is called a satisfying assignment. Boolean satisfiability problem consists in answering the question if a given formula is satisfiable [4]. In practice a SAT solving algorithm needs to either find a satisfying assignment or to prove that formula is unsatisfiable. Usually, state-of-the-art SAT solving algorithms work with Boolean formulas represented in Conjunctive Normal Form (CNF). CNF is essentially a conjunction of clauses, where by clause we mean a disjunction of several literals or a single (unit) literal. An arbitrary formula can be effectively represented in CNF using Tseitin transformations [11]. In the following subsection we will consider the process of constructing different SAT encodings for finding MOLS in more detail. 2.2 Reducing the Problem of Search for MOLS to SAT Let us first represent the problem of search for MOLS as a problem of satisfying a set of constraints on Boolean variables. Latin square of order 𝑛 can be represented as an incidence cube [9] β€” an 𝑛×𝑛×𝑛 0βˆ’1 array where dimensions are identified with the rows, columns and symbols of a Latin square. Cell with coordinates (𝑖, 𝑗, π‘˜) contains 1 if and only if the cell of the corresponding Latin square with coordinates (𝑖, 𝑗) contains π‘˜. From the definition of Latin square it follows that if we fix two coordinates in incidence cube, then in the remaining β€˜line’ of the cube, produced by varying the remaining coordinate, there should be exactly one 1. Thus to represent the Latin square we use 𝑛3 Boolean variables {π‘₯(𝑖, 𝑗, π‘˜)}, 𝑖, 𝑗, π‘˜ = 1, . . . , 𝑛, encoding the incidence cube. Let us introduce the general form of 𝐸𝑂 predicate: assume that 𝑋 = {π‘₯1 , . . . , π‘₯π‘š } is a set of Boolean variables. Then 𝐸𝑂(𝑋) = 𝐸𝑂(π‘₯1 , . . . , π‘₯π‘š ) = 1 if and only if among π‘₯1 , . . . , π‘₯π‘š exactly one variable takes the value of TRUE and all remaining variables take the value of FALSE. We will consider the ways this predicate can be transformed to CNF below. Then the Latin square can be specified using following constraints: 𝐸𝑂(π‘₯(𝑖, 𝑗, 1), . . . , π‘₯(𝑖, 𝑗, 𝑛)), 𝑖, 𝑗 = 1, . . . , 𝑛; 𝐸𝑂(π‘₯(𝑖, 1, π‘˜), . . . , π‘₯(𝑖, 𝑛, π‘˜)), 𝑖, π‘˜ = 1, . . . , 𝑛; 𝐸𝑂(π‘₯(1, 𝑗, π‘˜), . . . , π‘₯(𝑛, 𝑗, π‘˜)), 𝑗, π‘˜ = 1, . . . , 𝑛. 157 Mathematical and Information Technologies, MIT-2016 β€” Information technologies If we consider a diagonal Latin square, then we add two more constraints on varaibles corresponding to main diagonal and antidiagonal: 𝐸𝑂(π‘₯(1, 1, π‘˜), . . . , π‘₯(𝑛, 𝑛, π‘˜)), π‘˜ = 1, . . . , 𝑛; 𝐸𝑂(π‘₯(1, 𝑛, π‘˜), . . . , π‘₯(𝑛, 1, π‘˜)), π‘˜ = 1, . . . , 𝑛. Since we encode the problem of finding MOLS, we also need to specify the orthogonality condition. Let us remind that Latin squares 𝐴 and 𝐡 are orthog- onal if all ordered pairs of the form (π‘Žπ‘–π‘— , 𝑏𝑖𝑗 ) are distinct. Assume that variables {π‘₯𝐴 (𝑖, 𝑗, π‘˜)} correspond to square 𝐴 and variables {π‘₯𝐡 (𝑖, 𝑗, π‘˜)} correspond to square 𝐡. One way (usually referred to as naive) to represent orthogonality condition in the form of CNF is to write β‰ˆ 𝑛6 clauses of the kind: Β¬π‘₯𝐴 (𝑖1 , 𝑗1 , π‘˜1 ) ∨ Β¬π‘₯𝐴 (𝑖2 , 𝑗2 , π‘˜2 ) ∨ Β¬π‘₯𝐡 (𝑖1 , 𝑗1 , π‘˜1 ) ∨ Β¬π‘₯𝐡 (𝑖2 , 𝑗2 , π‘˜2 ), 𝑖1 , 𝑖2 , 𝑗1 , 𝑗2 , π‘˜1 , π‘˜2 = 1, . . . , 𝑛, 𝑖1 ΜΈ= 𝑖2 , 𝑗1 ΜΈ= 𝑗2 . Each of these clauses restricts that the ordered pair (π‘˜1 , π‘˜2 ) appears simultane- ously in two different cells with coordinates (𝑖1 , 𝑗1 ) and (𝑖2 , 𝑗2 ). An alternative variant of representing orthogonality condition in CNF relies on the use of auxiliary variables. Assume we use 𝑛2 arrays of 𝑛2 Boolean variables 𝑂𝐢[𝑒, 𝑣] = (π‘œπ‘π‘’,𝑣 𝑒,𝑣 1,1 , . . . , π‘œπ‘π‘›,𝑛 ), 𝑒, 𝑣 = 1, . . . , 𝑛. With each varaible from these arrays we associate the following Boolean equation π‘œπ‘π‘’,𝑣 𝐴 𝐡 𝑖,𝑗 ≑ π‘₯ (𝑖, 𝑗, 𝑒) ∧ π‘₯ (𝑖, 𝑗, 𝑣) i.e. if the pair (𝑒, 𝑣) is formed by elements of Latin squares with coordinates (𝑖, 𝑗) then the corresponding Boolean variable π‘œπ‘π‘’,𝑣 𝑖,𝑗 takes the value of TRUE. After this the orthogonality condition can be written using the following constraints: 𝐸𝑂(𝑂𝐢[π‘˜1 , π‘˜2 ]), π‘˜1 , π‘˜2 = 1, . . . , 𝑛. It is clear that by employing different encoding schemes for 𝐸𝑂 predicate we can produce different SAT encodings for finding MOLS. Let us consider the 𝐸𝑂 predicate in more detail. 2.3 Encoding 𝐸𝑂 predicate In recent years there had been published several variants of algorithms for encod- ing it to SAT. The paper [10] contains quite comprehensive and detailed review of them. Below let us briefly cite the encoding variants described in [10] that we will use in our experiments. Assume that 𝑋 = (π‘₯1 , . . . , π‘₯π‘š ). It is convenient to split the EO predicate into two: 𝐸𝑂(𝑋) = 𝐴𝑀 𝑂(𝑋) ∧ 𝐴𝐿𝑂(𝑋) where 𝐴𝑀 𝑂(𝑋) is the predicate encoding that among the variables from the set 𝑋 there is at most one with the value of TRUE, and 𝐴𝐿𝑂(𝑋) is a predicate encoding that at least one variable in 𝑋 takes the value of TRUE. The encoding 158 Mathematical and Information Technologies, MIT-2016 β€” Information technologies of 𝐴𝐿𝑂 predicate to CNF is relatively straightforward – it can be written via one big clause: 𝐴𝐿𝑂(π‘₯1 , . . . , π‘₯π‘š ) = π‘₯1 ∨ . . . ∨ π‘₯π‘š . It is the 𝐴𝑀 𝑂 predicate that requires a more thorough consideration. The most simple way to transform it to CNF is the so-called Pairwise encoding. It implies the construction of π‘š Γ— (π‘š βˆ’ 1)/2 clauses of the kind ¬𝑣𝑖 ∨ ¬𝑣𝑗 , 𝑖, 𝑗 = 1, . . . π‘š, 𝑖 ΜΈ= 𝑗. Pairwise encoding is the only encoding we used that does not employ auxiliary variables for encoding 𝐴𝑀 𝑂 predicate. When we use Binary encoding to transform 𝐴𝑀 𝑂 predicate to CNF we introduce auxiliary variables 𝑏1 , . . . , π‘βŒˆπ‘™π‘œπ‘”2 π‘šβŒ‰ . Then with each variable π‘₯𝑖 ∈ 𝑋, 𝑖 = 1, . . . , π‘š we associate a set of clauses: βŒˆπ‘™π‘œπ‘”2 π‘šβŒ‰ ⋀︁ Β¬π‘₯𝑖 ∨ πœ“(𝑖, 𝑗), 𝑗=1 where πœ“(𝑖, 𝑗) denotes 𝑏𝑖 (¬𝑏𝑖 ) if the 𝑗-th bit of binary representation of 𝑖 βˆ’ 1 is 1(0). The idea behind the encoding is to create such situation that when any π‘₯𝑖 is assigned the value of TRUE it leads to the assignment of all auxiliary variables 𝑏1 , . . . , π‘βŒˆπ‘™π‘œπ‘”2 π‘šβŒ‰ and thus to assigning the value of FALSE to all other π‘₯𝑗 , 𝑗 ΜΈ= 𝑖. The Commander encoding can be considered a meta-encoding method as it can employ other encodings. It is based on dividing the set 𝑋 into π‘˜ disjoint subsets 𝐺1 , . . . , πΊπ‘˜ . Then we introduce auxiliary commander variables 𝑐1 , . . . , π‘π‘˜ that act as representatives of corresponding subsets. After this we write the following set of clauses π‘˜ ⋀︁ π‘˜ ⋀︁ 𝐴𝑀 𝑂(¬𝑐𝑖 βˆͺ 𝐺𝑖 ) ∧ 𝐴𝐿𝑂(¬𝑐𝑖 βˆͺ 𝐺𝑖 ) ∧ 𝐴𝑀 𝑂(𝑐1 , . . . , π‘π‘˜ ). 𝑖=1 𝑖=1 The idea is that once a variable π‘₯𝑖 becomes TRUE, the corresponding comman- der variable also becomes TRUE, and thus all π‘₯𝑗 , 𝑗 ΜΈ= 𝑖 are assigned FALSE. In Product encoding we introduce 𝑝 + π‘ž auxiliary variables π‘ˆ = {𝑒1 , . . . , 𝑒𝑝 } and 𝑉 = {𝑣1 , . . . , π‘£π‘ž }, 𝑝 Γ— π‘ž β‰₯ π‘š. Then each variable π‘₯π‘˜ , π‘˜ = 1, . . . , π‘š is mapped to a pair (𝑒𝑖 , 𝑣𝑗 ), such that π‘˜ = (𝑖 βˆ’ 1)π‘ž + 𝑗. Then the following set of clauses: 1β‰€π‘˜β‰€π‘š,π‘˜=(π‘–βˆ’1)π‘ž+𝑗 ⋀︁ 𝐴𝑀 𝑂(𝑋) = 𝐴𝑀 𝑂(π‘ˆ ) ∧ 𝐴𝑀 𝑂(𝑉 ) (Β¬π‘₯π‘˜ ∨ 𝑒𝑖 ) ∧ (Β¬π‘₯π‘˜ ∨ 𝑣𝑗 ) 1≀𝑖≀𝑝,1β‰€π‘—β‰€π‘ž guarantees that once π‘₯π‘˜ is assigned TRUE, the corresponding pair of variables (𝑒𝑖 , 𝑣𝑗 ) are also assigned TRUE and it leads to assigning FALSE to remaining π‘₯𝑑 , 𝑑 ΜΈ= π‘˜. The Sequential encoding implements the idea of sequential counter, where we traverse the set of variables in the ordered fashion and track if we already 159 Mathematical and Information Technologies, MIT-2016 β€” Information technologies met a variable with the value of TRUE. It employs π‘š βˆ’ 1 auxiliary variables 𝑠1 , . . . , π‘ π‘›βˆ’1 in the following set of clauses: ⋀︁ (Β¬π‘₯1 ∨ 𝑠1 ) ∧ (Β¬π‘₯π‘š ∨ Β¬π‘ π‘›βˆ’1 ) (Β¬π‘₯𝑖 ∨ 𝑠𝑖 ) ∧ (Β¬π‘ π‘–βˆ’1 ∨ 𝑠𝑖 ) ∧ (Β¬π‘₯𝑖 ∨ Β¬π‘ π‘–βˆ’1 ). 1<𝑖<𝑛 Finally, the Bimander encoding combines the features of Binary and comman- der encodings in the following way. Similarly to commander encoding the original set 𝑋 is divided into π‘˜ disjoint subsets 𝐺1 , . . . , πΊπ‘˜ , such that each group 𝐺𝑖 con- tains 𝑔 = ⌈ π‘š π‘˜ βŒ‰ variables. Then we introduce auxiliary variables 𝑏1 , . . . , π‘βŒˆπ‘™π‘œπ‘”2 π‘šβŒ‰ similar to binary encoding and write the following set of clauses: βŽ› ⎞ π‘˜ ⋀︁ 𝑔 βŒˆπ‘™π‘œπ‘” ⋀︁ ⋀︁2 π‘˜βŒ‰ βŽπ΄π‘€ 𝑂(𝐺𝑖 ) ∧ Β¬π‘₯𝑖,β„Ž ∨ πœ“(𝑖, 𝑗)⎠ , 𝑖=1 β„Ž=1 𝑗=1 where πœ“(𝑖, 𝑗) has the same meaning as in binary encoding. We applied all considered encoding methods to construct different SAT en- codings for several problems of finding pairs and triples of MOLS of various order. The results are presented in Table 1. Since the size difference between SAT encodings for finding MOLS and MODLS is relatively little, we compare only encodings for finding MOLS. The columns naive, pw, bn, cm, pr, sq, bm correspond to naive, pairwise, binary, commander, product, sequential and bimander encoding schemes, respectively. Note, that we applied them only to encode EO predicates corresponding to orthogonality condition. EO predicates corresponding to constraints on incidence cube were encoded using pairwise en- coding in all cases. Below we refer to problem of finding π‘˜ MOLS (MODLS) of order 𝑛 as 𝑀 𝑂𝐿𝑆 𝑛 π‘˜ (𝑀 𝑂𝐷𝐿𝑆 𝑛 π‘˜). For 𝑛 = 8, 9 we used 𝑝 = 3, π‘ž = 3 for product encoding and π‘š = 3 for bimander and comander encodings, and for 𝑛 = 10 we used 𝑝 = 3, π‘ž = 4, π‘š = 3. Table 1. Size of SAT encodings for finding MOLS constructed using different AMO encoding schemes, Kb. Problem naive pw bn cm pr sq bm MOLS 8 2 2 371 2 233 691 660 508 512 727 MOLS 8 3 7 326 6 757 1 952 1 857 1 383 1 420 2 059 MOLS 9 2 5 164 4 415 1 224 1 126 836 864 1330 MOLS 9 3 15 752 13 877 3 551 3 234 2 292 2 336 3 889 MOLS 10 2 10 198 8 343 1 930 1 856 1 328 1 363 2 169 MOLS 10 3 30 893 26 185 5 515 5 269 3 566 3 618 6 287 3 Parametrization of SAT solving algorithms State-of-the-art SAT solvers are programs with a large number of various param- eters. Meticulous tuning of these parameters for a particular class of problems 160 Mathematical and Information Technologies, MIT-2016 β€” Information technologies may significantly improve average effectiveness of the solver: sometimes it is even possible to achieve more than 100 times better performance. There are some generally accepted techniques for parametrization of SAT solvers. According to papers [8, 7, 1] one should select from the considered set of SAT instances some subset called training set. On this training set the SAT solver with different combinations of parameter values is launched. For each com- bination of parameter values a special objective function is computed to measure the effectiveness of SAT solving with these values. The parametrization process itself is essentially a local search in a Cartesian product of domains containing all possible values of considered parameters. So all the solver parameters must be discrete (each non-discrete parameter should be discretized). To jump from local optimums sometimes various metaheuristic procedures are used. When the local search scheme finishes its work either due to reaching the optimality condition or because time limit was exceeded, the resulting combination of parameters is applied to solve all problems from the so-called test set. By test set it is usu- ally meant the set of test instances used to measure the effectiveness of the parametrization procedure. Usually it is assumed that test set and training set do not intersect. In practice, given some test set one employs reasonable heuris- tics to form training set using problems of the same nature and similar dimension as in test set. There are three state-of-the-art tools for tuning the parameters of SAT solvers: ParamILS (Iterated Local Search in Parameter Configuration Space [8]), GGA (Gender-based Genetic Algorithm [1]) and SMAC (Sequential Model- based Algorithm Configuration [7]). All mentioned tools are based on some local search metaheuristics. GGA uses the genetic algorithm, ParamILS and SMAC are based on the iterative hill climbing algorithm. Using these tools one can speed up both local search and tree search SAT algorithms. With the help of these tools two Configurable SAT Solver Challenges (CSSC) in 2013 and 2014 were held. According to [7] SMAC shows better efficiency compared to ParamILS and GGA. That is why in our computational experiments we used SMAC. One of the last stages in the development of a SAT solver consists in fixing default values of its parameters. Usually to find such values developers use one of the mentioned tools. During this process the families of SAT instances from the latest SAT competitions are usually used as a training set. One of the reasons of such choice is that these families are formed by SAT encodings of problems from various areas of science. The set of values that has showed the best performance on the training set is finally utilized in the role of the default set of the parame- ters values. As a result the tuned solver shows good performance in application to the wide class of problems. Meanwhile, in practice one often faces the situa- tion when it is necessary to solve large amount of SAT instances which encode almost identical combinatorial problems. Often such combinatorial problems are obtained by decomposing an original combinatorial problem. In the next section this situation will be described in application to finding systems of MOLS and MODLS. 161 Mathematical and Information Technologies, MIT-2016 β€” Information technologies We chose the lingeling SAT solver [3] for tuning, because at CSSC 2014 it won the gold medals in all categories (Random SAT, Random SAT+UNSAT, Industrial SAT+UNSAT, Crafted SAT+UNSAT). There are 323 parameters in lingeling available for tuning. In the next section we will show how this solver works with the default values of parameters on SAT instances built according to the SAT encodings described in the previous section. Then we will describe the results of its tuning in application to some problems which turned out to be very hard. 4 Computational experiments To compare the effectiveness of SAT solvers on the SAT encodings described in Section 2 we considered the following combinatorial problems: – MOLS 8 2; – MOLS 9 2; – MOLS 10 2; – MODLS 8 2; – MODLS 8 3; – MODLS 10 2; – MODLS 10 3. For each of these problems we made all 7 considered SAT encodings. In our experiments besides lingeling, we used plingeling and treengeling SAT solvers [3]. We chose them because they won several prizes on the latest SAT competition and SAT Race (they were held in 2014 and 2015 respectively). In particular, we used the versions from SAT Race 2015 for all solvers. Note that plingeling and treengeling are multi-threaded programs, while lingeling is a sequential program. We utilized the experimental setup consisting of two 16- core AMD 6276 processors coupled with 64 Gb RAM. Thus, each multi-threaded solver was launched on 32 cores. On the first stage we launched each of the mentioned solvers with the default values of parameters on every SAT instance (49 SAT instances in total). In this experiment we used the time limit of 5000 seconds for every launch. This limit corresponds to the wall time, so for a sequential solver it is almost identical to CPU time, but in the case of multi-threaded solvers the CPU time can be much greater. It should be noted that this is a standard wall time limit used at SAT competitions. In Tables 2, 3 and 4 the results of the described experiment are shown. Each value in these tables corresopnds to the CPU time in seconds. Here β€œ-” stands for β€œinterrupted due to exceeding the time limit”. The best value for each pair (problem, type of the SAT encoding) is marked with bold. Let us discuss the obtained results. In every case when a solver could cope with a SAT instance, the answer was SATISFIABLE. Problems MODLS 10 2 and MODLS 10 3 turned out to be very hard β€” no pair (SAT solver, SAT encoding) could cope with them. On the considered test instances two variants of SAT encodings (bm and pw) turned out to be quite mediocre. Interesting 162 Mathematical and Information Technologies, MIT-2016 β€” Information technologies Table 2. CPU time for lingeling with the default parameters values, seconds. Problem naive pw bn cm pr sq bm MOLS 8 2 50 151 2489 674 1718 158 276 MOLS 9 2 - - - - - - - MOLS 10 2 2404 - - - - - - MODLS 8 2 50 200 957 1890 290 847 248 MODLS 8 3 - - - - - - - MODLS 10 2 - - - - - - - MODLS 10 3 - - - - - - - Table 3. CPU time for plingeling, seconds. Problem naive pw bn cm pr sq bm MOLS 8 2 13.7 0.4 25.5 0.2 0.1 0.2 620.6 MOLS 9 2 5581 20135 142346 40396 4516 15141 - MOLS 10 2 9169 73653 - - - - 38935 MODLS 8 2 1400 512 1272 2850 91 851 3617 MODLS 8 3 - - - - - - - MODLS 10 2 - - - - - - - MODLS 10 3 - - - - - - - Table 4. CPU time for treengeling, seconds. Problem naive pw bn cm pr sq bm MOLS 8 2 19 779 4976 536 9 643 31 MOLS 9 2 32569 29626 153762 26940 32175 9290 53727 MOLS 10 2 18710 102101 - 6111 - - - MODLS 8 2 437 739 391 1567 1269 2574 698 MODLS 8 3 - - - - - 44986 145142 MODLS 10 2 - - - - - - - MODLS 10 3 - - - - - - - Table 5. CPU time of parametrized lingeling on test sets, seconds. Problem naive pw bn cm pr sq bm MODLS 10 2, 5.73 9.28 9.78 13.30 8.80 11.79 10.83 6 rows known MODLS 10 3, 13.52 29.47 32.02 36.17 35.45 44.34 32.74 6 rows known 163 Mathematical and Information Technologies, MIT-2016 β€” Information technologies fact is that plingeling showed superlinear speed up (compared to lingeling) on MOLS 8 2. On lingeling in all cases the best results were obtained using naive SAT encoding, however plingeling and treengeling in almost all cases displayed the best results with other encodings. Finally, the best CPU times for MOLS 8 2 and MOLS 9 2 were obtained by plingeling on pr encoding; for MOLS 10 2 and MODLS 8 2 β€” by lingeling on naive SAT encoding; for MODLS 8 3 β€” by treengeling on sq SAT encoding. In [13] we considered weakened problems for MODLS 10 3 in which the val- ues of the first 45 cells of the first DLS were added to an original CNF via unit clauses. The corresponding SAT instances turned out to be quite hard. In the present paper we considered another type of weakened problems for MODLS 10 3. We constructed 100 SAT instances by adding to an original CNF the values of the first 6 rows of the first DLS via unit clauses. We also made 100 SAT instances for MODLS 10 2 in the similar way. Following [13] we took the corresponding values from the first 50 pairs of MODLS of order 10 found in the volunteer computing project SAT@home [12]. As a result we obtained 100 relatively simple (for lingeling with the default parameters values) SAT instances for each of the considered problems. We used SMAC (see Section 3) to find good lingeling parameters values for the obtained families of instances. In every case as the training set we used the first 10 SAT instances from a family, thus the remaining 90 SAT instances formed the test set. In every case SMAC was launched 16 times, each of them for 1 day (with different values of the start seeds). The final performance of the solver on test sets for each type of encoding is presented in Table 5 (the best one out of 16 SMAC results was chosen in every case). Let us discuss the obtained results. For both considered weakened prob- lems the naive encoding turned out to be better than others. With the help of parametrization the speed-up of 49 % (40 %) was achieved for the weakened problem MODLS 10 2 (MODLS 10 3) on this encoding in comparison with the default parameters values. 5 Conclusion The results of computational experiments clearly show that it is very important to choose the best pair (SAT solver, SAT encoding) for a particular combinatorial problem. The parametrization of the chosen SAT solver also can provide an additional speed-up. In future we plan to evaluate other types of SAT encodings for the considered problems, such as the ones based on representing Latin squares via orthogonal arrays, sets of transversals, etc. We also plan to utilize other tools for the SAT solvers parameters tuning. Acknowledgments. The research was funded by Russian Science Foundation (project No. 16-11-10046). 164 Mathematical and Information Technologies, MIT-2016 β€” Information technologies References 1. Ansótegui, C., Sellmann, M., Tierney, K.: A gender-based genetic algorithm for the automatic configuration of algorithms. In: Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming. pp. 142–157. CP’09, Springer-Verlag, Berlin, Heidelberg (2009) 2. Balint, A., Belov, A., Järvisalo, M., Sinz, C.: Overview and analysis of the SAT challenge 2012 solver competition. Artif. Intell. 223, 120–155 (2015) 3. Biere, A.: Lingeling essentials, A tutorial on design and implementation aspects of the the SAT solver lingeling. In: Berre, D.L. (ed.) POS-14. Fifth Pragmatics of SAT workshop, a workshop of the SAT 2014 conference, part of FLoC 2014 during the Vienna Summer of Logic, July 13, 2014, Vienna, Austria. EPiC Series, vol. 27, p. 88. EasyChair (2014) 4. Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satis- fiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (February 2009) 5. Colbourn, C.J., Dinitz, J.H.: Handbook of Combinatorial Designs, Second Edition (Discrete Mathematics and Its Applications). Chapman & Hall/CRC (2006) 6. Cook, S.A.: The complexity of theorem-proving procedures. In: Harrison, M.A., Banerji, R.B., Ullman, J.D. (eds.) Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA. pp. 151–158. ACM (1971) 7. Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Proc. of LION-5. p. 50723 (2011) 8. Hutter, F., Hoos, H.H., Stützle, T.: Automatic algorithm configuration based on local search. In: Proc. of the Twenty-Second Conference on Artifical Intelli- gence (AAAI ’07). pp. 1152–1157 (2007) 9. Jacobson, M.T., Matthews, P.: Generating uniformly distributed random latin squares. Journal of Combinatorial Designs 4(6), 405–437 (1996) 10. Nguyen, V.H., Mai, S.T.: A new method to encode the at-most-one constraint into sat. In: Proceedings of the Sixth International Symposium on Information and Communication Technology. pp. 46–53. SoICT 2015, ACM, New York, NY, USA (2015) 11. Tseitin, G.S.: Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, chap. On the Complexity of Derivation in Propositional Calculus, pp. 466–483. Springer Berlin Heidelberg, Berlin, Heidelberg (1983) 12. Zaikin, O., Kochemazov, S., Semenov, A.: SAT-based search for systems of diag- onal latin squares in volunteer computing project SAT@home. In: Biljanovic, P., Butkovic, Z., Skala, K., Grbac, T.G., Cicin-Sain, M., Sruk, V., Ribaric, S., Gros, S., Vrdoljak, B., Mauher, M., Tijan, E., Lukman, D. (eds.) 39th International Convention on Information and Communication Technology, Electronics and Mi- croelectronics, MIPRO 2016, Opatija, Croatia, May 30 - June 3, 2016. pp. 277–281. IEEE (2016) 13. Zaikin, O., Zhuravlev, A., Kochemazov, S., Vatutin, E.: On the construction of triples of diagonal Latin squares of order 10. Electronic Notes in Discrete Mathe- matics 54, 307–312 (2016) 14. Zhang, H.: Combinatorial designs by SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 533–568. IOS Press (2009) 165