Abstract
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.
| Original language | English |
|---|---|
| Title of host publication | AAAI-07/IAAI-07 Proceedings |
| Subtitle of host publication | 22nd AAAI Conference on Artificial Intelligence and the 19th Innovative Applications of Artificial Intelligence Conference |
| Pages | 1667-1670 |
| Number of pages | 4 |
| Publication status | Published - 2007 |
| Event | AAAI-07/IAAI-07 Proceedings: 22nd AAAI Conference on Artificial Intelligence and the 19th Innovative Applications of Artificial Intelligence Conference - Vancouver, BC, Canada Duration: 22 Jul 2007 → 26 Jul 2007 |
Publication series
| Name | Proceedings of the National Conference on Artificial Intelligence |
|---|---|
| Volume | 2 |
Conference
| Conference | AAAI-07/IAAI-07 Proceedings: 22nd AAAI Conference on Artificial Intelligence and the 19th Innovative Applications of Artificial Intelligence Conference |
|---|---|
| Country/Territory | Canada |
| City | Vancouver, BC |
| Period | 22/07/07 → 26/07/07 |