=Paper= {{Paper |id=Vol-1839/MIT2016-p14 |storemode=property |title= The comparison of different SAT encodings for the problem of search for systems of orthogonal latin squares |pdfUrl=https://ceur-ws.org/Vol-1839/MIT2016-p14.pdf |volume=Vol-1839 |authors=Stepan Kochemazov,Oleg Zaikin, Alexander Semenov }} == The comparison of different SAT encodings for the problem of search for systems of orthogonal latin squares == https://ceur-ws.org/Vol-1839/MIT2016-p14.pdf

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. Ansó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., Jä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., Stü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