
| Dimension                      | 8    | 9     | 10    | 11    | 12     | 13    | 14     |
|--------------------------------|------|-------|-------|-------|--------|-------|--------|
| FznTini 1: variables           | 3012 | 3825  | 4735  | 5742  | 6846   | 8047  | 9345   |
| clauses                        | 9128 | 11628 | 14460 | 17567 | 21000  | 24713 | 28770  |
| all solutions                  | 0.15 | 0.79  | 3.20  | 14.53 | 111.78 | >600  | >600   |
| ursa (queens-1): variables 841 | 1052 | 1286  | 1560  | 1819  | 2139   | 2468  |        |
| clauses                        | 3352 | 4217  | 5179  | 6295  | 7390   | 8712  | 10089  |
| all solutions                  | 0.08 | 0.53  | 2.83  | 17.60 | 98.04  | >600  | >600   |
| sugar: variables               | 220  | 284   | 356   | 436   | 524    | 620   | 724    |
| clauses                        | 1138 | 1653  | 2253  | 3012  | 3924   | 5003  | 6263   |
| all solutions                  | 0.02 | 0.06  | 0.31  | 1.58  | 9.59   | 68.07 | 411.15 |
| ursa (queens-2): variables 542 | 739  | 978   | 1263  | 1598  | 1987   | 2434  |        |
| clauses                        | 3319 | 5008  | 7280  | 10258 | 14077  | 18884 | 24838  |
| all solutions                  | 0.01 | 0.04  | 0.12  | 0.70  | 4.01   | 23.17 | 138.55 |
| ursa (queens-3): variables 176 | 225  | 280   | 341   | 408   | 481    | 560   |        |
| clauses                        | 800  | 1110  | 1490  | 1947  | 2488   | 3120  | 3850   |
| all solutions                  | 0.01 | 0.03  | 0.12  | 0.69  | 3.82   | 21.09 | 136.45 |
| FznTini 2: variables           | 128  | 162   | 200   | 242   | 288    | 338   | 392    |
| clauses                        | 872  | 1236  | 1690  | 2244  | 2908   | 3692  | 4606   |
| all solutions                  | 0.01 | 0.02  | 0.07  | 0.33  | 1.52   | 8.39  | 52.12  |

Table 6: Data on sat **formulae generated by** FznTini, sugar and ursa for the N **queens**
problem for N = 8, . . . , **14 and solved by the** clasp sat **solver**

were Ti > 0 and Ti ≤ Tn, for i = 1**, . . . , n**. ursa and FznTini **were used with 32 bit**
length for numerical values.

Non-linear recurrence relations: In non-linear homogenous recurrence relations of degree k, the link between Tn+k and Tn+k−1, Tn+k−2, . . ., Tn**, is not necessarily linear.**
For the experiment we used the relation Tn+4 = Tn+3 · Tn+2 + Tn+1, 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 of implicitly) for all**
considered systems) were Ti > 0 and Ti ≤ Tn, for i = 1, . . . , n**. For all problem instances,**
the size of all relevant values Ti **were smaller than 2**32. ursa and FznTini **were used**
with 32 bit length for numerical values.

The ursa **was used with the following specification for the Golomb ruler problem (for the** instance m = 7, L **= 25):**
nM=7; nL=25; bRulerEndpoints = num2bool(nRuler & nRuler >> nL & 1);
nMarks=2; bDistanceDiff=true; for(ni=1; ni<=nL-1; ni++) {
nMarks += (nRuler >> ni) & 1; n = (nRuler & (nRuler << ni));
bDistanceDiff &&= (n & (n-1))==0;