GUNSAT: A Greedy Local Search Algorithm for Unsatisfiability

Gilles Audemard, Laurent Simon

Local search algorithms for satisfiability testing are still the best methods for a large number of problems, despite tremendous progresses observed on complete search algorithms over the last few years. However, their intrinsic limit does not allow them to address UNSAT problems. Ten years ago, this question challenged the community without any answer: was it possible to use local search algorithm for UNSAT formulae? We propose here a first approach addressing this issue, that can beat the best resolution-based complete methods. We define the landscape of the search by approximating the number of filtered clauses by resolution proof. Furthermore, we add high-level reasoning mechanism, based on Extended Resolution and Unit Propagation Look-Ahead to make this new and challenging approach possible. Our new algorithm also tends to be the first step on two other challenging problems: obtaining short proofs for UNSAT problems and build a real local-search algorithm for QBF.

URL: http://www.lri.fr/~simon/recherche/papiers/simon-audemard-ijcai07.pdf