Yamasaki and Doshita (1983) have defined an extension of the class of propositional Horn formulas; later, Gallo and Scutellà (1988) generalized this class to a hierarchy ¦)0⊆¦)1ëëë⊆¦)k⊆ëëë, where ¦)0 is the set of Horn formulas and ¦)1 is the class of Yamasaki and Doshita. For any fixed k, the propositional formulas in ¦)Åk can be recognized in polynomial time and the satisfiability problem for ¦)k formulas can be solved in polynomial time. A possible way of extending these tractable subclasses of the satisfiability problem is to consider renamings: a renaming of a formula is obtained by replacing for some variables all their positive occurrences by negative occurrences and vice versa. The class of renamings of Horn formulas can be recognized in linear time. Chandru et al. (1990) have posed the problem of deciding whether the renamings of ¦)1 formulas can be recognized efficiently. The authors show that this is probably not the case by proving the NP-completeness of recognizing the renamings of ¦)Åk formulas for any k≥1.
