arXiv:0910.1244v1 [cs.AI] 7 Oct 2009

# On Improving Local Search For Unsatisfiability

David Pereira Ines Lynce ˆ
IST/INESC-ID, Technical University of Lisbon, Portugal david,ines@sat.inesc-id.pt Steven Prestwich Cork Constraint Computation Centre, Dept of Computer Science, University College, Cork, Ireland s.prestwich@cs.ucc.ie Stochastic local search (SLS) has been an active field of research in the last few years, with new techniques and procedures being developed at an astonishing rate. SLS has been traditionally associated with satisfiability solving, that is, finding a solution for a given problem instance, as their intrinsic nature does not address unsatisfiable problems. Unsatisfiable instances were therefore commonly solved using backtrack search solvers. For this reason, in the late 90s Selman, Kautz and McAllester proposed a challenge to use local search instead to prove unsatisfiability. More recently, two SLS
solvers - RANGER and GUNSAT - have been developed, which are able to prove unsatisfiability albeit being SLS solvers. In this paper, we first compare RANGER with GUNSAT and then propose to improve RANGER performance using some of GUNSAT's techniques, namely unit propagation look-ahead and extended resolution.

## 1 Introduction

Selman, Kautz and McAllester posed an intriguing challenge in 1997 to use local search to prove unsatisfiability rather than satisfiability [18]. In 2006 and 2007, two different approaches were proposed in response to that challenge [14, 2]. These two algorithms - RANGER [14] and GUNSAT [2] - use local search to prove unsatisfiability instead of satisfiability, still being incomplete algorithms. They can, however, prove that a formula is satisfiable under certain conditions.

Previous work has addressed the use of hybrid algorithms combining clause learning with local search to prove either satisfiability or unsatisfiability [15, 9, 20] at the cost of having worst-case exponential space complexity. Alternative approaches combined unit clause elimination and local search [10].

We should note, however, that the algorithms just mentioned clearly differ from RANGER and GUN-SAT, which were built with the main goal of proving unsatisfiability by (directly or indirectly) deriving the empty clause. The main idea is to apply a sequence of resolution steps and other satisfiability preserving techniques to conclude that the formula has no solution.

Although based on the same ideas, RANGER and GUNSAT differ. RANGER is a lightweight algorithm that performs many moves per second, while GUNSAT applies more powerful reasoning techniques. This paper presents for the first time a detailed comparison of these two algorithms and further integrates some of GUNSAT techniques into RANGER.

This paper is organised as follows. The next section provides the required background. Section 3 describes and compares RANGER and GUNSAT. Afterwards, we describe the integration of GUNSAT's techniques into RANGER. Section 5 provides the experimental evaluation of the new techniques. Finally, the paper concludes.