
## 2 Background

We assume the basic definitions in the context of propositional satisfiability. A propositional formula ϕ is a conjunction of clauses, where a clause c is a disjunction of literals and a literal l is either a variable or its negation, being either a positive or a negative literal, respectively. Each variable ν can be assigned a truth value (true or false, also often referred to as 1 or 0, respectively). A positive literal l is said to be satisfied (unsatisfied) if the corresponding variable is assigned value true (false). A negative literal l is said to be satisfied (unsatisfied) if the corresponding variable is assigned value false (true).

A clause is said to be satisfied if at least one of its literals is satisfied, unsatisfied if all of its literals are unsatisfied and unresolved otherwise. Unresolved clauses with only one unassigned literal are said to be unit. A formula is satisfied if all of its clauses are satisfied. The propositional satisfiability (SAT) problem consists in deciding whether there exists a truth assignment to the variables such that the formula becomes satisfiable. Such an assignment is called a solution.

Two of the most well-known complete algorithms for SAT, which both still inspire current state of the art algorithms, are the Davis-Putnam (DP) [7] and the Davis-Logemann-Loveland (DLL) [6] algorithms. The first one is based on the resolution principle [16], whereas the second one is based on backtrack search. An important feature on a backtrack search algorithm for SAT is the use of unit propagation. Clearly, a unit clause has only one way to be satisfied, which implies satisfying its unassigned literal.

This rule may be iteratively applied until no unit clauses remain in the formula.

Local search algorithms, in contrast, are incomplete as they are not able to prove unsatisfiability:
either they find a solution or the answer is *unknown*, which means that either the formula has no solution or the solver was not able to find a solution in the allowed CPU time.

Local search algorithms start at some location in the given problem's search space and then move from the start location to a neighbouring location in the search space which is determined by a decision based on local knowledge only. These local search algorithms are typically incomplete, that is, there is no guarantee that an existing solution will be found, and if no solution exists that fact can never be determined with certainty. Furthermore, these search methods can visit the same location in the search space more than once, and they can become trapped in a small number of locations from which they cannot escape: these are called *local minima*, which will be discussed shortly, and require special *escape* strategies.

Many widely known and high-performance local search algorithms make use of randomized choices when generating and/or selecting candidate solutions for a given problem [11]. These algorithms are called *stochastic local search* (SLS) algorithms, and they belong to the most powerful methods for practically solving large and hard satisfiable instances of SAT, and outperform the best systematic search methods on a number of domains. In SLS algorithms, the initial position in the search space is chosen randomly, as are the decisions to move from a position to another. Two early but influential stepping stones in SLS algorithm development are GSAT [19] and WalkSAT [17].

## 3 Local Search For Unsatisfiability

RANGER and GUNSAT are two stochastic local search algorithms which resemble the skeleton of SLS
algorithms, but on the other hand aim at deriving the empty clause to prove unsatisfiability.

## 3.1 Ranger

RANGER [14] stands for RANdomized GEneral Resolution and was presented in 2006 as the first SLS