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 Fermiiller is optimal in the number of theta-subsumption calls. However, this method is inefficient since it exploits neither the result of the theta-subsumption nor the intermediary results of similar theta-subsumption calls. Recently, Hirata has shown that this problem is equivalent to finding a minimal solution to a theta-subsumption of a clause with itself, and proposed an incomplete algorithm based on a theta-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 theta-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 Fermiiller by several orders of magnitude, particularly in hard cases.