Generalising unit-refutation completeness and SLUR via nested input resolution

Based on the theory of hardness hd(F) for clause-sets F, we develop a systematic approach towards classes interesting for the area of knowledge compilation for the clausal entailment problem, as well as towards providing soft ("good") target classes for SAT translation. The notion of hardness was introduced in [Kullmann 1999, 2004]. We now consider a variation, first mentioned in [Ansotegui, Bonet, Levy, Manya, 2008], which differs on satisfiable clause-sets. The class of unit-refutation complete clause-sets was introduced in [del Val, 1994], denoted here by UC_1. It turns out to be exactly the class of clause-sets of hardness at most 1. Thus we obtain a natural generalisation UC_k of classes of clause-sets which are "unit-refutation complete of level k". Utilising the strong connections to (tree-)resolution complexity and (nested) input resolution, we develop fundamental methods for determination of hardness (the level k in UC_k). UC_1 also turns out to be precisely the class SLUR (Single Lookahead Unit Resolution) introduced in [Schlipf, Annexstein, Franco, Swaminathan, 1995]. A natural hierarchy SLUR_k based on SLUR is derived, and we show SLUR_k = UC_k for all k >= 0, offering an alternative interpretation of UC_k. Furthermore we show that the hierarchies introduced in [Cepek, Kucera, Vlcek, 2012; Balyo, Gursky, Kucera, Vlcek, 2012], based on SLUR, are strongly subsumed by SLUR_k. Finally we consider the problem of "irredundant" clause-sets in UC_k. For 2-CNF we show that strong minimisations are possible in polynomial time, while already for (very special) Horn clause-sets minimisation is NP-complete. We conclude with a discussion of open problems and future directions.