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 Scutella, who defined the hierarchy {Gamma(i)}, where Gamma(1) corresponds to the Generalized Horn class. We propose a family of polynomial hierarchies, where a polynomial hierarchy {Pi(i)} is a sequence of polynomially solvable classes that cover the whole set of CNF formulas, and such that Pi(i) subset of Pi(i+1) for i greater than or equal to 0. Following a different approach, based on a new decomposition technique, we define the class of Split-Horn formulas, which is an extension of Gamma(1). We discuss and compare the basic properties of the proposed classes; polynomial time algorithms for recognition and solution are provided.