On the Complexity of Clause Condensing
This paper deals with complexity issues related to the recognition of redundancy and to the removal of redundant literals from a clause. We first consider condensing, a weak type of redundancy elimination. A clause is condensed iff it does not subsume any proper subset of itself. It is often useful (and sometimes necessary) to replace 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 an existing clause condensing algorithm, we show that the problem of testing whether a given clause is condensed is co-NP-complete. Furthermore, we prove that the problems of identifying clause condensations and of testing whether there exists a condensation of a given cardinality are complete for DP, a complexity class which is likely to properly include both NP and co-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’ such that C implies C’. We show that the problem of testing whether a clause is strongly condensed is undecidable.
Unable to display preview. Download preview PDF.
- L.D. Baxter. The NP-completeness of subsumption. unpublished manuscript, 1977.Google Scholar
- S. Ceri, G. Gottlob, and L. Tanca. What you always wanted to know about datalog (and never dared to ask). IEEE Transactions on Knowledge and Data Engineering, 1(1), March 1989.Google Scholar
- G. Gottlob and A. Leitsch. Fast subsumption algorithms. In Proceedings of the EUROCAL 85 Conference on Computer Algebra, Lecture Notes in Computer Science. Springer Verlag, 1985.Google Scholar
- H. Gallaire and J. Minker, editors. Logic and Databases. Plenum Press, New York, 1978.Google Scholar
- W.H. Joyner. Automatic Theorem Proving and the Decision Problem. PhD thesis, Harvard University, May 1973.Google Scholar
- A. Leitsch. Implication algorithms for classes of Horn clauses, in: Informatik+Oekonomie, Berlin, 1988.Google Scholar
- A. Leitsch and G. Gottlob. Deciding Horn clause implication problems by ordered semantic resolution. In F. Gardin, editor, Computational Intelligence II, Proceedings of the International Symposium, Milan, Italy, 25–27 Sept 1989. North Holland, Amsterdam, 1989.Google Scholar