The above data are obtained using numbers represented by vectors of length 5. However, using the minimal vectors length is not critical - if a larger **vector size is used, only trivial** constraints are added and they have a very small impact on the **solving process. Table**
3 shows results for the above specification of the queens problem for instance size 10, for vectors length increasing from 5 to 12. The time for generating formulae slightly increases, the number of variables and clauses increases significantly, but the time spent for solving remains about the same for all vector lengths.

| number of bits   | 5    | 6    | 7    | 8    | 9     | 10    | 11    | 12    |
|------------------|------|------|------|------|-------|-------|-------|-------|
| variables        | 1286 | 1611 | 1936 | 2261 | 2586  | 2911  | 3236  | 3561  |
| clauses          | 5179 | 6604 | 8119 | 9724 | 11419 | 13204 | 15079 | 17044 |
| generating       | 0.02 | 0.02 | 0.02 | 0.03 | 0.03  | 0.04  | 0.04  | 0.04  |
| solving          | 3.12 | 3.26 | 3.38 | 3.19 | 3.37  | 3.13  | 3.22  | 3.23  |

Table 3: Experimental results for the queens-1 specification applied (for finding all solution) for N = 10 and for number representations using 5, 6, . . . , **12 propositional**
formulae The same problem can be represented in ursa **in other ways as well. For instance,**
the above specification can be slightly modified so it uses bit-wise operators, instead of arithmetic operators. Each row of the table can be represented as a N**-digits number, i.e.,** by an element of an array n**. Each of these numbers should have exactly one 1 in its binary** representations (which can be checked in the way described in Example 8.1), and at each position exactly one of n[i] **should have 1. The remaining (diagonal) no-attack conditions** (for pairs of positions represented by indexes (Ax,Ay) and (Bx,By**)) can be also expressed by**
using bit-wise operations. A corresponding ursa **specification (referred to as to** queens-2 in the following text) is as follows (it should be used with numbers represented as vectors of length N):
/* ***** queens-2 ***** */ nDim = 8; bHorizontal = true; for(ni=0; ni<nDim; ni++)
bHorizontal &&= ((n[ni] & n[ni]-1)==0) && (n[ni]!=0);
nVertical = 0; for(ni=0; ni<nDim; ni++)
nVertical |= n[ni];
bVertical = (nVertical+1 == 0);
bDiagonal = true; for(nAi=0; nAi<nDim-1; nAi++)
for(nAj=0; nAj<nDim; nAj++)
for(nBi=nAi+1; nBi<nDim; nBi++)
for(nBj=0; nBj<nDim; nBj++)
if (nBi-nAi==nBj-nAj || nBi-nAi==nAj-nBj)
bDiagonal &&= (((n[nBj]<<(nBi-nAi)) & n[nAj])==0);
assert_all(bHorizontal && bVertical && bDiagonal);
The queens problem can be represented also in the spirit of the direct encoding**. Namely,**
each position in the table is associated with one Boolean variable, so b[i][j] is set if and