integers encoded with 5 bits) and with FlatZinc **specifications obtained from a** MiniZinc specification made in the style of the direct encoding,36 **we will denote them by 1 and 2.**
sugar **was used only with a specification that employs the order encoding.** ursa **was used**
with the specifications queens-1 **(with integers encoded with 5 bits),** queens-2 **(with the**
number of bits equal the instance dimension), and queens-3**, (with integers encoded with 4** bits). Table 6 presents the obtained experimental results. **All recorded times were obtained**
for the "quiet" mode of the sat **solver (without printing the models). Times for generating** formulae were negligible (compared to the solving phase) for all systems, so we don't report them here.

For related specifications, ursa's queens-1 **gave much smaller formulae (probably**
thanks to techniques mentioned in Section 6.2) and somewhat **better performance than**
FznTini **1, which suggests that** FznTini **does not benefit much from information about** the global structure of the problem. The formulae generated by sugar **were significantly** smaller than in the above two cases, and led to much better solving efficiency. However, it was outperformed by the remaining entrants. The ursa**'s specifications** queens-2 and queens-3 **gave similar results. The specification** queens-3 **produced formulae with the**
smallest number of clauses. FznTini **2 produced formulae with the smallest number of**
variables. The best results in terms of the solving times were obtained also by FznTini 2.

It can be concluded that ursa can produce, with suitable problem specifications, propositional formulae comparable in size and in solving times with **formulae produced by related**
state-of-the-art systems. Additional Experiments. In additional experiments, only the systems that performed the best on the queens problem were considered (with only one constraint logic programming system kept): B-prolog, clasp, FznTini, g12/fd**, and** ursa**. The following problems**
were considered (for all problems all solutions were sought):
Golomb Ruler: **The problem (actually, one of its variation) is as follows, given a value** L
check if there are m numbers a0, a1, . . ., am−1 such that 0 = a0 < a1 **< ... < a**m−1 = L
and all the m(m − 1)/2 differences aj − ai, 0 ≤ i < j ≤ m **are distinct (problem 6**
at CSPlib37). The experiments were performed for m = 5, . . . , **11, with the largest** L
that make the problem unsatisfiable and with the smallest L **that make the problem**
satisfiable.

Magic Square: A magic square of order N is a N × N **matrix containing the numbers**
from 0 to N2 − 1, with each row, column and main diagonal equal the same sum. The problem is to find all magic squares of order N **(problem 19 at CSPlib). The experiments** were performed for N = 3 and N **= 4.**
Linear Recurrence Relations: **Linear homogeneous recurrence relations of degree** k are of the form: Tn+k+1 = akTn+k + . . . + a1Tn+1 for n ≤ 0. Given T1, . . . , Tk and n, Tn can be simply calculated, but finding explicit formula for Ti **requires solving a**
nonlinear characteristic equation of degree k**, which is not always possible. So, the**
following problem is nontrivial: given T1, . . ., Tk−1 and Tn, find Tk**. For the experiment,**
we used the relation Tn+3 = Tn+2 + Tn+1 + Tn, T1 = T2 **= 1. We generated instances**
with the (only) solution T3 **= 1 and the systems were required to seek all possible values** for T3**. Additional constraints (used explicitly or implicitly) for all considered systems)**