RECOGNIZING RENAMABLE GENERALIZED PROPOSITIONAL HORN FORMULAS IS NP-COMPLETE

Yamasaki and Doshita (l983) have defined an extension of the class of propositional Horn formulas; later, Gallo and Scutella (1988) generali zed this class to a hierarchy Gamma(0) subset of or equal to Gamma(1) subset of or equal to ... subset of or equal to Gamma(k) subset of or equal to ..., where Gamma(0) is the set of Horn formulas and Gamma(1) is the class of Yamasaki and Doshita. For any fixed k, the proposition al formulas in Gamma(k) can be recognized in polynomial time, and the satisfiability problem for Gamma(k) formulas can be solved in polynomi al time. A possible way of extending these tractable subclasses of the satisfiability problem is to consider renamings: a renaming of a form ula is obtained by replacing for some variables all their positive occ urrences by negative occurrences and vice versa. The class of renaming s of Horn formulas can be recognized in linear time. Chandru et al (19 90) have posed the problem of deciding whether the renamings of Gamma( 1) formulas can be recognized efficiently. We show that this is probab ly not the case by proving the NP-completeness of recognizing the rena mings of Gamma(k) formulas for any k greater than or equal to 1.