Hierarchies of polynomially solvable satisfiability problems

In this paper, we introduce general techniques for extending classes of polynomially solvable SAT instances. We generalize the approach of Gallo and Scutellà, who defined the hierarchy { _i }, where _l corresponds to the Generalized Horn class. We propose a family of polynomial hierarchies, where a polynomial hierarchy { _i } is a sequence of polynomially solvable classes that cover the whole set of CNF formulas, and such that _{i i+1} fori0. Following a different approach, based on a new decomposition technique, we define the class of Split-Horn formulas, which is an extension of _l. We discuss and compare the basic properties of the proposed classes; polynomial time algorithms for recognition and solution are provided.