Several authors have proposed increasingly e cient methods for computing the least general generalization of two clauses under theta-subsumption. The most expensive step in this computation is the reduction of the clause to its minimal size. In general, this requires testing all literals for redundancy, which in the worst case requires a thetasubsumption test for each of them. In this paper, we present a small result that is complementary to earlier published results. It basically extends the conditions under which a literal can be decided non-redundant without running a theta-subsumption test. Preliminary experiments show a speedup factor of about 3 on one dataset when this new result is used.
Several ILP systems rely on computing the least general generalization (lgg) of two clauses under theta-subsumption. This computation consists of two steps. In the rst step, a clause is constructed that contains all pairwise lgg's of literals from the rst and second clause. This clause may contain many redundant literals, therefore, in the second step, which is called reduction, all redundant literals are removed from this clause. Checking whether a literal is redundant boils down to a theta-subsumption test in the worst case. Therefore, while the rst step has polynomial complexity (O(mn), with m and n the number of literals in the rst and second clause, respectively), the second step is NP-hard (O(nm)). Unsurprisingly, attempts to make the computation of the lgg more e cient focus on reducing the number of theta-subsumption tests needed (in addition to using an e cient theta-subsumption test, which is a separate problem).
In this paper, we present a result that, while simple, does not seem to have made it into the literature. We show that exploiting this result can substantially reduce the number of theta-subsumption tests needed during the reduction.
We assume familiarity with standard terminology from logic programming, and with the Prolog programming language. 2.1
De nition 1 (theta-subsumption). A clause c theta-subsumes another clause d, denoted c d, if and only if there exists a variable substitution such that c d.
De nition 2 (lgg). The least general generalization under theta-subsumption (brie y, lgg) of two clauses c and d is e if and only if e c, e d, and there does not exist a clause e0 6= e such that e e0, e0 c and e0 d. Theta-subsumption is a semi-order; it is re exive and transitive but not antisymmetric. Di erent clauses may subsume each other; they are called variants of each other.
De nition 3 (variants). Two clauses c and d are variants, denoted c c d and d c. d, if
De nition 4 (redundant literals). A literal l in a clause c is redundant if and only if c n flg c.
Let jcj denote the number of literals in c.
De nition 5 (reduced clauses). A clause c is reduced if there is no c0 such that jc0j < jcj. c
In other words, a clause is reduced if there is no shorter clause equivalent to it. Reducing a clause c means computing its shortest variant. 2.2
The lgg of two clauses can be computed using an algorithm proposed by Plotkin
[
Gottlob and Fermuller (1993) proposed the following algorithm for reduction of clauses: for each literal l in the original clause c: if c c n flg then remove l from c
This algorithm takes jcj calls to theta-subsumption. As indicated by Gottlob and Fermuller, this number can be reduced, by skipping those literals for which it is obvious that they cannot be removed. More generally, to reduce a clause more e ciently, the following scheme can be used:
3. for the remaining literals, determine redundancy by means of a subsumption test
Gottlob and Fermuller point out that the test c c n flg can only succeed if there exist a such that l 2 c n flg, in other words, there must be another literal l0 2 c, besides l, such that l = l0. A literal l that has no matching literal l0 is certainly non-redundant.
Malobert and Suzuki point out that, when c c n flg, all literals in c n flg n c can be concluded to be redundant, not just l. They provide a method for computing the that minimizes jc j, thus identifying a maximum number of redundant literals using one complete subsumption test (a complete subsumption test is one that returns f jc dg rather than just a boolean that indicates the non-emptiness of this set).
The main contribution of this paper is that we generalize the conditions under which literals can easily be identi ed as non-redundant, thus increasing the impact of (1). 3
E
ciently identifying non-redundant literals We now generalize the conditions under which a literal l can safely be assumed non-redundant.
De nition 6. Given a clause c, a literal l0 2 c matches a literal l 2 c if 9 : l = l0.
De nition 7. A literal l in a clause c is called unique if and only if there is no literal l0 2 c n flg that matches l.
function ReduceUP(clause C):
U := ; repeat for all l 2 C: if there is no l0 in C [ U n flg that matches l then remove l from C, add l to U skolemize U until C does not change anymore for all l 2 C: if U [ C U [ C n flg then remove l from C deskolemize U [ C return U [ C
The for-all loop in this algorithm moves all unique literals from C to U . Literals in U are certainly non-redundant and need not be tested afterwards.
After this for-all loop comes a skolemization step. Skolemization instantiates each variable in U with a di erent and new constant (that is, one that does not yet occur in U [ C). Note that U and C share variables; if a variable in U is instantiated, its occurrences in C are too. This may introduce new unique constants in C, and therefore, a literal that had a matching literal earlier on may no longer have one now. A new check for non-matched literals is then run. More literals may be added to U as a result; more variables will be instantiated in the new skolemization step, and so on, until C no longer changes. At that point, the literals in C are tested for redundancy using theta-subsumption. Example 1. Consider C = fp(a; Y ); p(Y; b); p(X; b); p(X; Z)g.
In the rst run, p(a; Y ) is the only literal that does not match any other literals. Therefore, after one execution of the outer loop, U = fp(a; Y )g and C = fp(Y; b); p(X; b); p(X; Z)g. We now skolemize U , which results in U = fp(a; y)g and C = fp(y; b); p(X; y); p(X; Z)g (where y is the constant that variable Y was instantiated to). At this point, p(y; b) no longer matches any other literal and therefore joins U , giving U = fp(a; y); p(y; b)g and C = fp(X; b); p(X; Z)g. At this point U contains no variables, therefore skolemization does not change anything and C will not change. The algorithm will now only test the literals in C for redundancy using theta-subsumption. Both literals in C turn out to be redundant (by = fX=y; Z=bg), yielding as nal result U = fp(a; y); p(y; b)g and C = ;, and after deskolemization, returning fp(a; Y ); p(Y; b)g as the reduced clause.
It is intuitively clear that this procedure is sound: if a literal l in C becomes unique through the skolemization (while it wasn't before), this is because it shared a variable with a literal u in U . Hence, any substitution that could be used to make l equal to another literal l0 (which is necessary to have (U [ C) U [ C n flg) would have an e ect on u as well, and would map u to a literal outside U [ C (since no substitution exists that maps u to a literal in U [ C, by de nition of uniqueness of u).
The nal subsumption tests in our algorithm are performed using the partially skolemized clause. Indeed, it makes no di erence whether these tests are run on the deskolemized or partially skolemized clause: by de nition of uniqueness, we know that the literals in u cannot map onto any other literal than themselves, therefore the variables in them cannot occur in any substitution except one that assigns them to themselves, therefore replacing these variables by constants does not make a di erence for the outcome of the test. The subsumption test may be faster when performed on the partially skolemized clause, though, simply because this clause contains fewer variables (and the number of variables a ects the e ciency of theta-subsumption). 4
The algorithm presented above causes a kind of \propagation of uniqueness" (hence its name, ReduceUP). While it trivial that a literal with a unique predicate symbol or a unique constant must be unique (hence, non-redundant), the skolemization of unique literals can cause their neighbors (that is, the literals that share a variable with them) to become unique too. This may substantially increase the number of literals considered unique and therefore trivially nonredundant.
The above result is complementary to existing results on lgg computation.
Both the procedure proposed by Gottlob and Fermuller [
We performed preliminary experiments on a dataset used by Becerra-Bonache
et al. [
Our lgg implementation uses another, more trivial, optimization: literals that do not share any variables with other literals and subsume a unique literal are automatically removed (indeed, as they do not share variables with any other literals, their matching substitution cannot be incompatible with substitutions for other literals). This further reduces the number of remaining literals that needs to be tested by subsumption. With an overall CPU time of 7.1s for processing 100 examples, the version with uniqueness propagation is over 3 times faster than the one with standard uniqueness (25.0 seconds). This factor 3 is higher than the reduction of the number of subsumption tests, but as said before, the tests themselves tend to become more e cient too. 6
The computation of the lgg of two clauses contains a reduction step, which itself is NP-hard and generally has to rely on multiple theta-subsumption tests. The fewer such tests are needed, the more e cient the lgg computation becomes. \Unique" literals, which have no other literals that match it, can trivially be excluded from such testing. In this paper, we have showed that the concept of uniqueness can be broadened, so that more literals ful ll the criterion, and that this can lead to faster computation of the lgg.
This work is preliminary. A more extensive experimental comparison of lgg computation methods would be useful; this comparison should be done on a wider range of datasets, and should assess not only the e ect of uniqueness propagation in a simple implementation of lgg, but also when combined with a more advanced version such as Maloberti and Suzuki's Jivaro.