
| n[2]=3 n[3]=5 n[4]=7 n[5]=1 n[6]=4 n[7]=2   |
|---------------------------------------------|

...

[Formula generation: 0s; conversion to CNF: 0.01s; total: 0.01s] [Solving time: 0.08s]
[Formula size: 841 variables, 3352 clauses]
In the above specification (referred to as to queens-1 in the following text), i**-th row**
(i = 0, . . . , N − 1) is associated with the i-th element the array n**. In each row there should** be one queen and n[i] **is equal to the column in which that queen is placed. The variable**
bDomain **encodes the condition that each** n[i] is between 0 and N − **1 and the variable** bNoCapture **encodes the condition that there are no two queens that attach each other.** If the numbers are represented by vectors of length l**, for each problem instance there are**
lN basic variables in the propositional formula generated. For N < **16, the numbers (and** intermediate results such as ni+n[nj]**) in the above specification can be represented by 5** bits. Table 2 shows experimental results for the above specification for the instance sizes N = 1, 2, 3, . . .**, 12 (instances for which all solutions were found within 600s), including** the number of solutions, the number of variables and clauses **in the generated propositional**
formula, and the time spent13 **for finding all solutions. The time spent for finding the first**
solution was less than 0.05s **for each problem instance. The time spent for generating the**
formulae was less than 0.01s **for each problem instance and was negligible compared to the** solving time. This shows that the used generation mechanism **is rather efficient. For these** problems (as well as for many other csp **problems), the ratio of the number of clauses and** the number of variables in the generated formulae, gets rather stable (as the size of the instance increases) and it reflects the problem constrainedness **[29].**

| --> Solution 92 n[0]=3 n[1]=1 n[2]=4 n[3]=7 n[4]=5 n[5]=0 n[6]=2 n[7]=6   |
|---------------------------------------------------------------------------|

![0_image_0.png](0_image_0.png)

Table 2: Experimental results for the queens-1 specification applied for N = 1**, . . . ,** 12 13 **Reported experimental results were obtained on a PC computer with Intel Celeron 420 1.60Ghz, 1Gb**
RAM, for ursa **using** clasp **as the underlying** sat solver.