Local search is widely applied to satisfiable SAT problems, and on some classes outperforms backtrack search. An intriguing challenge posed by Selman, Kautz and McAllester in 1997 is to use it instead to prove unsatisfiability. We investigate two distinct approaches. Firstly we apply standard local search to a reformulation of the problem, such that a solution to the reformulation corresponds to a refutation of the original problem. Secondly we design a greedy randomised resolution algorithm that will eventually discover proofs of any size while using bounded memory. We show experimentally that both approaches can refute some problems more quickly than backtrack search. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Prestwich, S., & Lynce, I. (2006). Local search for unsatisfiability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4121 LNCS, pp. 283–296). Springer Verlag. https://doi.org/10.1007/11814948_28
Mendeley helps you to discover research relevant for your work.