@inbook{49fb9e42f2cf4c84924373f7f8ab3ec7,
title = "Local search for unsatisfiability",
abstract = "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.",
author = "Steven Prestwich and In{\^e}s Lynce",
year = "2006",
doi = "10.1007/11814948\_28",
language = "English",
isbn = "3540372067",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "283--296",
booktitle = "Theory and Applications of Satisfiability Testing, SAT 2006 - 9th International Conference, Proceedings",
address = "Germany",
note = "9th International Conference on Theory and Applications of Satisfiability Testing, SAT 2006 ; Conference date: 12-08-2006 Through 15-08-2006",
}