The class SLUR (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 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 [10]. Via the theory of (tree-resolution based) "hardness" of clause-sets as developed in [19,20,1] 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 UC_k). 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. As an application we can easily show that the hierarchies from [7,2] are strongly subsumed by SLUR_k. We conclude with a discussion of open problems and future directions.
展开▼
