
| Number of iterations   |             |            |            |
|------------------------|-------------|------------|------------|
| Instance               | Original    | UPLA       | UPLA+ER    |
| aim−50−no−1 6          | 39,223      | 4,201      | 4,958      |
| aim−50−no−2 0          | 67,105      | 6,240      | 7,026      |
| aim−100−no−1 6         | 433,398     | 134,572    | 120,122    |
| aim−100−no−2 0         | 3,266,805   | 160,971    | 174,131    |
| aim−200−no−1 6         | 5,902,875   | 1,390,580  | 1,788,612  |
| aim−200−no−2 0         | 9,802,581   | 3,066,713  | 3,762,236  |
| uu f 50−218            | 174,752,209 | 43,620,471 | 5,139,0176 |

Table 4: Number of iterations for the RANGER variants reasoning mechanism and a finer heuristic to guide moves, whereas RANGER is simpler. Because of the use of powerful high reasoning techniques like unit propagation look-ahead and extended resolution, and a finer heuristic, GUNSAT's moves are slower but more intelligent and pondered, in contrast to RANGER's rather faster but blinder moves.

The integration of GUNSAT's techniques into RANGER, namely unit propagation look-ahead and extended resolution resulted in improving RANGER's performance overall with the first technique, whereas the second one has degraded RANGER's performance.

Future work includes further investigating why extended resolution impede the basic version of Ranger and using automatic methods to tune parameters, namely Per, such as the F-race proposed by Birattari *et al.* [4].

## Acknowledgements

This material is based in part upon works supported by the Science Foundation Ireland under Grant No. 05/IN/I886, and partially supported by Fundac¸ao para a Ci ˜ encia e Tecnologia under research project ˆ
PTDC/EIA/64164/2006.

## References

[1] Y. Asahiro, K. Iwama & E. Miyano (1996): *Random Generation of Test Instances with Controlled Attributes*.

In: D.S.Johnson and M.A.Trick, editors, Cliques, Coloring, and Satisfiability: The Second DIMACS Implementation Challenge. Vol. 26 of DIMACS Series on Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, pp. 377–394.

[2] G. Audemard & L. Simon (2007): *Gunsat: A greedy local search algorithm for unsatisfiability*. In: *International Joint Conference on Artificial Intelligence (IJCAI)*. pp. 2256–2261.

[3] F. Bacchus (2002): *Enhancing Davis Putnam with extended binary clause reasoning*. In: AAAI Conference on Artificial Intelligence. pp. 613–619.

[4] M. Birattari, T. Stutzle, L. Paquete & K. Varrentrapp (2002): ¨ *A racing algorithm for configuring metaheuristics*. In: *Genetic and Evolutionary Computation Conference (GECCO)*. pp. 11–18.

[5] V. Chvatal & E. Szemer ´ edi (1988): ´ Many hard examples for resolution. *Journal of the Association for* Computing Machinery 35(4), pp. 759–768.

[6] M. Davis, G. Logemann & D. Loveland (1962): A Machine Program for Theorem-Proving. *Communications* of the Association for Computing Machinery 5(7), pp. 394–397.