AN ALGORITHM OF REMOVING REDUNDANCY FROM CLAUSE AND ITS COMPLEXITY

This paper deals with the problem of removing redundancy from a given clause, and discusses the case of redundant literals elimination in a clause. Condensing is one important type of redundancy elimination. We first consider the decidability and complexity of this problem, and then gives a polynomial algorithm of its sub-problem.