One of the objectives of this paper is to successfully integrate features of the GUNSAT algorithm into the RANGER algorithm. We do not want, however, to modify the most important properties of the original RANGER, nor alter its flow. The unit propagation look-ahead was, thus, added to the step of satisfiability-preserving transformations. The probability, Pt, to execute these transformations is 90%,
and like the other transformations, unit propagation will be executed, on average, in 90% of the iterations of the algorithm.

This procedure has been divided into two parts: unit propagation look-ahead with pairs of literals and unit propagation look-ahead with only one literal. The first one is only executed once, the first time that satisfiability-transformations are executed, due to the overhead it has on the performance of the solver. The second part of this procedure, which is less expensive, is executed in every satisfiability-preserving transformation.

Finally, note that these methods can prove the unsatisfiability of a formula themselves: if all possible assignments to a pair of variables result in conflicts then the formula is unsatisfiable; likewise, if for both possible assignments to a variable a conflict is detected, the algorithm also returns UNSATISFIABLE. It is also possible to find a solution during this step, though this occurs less frequently.

## 4.2 Implementing Extended Resolution

The way extended resolution is used in GUNSAT is intrinsically related to the algorithm itself, built to take advantage of its scoring scheme. Note that extended resolution is only used when the algorithm has tried to increase the score of a pair of literals too many times without success. It is very different from the way RANGER operates, where no scoring scheme for literals is used. Thus, we had to add GUNSAT's scoring scheme to RANGER to implement extended resolution in the same way it was successfully used in GUNSAT.

But there is a problem with this approach. GUNSAT's scoring system for pairs of literals is part of the main heuristic of the solver. It was developed to be the backbone of the algorithm and to be a highly refined heuristic of scoring for choosing the best literals and clauses to resolve. Methods like extended resolution, unit propagation look-ahead or binary clause saturation are only meant to improve this heuristic.

In the previous section, we described the way in which unit propagation look-ahead, a method also used in GUNSAT and which proved to yield successful results, was added to the original RANGER.

But this method was not intrinsically linked to the base of GUNSAT, as extended resolution is. One could simply add it as a preprocessing technique, or run it as a satisfiability preserving transformation to RANGER without loss of identity.

Even though adding extended resolution to RANGER seemed to be neither more efficient nor an easy task, and although it did not promise to integrate well with the already implemented algorithm and methods, we tried to integrate it with RANGER and to improve its performance on unsatisfiable instances. As said above, RANGER does not have a scoring scheme for literals like GUNSAT does, so that extended resolution could be applied directly to that scheme and be integrated seamlessly in the algorithm. Instead, we chose to adapt the scoring method of GUNSAT to RANGER and thus apply the extended resolution in the same way GUNSAT does.

Extended resolution is executed only during the satisfiability-preserving transformations phase of the RANGER algorithm, in the same way as unit propagation look-ahead with one variable is, and for the same reason: we did not want to alter RANGER's base concept and program flow. Furthermore, besides the probability Pt of this phase of the algorithm, we inserted another probability Per, and the steps of extended resolution will only be executed according to this probability. We had some trouble finding an