An efficient algorithm for reducing clauses based on constraint satisfaction techniques

This paper presents a new reduction algorithm which employs Constraint Satisfaction Techniques for removing redundant literals of a clause efficiently. Inductive Logic Programming (ILP) learning algorithms using a generate and test approach produce hypotheses with redundant literals. Since the reduction is known to be a co-NP-complete problem, most algorithms are incomplete approximations. A complete algorithm proposed by Gottlob and Fermüller is optimal in the number of θ-subsumption calls. However, this method is inefficient since it exploits neither the result of the θ-subsumption nor the intermediary results of similar θ-subsumption calls. Recently, Hirata has shown that this problem is equivalent to finding a minimal solution to a θ-subsumption of a clause with itself, and proposed an incomplete algorithm based on a θ-subsumption algorithm of Scheffer. This algorithm has a large memory consumption and performs many unnecessary tests in most cases. In this work, we overcome this problem by transforming the θ-subsumption problem in a Constraint Satisfaction Problem, then we use an exhaustive search algorithm in order to find a minimal solution. The experiments with artificial and real data sets show that our algorithm outperforms the algorithm of Gottlob and Fermüller by several orders of magnitude, particularly in hard cases.