Generalising and unifying SLUR and unit-refutation completeness

Abstract

The class (Single Lookahead Unit Resolution) was introduced in [22] as an umbrella class for efficient SAT solving.[7,2] extended this class in various ways to hierarchies covering all of CNF (all clause-sets). We introduce a hierarchy which we argue is the natural "limit" of such approaches. The second source for our investigations is the class of unit-refutation complete clause-sets introduced in [10]. Via the theory of (tree-resolution based) "hardness" of clause-sets as developed in [19,20,1] we obtain a natural generalisation, 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). A fundamental insight now is that holds for all k. We can thus exploit both streams of intuitions and methods for the investigations of these hierarchies. As an application we can easily show that the hierarchies from [7,2] are strongly subsumed by. We conclude with a discussion of open problems and future directions. © 2013 Springer-Verlag Berlin Heidelberg.