|
Abstract : |
Yamasaki and Doshita have dened an extension of the class of propositional Horn formulas; later, Gallo and Scutella 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 xed k, the propositional formulas in k can be recognized in polynomial time, and the satisability problem for k formulas can be solved in polynomial time. A possible way of extending these tractable subclasses of the satisability 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. have posed the problem of deciding whether the renamings of 1 formulas can be recognized eciently. 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., |
