algorithm that can prove unsatisfiability rather than satisfiability. It explores a space of multisets of resolvents using general resolution and aims at deriving the empty clause non-systematically but greedily, thus proving unsatisfiability. RANGER will eventually refute any unsatisfiable instance while using only bounded memory.

A theoretical result behind the exploration of local search on multisets of resolvents can be found in [8]. The authors show that the space needed for a resolution proof is no more than n+1 resolvents, where n is the number of variables in the problem.

Given an unsatisfiable SAT formula ϕ with n variables and m clauses, a general resolution refutation can be represented by a series of formulae ϕ1,...,ϕs where ϕ1 consists of some or all of the clauses in ϕ, and ϕs contains the empty clause. Each ϕiis obtained from ϕi−1 by (optionally) deleting some clauses in ϕi−1, adding the resolvent of two clauses in ϕi−1, and (optionally) adding clauses from ϕ. The *space* of a proof is defined as the minimum k such that each ϕi contains no more than k clauses.

Intuitively, each ϕi represents the set of *active* clauses at step i of the proof. Inactive clauses are not required for future resolutions, and after they have been used as needed they can be deleted (for example clauses that are subsumed by others).

The *width* of a proof is the length (in literals) of the largest clause in the proof. Any non-tautologous clause must have length no greater than n, so this is a trivial upper bound for the *width* used in RANGER.

However, in practice, it may succeed even if the resolvent length is restricted to a smaller value, which will save memory on large problems. Each ϕi will be of the same constant size, and derived from ϕi−1 by the application of resolution or the replacement of a clause by one taken from ϕ.

The architecture of RANGER is shown in algorithm 1. It has six parameters: the formula ϕ, three probabilities pi, pt and pg, the width w and the size k of the formula ϕi.

The RANGER algorithm begins by choosing any k clauses from the formula ϕ into ϕ1. It then performs i iterations, either replacing a ϕi clause with a ϕ clause (with probability pi) or resolving two ϕi clauses and placing the result r into ϕi. In the latter case, if r is a tautology or contains more than w literals then it is discarded and ϕi+1 = ϕi. Otherwise a ϕi clause must be removed to make room for r: either (with probability pg) the removed clause is the longer of the two parents of r or it is randomly chosen. In the former case, if r is longer than the parent then r is discarded and ϕi+1 = ϕi. With probability pt any satisfiability-preserving transformation may be applied to ϕ, ϕi or both. One can apply subsumption and the pure literal rule in several ways as satisfiability-preserving transformations. If the empty clause has been derived then the algorithm returns UNSATISFIABLE, otherwise it may not terminate. A time-out condition may be added to restrict the CPU time that the algorithm is allowed to run.

In this algorithm the goal is to derive the empty clause, and as such ϕi must contain some small clauses. This is controlled by the level of greediness (probability pg). A greedy local move is one that does not increase the number of literals in ϕi. So, increasing pg will increase the greediness of the search, reducing the proliferation of large resolvents.

RANGER has a useful convergence property: for any unsatisfiable SAT problem with n variables and m clauses, it finds a refutation if pi > 0, pi, pt, pg < 1, w = n and k ≥ n+1. For a proof, see [14].

The space complexity of RANGER is O(n+m+kw). To guarantee convergence, it requires w = n and k ≥ n+1 so the space complexity becomes at least Om+n 2. In practice, it may require k to be several times larger, but a smaller value of w is usually sufficient.

It should be noted that RANGER performs very poorly on unsatisfiable random 3-SAT problems. This is an interesting asymmetry, given that local search performs well on satisfiable random problems. This may be because such refutations are almost certainly exponentially long [5].