Conference Paper/Proceeding/Abstract 1007 views
Generalising and Unifying SLUR and Unit-Refutation Completeness
SOFSEM 2013: Theory and Practice of Computer Science. LCNS, Volume: 7741, Pages: 220 - 232
Swansea University Author:
Oliver Kullmann
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1007/978-3-642-35843-2_20
Abstract
The class SLUR (Single Lookahead Unit Resolution) was introduced in [Schlipf, Annexstein, Franco, Swaminathan, 1995] as an umbrella class for efficient SAT solving. Balyo, Gursky, Cepek, Kucera, Vlcek in 2012 extended this class in various ways to hierarchies covering all of CNF (all clause-sets). W...
| Published in: | SOFSEM 2013: Theory and Practice of Computer Science. LCNS |
|---|---|
| ISSN: | 0302-9743 1611-3349 |
| Published: |
Springer
2013
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa13748 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
The class SLUR (Single Lookahead Unit Resolution) was introduced in [Schlipf, Annexstein, Franco, Swaminathan, 1995] as an umbrella class for efficient SAT solving. Balyo, Gursky, Cepek, Kucera, Vlcek in 2012 extended this class in various ways to hierarchies covering all of CNF (all clause-sets). We introduce a hierarchy SLUR_k which we argue is the natural “limit” of such approaches. The second source for our investigations is the class UC of unit-refutation complete clause-sets introduced in [del Val 1994]. Via the theory of (tree-resolution based) “hardness” of clause-sets as developed in ECCC-report, Annals-paper and [Ansotegui, Bonet, Levy, Manya, 2008], we obtain a natural generalisation UC_k, containing those clause-sets which are “unit-refutation complete of level k”, which is the same as having hardness at most k. Utilising the strong connections to (tree-)resolution complexity and (nested) input resolution, we develop fundamental methods for the determination of hardness (the level k in UCk ). A fundamental insight now is that SLUR_k = UC_k holds for all k. We can thus exploit both streams of intuitions and methods for the investigations of these hierarchies. |
|---|---|
| Keywords: |
algorithms, satisfiability, polynomial time, knowledge compilation |
| College: |
Faculty of Science and Engineering |
| Start Page: |
220 |
| End Page: |
232 |