REMOVING REDUNDANCY FROM A CLAUSE

This paper deals with the problem Of removing redundant literals from a given clause. We first consider condensing, a weak type of redundanc y elimination. A clause is condensed if it does not subsume any proper subset of itself. It is often useful (and sometimes necessary) to rep lace a non-condensed clause C by a condensation, i.e., by a condensed subset of C which is subsumed by C. After studying the complexity of a n existing clause condensing algorithm, we present a more efficient al gorithm and provide arguments for the optimality of the new method. We prove that testing whether a given clause is condensed is co-NP-compl ete and show that several problems related to clause condensing belong to complexity classes that are, probably, slightly harder than NP. We also consider a stronger version of redundancy elimination: a clause C is strongly condensed iff it does not contain any proper subset C' s uch that C logically implies C'. We show that the problem of testing w hether a clause is strongly condensed is undecidable.