appropriate number for this probability, mostly because, in the GUNSAT paper [2] the authors write that extended resolution is used after the algorithm has tried to increase the score of a given pair of literals
"too many times", but do not provide details. We chose Per = 5% which means it will be executed in
about 4.5% of the iterations (calculated by multiplying the 90% chance that the satisfiability-preserving
transformations phase will be run and the 5% chance that extended resolution will be executed within
that phase).
At the start of each phase of extended resolution, our algorithm will compute the scores for all the
pairs of literals in the working formula, in the same way that GUNSAT calculates its scores: each pair of
literals (l1,l2) appearing in the formula is credited a score computed by adding the score of each literal
in each clause ci according to the following formula: 2
n−1−n1
ni.(ni−1)
. We compute the score of each variable in
each clause and add them for each pair of literals. The score of a clause is then computed by summing
the scores of all the pairs of literals it contains. Finally, we calculate the score of each quadruplet by
adding the sum of the squares of the scores of its pairs of literals.
After the scores have been computed, we continue to follow GUNSAT's heuristic to improve the score
of a pair of literals (note that extended resolution will only be applied if we cannot improve the score
of a pair of literals after too many times). The best scored quadruplet in the formula is computed and
found, containing the literals l1 and l2. We then try to find a new clause with both l1 and l2 by searching
the working formula for two clauses: one containing l1 and a pivot literal p, and the other containing
l2 and the complement of the pivot literal, ¬p, such that the resolution rule can be performed and the
needed clause with l1 and l2 is generated. We only try to generate the new clause c from the two clauses
having the lowest scores. Because of this restriction, it is not always possible to generate a new clause according to the specified conditions (the cause could simply be that the new clause may be subsumed by an already existing clause, or it may be a tautology). If the score of one pair of the highest scored
quadruplet cannot be improved, the other scores of the same quadruplet are iteratively tried. If no pairs of literals in this quadruplet can be improved, the second best scored quadruplet is tried and so on.
Finally, the algorithm checks, for all pairs of literals, whether their score has been increased too many
times without any success or not. We set this value to 20, i.e., we consider the score of a pair of literals
to be increased too many times when that value reaches 20. If this occurs for literals l1 and l2 then three
new clauses will be added along with a new variable e:
$$\begin{array}{c}{{c_{1}=\left(\neg e\lor l_{1}\lor l_{2}\right)}}\\ {{c_{2}=\left(e\lor\neg l_{1}\right)}}\\ {{c_{3}=\left(e\lor\neg l_{2}\right)}}\end{array}$$

## As We Can See, There Is A Lot Of Implementation Work Needed To Add This Method To Ranger, Especially If We Apply It In The Same Way Gunsat Does. Computing The Scores And Looking For The New Clause
Is Very Demanding For The Algorithm, And We Are Adding An Additional Layer Of Complexity To Ranger, Whereas In Gunsat This Computation Was Already Part Of The Algorithm Itself. 5 Experimental Evaluation

This section illustrates the behaviour of RANGER on a set of problem instances. The instances consist of two benchmarks 1:
- The aim benchmark instances are all generated with a particular random 3-SAT instance generator [1]. Its primary role is to provide instances that the conventional random generation cannot

1Available from www.cs.ubc.ca/~hoos/SATLIB/benchm.html.