Refutation by Randomised General Resolution

Abstract

Local search is widely applied to satisfiable SAT prob-lems, 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 unsatisfia-bility. 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 resolu-tion 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 resolu-tion.