Recognizing renamable generalized propositional Horn formulas is NP-complete Original Research Article

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 Γo ⊂- Γ1 ⊂- … ⊂- Γk ⊂- …, where Γo 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. We show that this is probably not the case by proving the NP-completeness of recognizing the renamings of Γk formulas for any k ⩾ 1.