TY - GEN
T1 - Refutation by Randomised General Resolution
AU - Prestwich, Steven
AU - Lynce, Inês
N1 - Publisher Copyright:
Copyright © 2007, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
PY - 2007
Y1 - 2007
N2 - Local search is widely applied to satisfiable SAT problems, and on some problem classes outperforms backtrack search. An intriguing challenge posed by Selman, Kautz and McAllester in 1997 is to use it instead to prove unsatisfiability. We design a greedy randomised resolution algorithm called RANGER that will eventually refute any unsatisfiable instance while using only bounded memory. RANGER can refute some problems more quickly than systematic resolution or backtracking with clause learning. We believe that non-systematic but greedy inference is an interesting research direction for powerful proof systems such as general resolution.
AB - Local search is widely applied to satisfiable SAT problems, and on some problem classes outperforms backtrack search. An intriguing challenge posed by Selman, Kautz and McAllester in 1997 is to use it instead to prove unsatisfiability. We design a greedy randomised resolution algorithm called RANGER that will eventually refute any unsatisfiable instance while using only bounded memory. RANGER can refute some problems more quickly than systematic resolution or backtracking with clause learning. We believe that non-systematic but greedy inference is an interesting research direction for powerful proof systems such as general resolution.
UR - https://www.scopus.com/pages/publications/85167434042
M3 - Conference proceeding
AN - SCOPUS:85167434042
T3 - Proceedings of the 22nd AAAI Conference on Artificial Intelligence, AAAI 2007
SP - 1667
EP - 1670
BT - Proceedings of the 22nd AAAI Conference on Artificial Intelligence, AAAI 2007
PB - AAAI Press
T2 - 22nd AAAI Conference on Artificial Intelligence, AAAI 2007
Y2 - 22 July 2007 through 26 July 2007
ER -