We present a reasoning architecture for deciding subsumption for the description logic E LQ. Our architecture combines saturation rules with algebraic reasoning based on Integer Linear Programming (ILP). Deciding the so-called numerical satis ability of a set of quali ed cardinality restrictions is reduced to constructing a corresponding system of linear inequalities and applying ILP methods in order to determine whether this system is feasible. Our preliminary experiments indicate that this calculus o ers a better scalability for quali ed cardinality restrictions than approaches combining both tableaux and ILP as well as traditional (hyper)tableau methods.
order to represent the QCRs as inequalities we create P xCi 2, P xDj 2, P xDk 2, and P xEl 2. For instance, the variables xCi represent the cardinalities of all elements in the power set of P that contain C; R. The same holds for the other variables respectively. As an additional constraint we specify that all variables must be greater or equal to zero. Our objective function minimizes the sum of all variables. Intuitively speaking, the above-mentioned concept conjunction is feasible and in this trivial case also satis able if the given system of inequalities has an integer solution. It is easy to see that the size of such an inequality system is exponential to m. Furthermore, in order to ensure completeness, we required a so-called choose rule that implements a semantic split that nondeterministically adds for each variable x either the inequality x 0 or x 1. Unfortunately, this uninformed choose rule could re 22m times in the worst case and cause a severe performance degradation.
(ii) The employed ILP algorithms were best-case exponential in the number of occurring QCRs due to the explicit representation of 2m variables. In [FH10a, FH10b] we developed an optimization technique called lazy partitioning that tries to delay the creation of ILP variables but it cannot avoid the creation of 2m variables in case m QCRs are part of a concept model. Our experiments in [FH10a, FH10b, FH10c] indicated that quite a few ILP solutions can cause clashes due to lack of knowledge about known subsumptions, disjointness, and unsatis ability of concept conjunctions. This knowledge can help reducing the number of variables and eliminating ILP solutions that would fail logically. For instance, an ILP solution for the example presented in the previous paragraph might require the creation of an R-successor as an instance of C u D u :E. However, if C and D are disjoint this ILP solution will cause a clash (and fail logically).
Characteristic (i) can be avoided by eliminating the choose rule for variables. This does not sacri ce completeness because the algorithms implementing our ILP component are complete (and certainly sound) for deciding (in)feasibility. In case a system is feasible (or numerically satis able), dedicated saturation rules determine whether the returned solutions are logically satis able. In case of logical unsatis ability a corresponding unsatis able concept conjunction is added to the input of the ILP component and therefore monotonically constrains the remaining feasibility space. Consequently, previously computed solutions that result in unsatis ability are eliminated. For instance, the example above would be deemed as infeasible once the ILP component learns that C and D are subsumed by E and that C and D are disjoint.
The avoidance of characteristic (ii) is motivated by the observation that only a small number of the 2m variables will have non-zero values in the optimal solution of the linear relaxation, i.e., no more variables than the number of constraints following the characteristics of the optimal solution of a linear program, see, e.g., [Chv83]. As a consequence, only a limited number of variables have a nonzero value in the integer optimal solution. In addition, linear programming techniques such as column generation [DW60, GG61] can operate with as few variables as the set of so-called basic variables in linear programming techniques at each iteration, i.e., nonbasic variables can be eliminated and are not required for the guarantee of reaching the conclusion that a system of linear inequalities is infeasible, or for reaching an optimal LP solution. Although the required number of iterations varies from one case to another, it is usually extremely limited in practice, in the order of few times the number of constraints. The e ciency of the branch-and-price approach, which is required in order to derive an ILP solution, see, e.g., [BJN+98, Van11, LD05], depends on the quality of the integrality gap (i.e., how far the optimal linear programming solution is from the optimal ILP solution in case the system of inequalities is feasible, and on the level of infeasibility otherwise). Several studies have been devoted to improving the convergence of column generation algorithms, especially when degeneracy occurs (see, e.g., [DGL14]) or when convergence is too slow (see, e.g., [ADF09]), and to accelerating the convergence of branch-and-price algorithms [DDS11]. Furthermore, our ILP component considers known subsumptions, disjointness, and unsatis ability of concept conjunctions and uses a di erent encoding of inequalities that already incorporates the semantics of universal restrictions. We delegate the generation of inequalities completely to the ILP component.
To summarize, the novel features of our architecture are (i) saturation rules that do not backtrack to decide subsumption (and disjointness); (ii) feasibility of QCRs is decided by ILP (in contrast to [BMC+16]); (iii) our revised encoding of inequalities and the aggregation of information about subsumption, disjointness, and unsatis ability of concept conjunctions allows a more informed mapping of QCR satis ability to feasibility and reduces the number of returned solutions that fail logically; (iv) the best-case time complexity of our ILP feasibility test is polynomial to the number of inequalities [Meg87]. In the following sections we present our saturation rules, introduce our ILP approach, sketch soundness, completeness, and termination, present our preliminary evaluation results, and conclude with a summary and future work. The DL E LQ allows the concept-forming constructors u (conjunction), (at-most restriction), and (at-least restriction). The semantics of E LQ concepts and roles is de ned by an interpretation I = ( I ; I ) that maps a concept A 2 NC (NC is a set of concept names) to AI I and a role R 2 NR (NR is a set of roles) to RI I I . We assume the prede ned concepts > and ? with >I = I and ?I = ;. E LQ concepts are inductively de ned from the sets NC and NR using the constructors as follows (n; m 2 N; n 1, k k denotes set cardinality, F R;C (x) = fy 2 CI j (x; y) 2 RI g): (i) (C u D)I = CI \ DI ; (ii) ( n R:C)I = fx j kF C;R(x)k ng; (iii) ( m R:C)I = fx j kF C;R(x)k mg. The latter two constructors are called QCRs. A concept C is satis able if there exists an I such that CI 6= ;.
An E LQ Tbox T is de ned as a nite set of axioms of the form C v D and such an axiom is satis ed by I if CI DI . We call I a model of T if it satis es all axioms in T . We use CTA to denote the set that contains > tahnediranllecgoantcioenp)t unsaemdeisnuTse,dainndTd,eCnT:eA C=T f=:ACTAjA[2CCT:ATA [n fC>TQg. gW,CeTQusteo RdTenototedtehneotseetththeastectoonftaroinlessaullseQdCiRnsT(.and
A Tbox T is normalized if all axioms are of the form A1 v B, A1 v ./ n R:A2, ./ n R:A1 v B, A1 u A2 v B, with B 2 CTA [ f?g, A1; A2 2 CTA , and ./ 2 f ; g. It is easy to see that this can be done in polynomial time following the normalizations described in [BBL05, Kaz09, SMH14]. A normalized Tbox is always in negation normal form because it does not allow the occurrence of negation. Some of our saturation rules make use of the negation operator :_ which returns the negation normal form for named concepts and QCRs de ned as :_(C) = :C, :_(:C) = C, :_( m R:C) = m+1 R:C, and :_( n R:C) = n 1 R:C for m 0, n 1.
We adopted the idea of saturation graphs from [BBL05, SGL14]. Our saturation graphs have been extended to deal with E LQ and delegate numerical reasoning on QCRs to an ILP component.
A saturation graph G = (V; E; L; LP ; L: ) is a directed graph where V = VP [ VA [ VC such that VP ; VA; VC are
P pairwise disjoint. VP = fvA j A 2 CTA g is the set of prede ned nodes, VA = fvS j S CTA g the set of anonymous nodes representing role successors, and VC is the set of nodes called QCR clones representing subsumption or disjointness tests based on QCRs. Each node vS 2 V uniquely represents either an element (S 2 L(vS )) of CTA or a subset (S L(vS )) of CTA [ CT:A. We also call S the initial label of vS . Each v 2 V is labelled with a set of concepts L CT [ f?g and sets of subsumption tuples LP ; LP: fhp; qi j p CTA ; q CTQ g. Each edge hv; v0i 2 E is labelled with a set L(v; v0) RT where v0 is called an r-successor (R-successor) of v with r L(v; v0) (R 2 L(v; v0)).
Given a normalized Tbox T and a corresponding saturation graph G the label set LP (LP: ) contains tuples specifying subsumption (disjointness) conditions caused by QCRs. A subsumption tuple of the form hp; qi consists of a set of precondition concepts p CTA and a set of QCRs q CTQ . Some of the rules that operate on LP and LP: make use of special (negated) membership (2, is new), subset ( ), union ([) operators, and a map (') operator. We de ne is new(q; S) = hf>g; fqgi 2= S and add to(Q; S) as S S [ fhf>g; fQgig if Q is a QCR or S S [ Q if Q is a set of subsumption tuples.
Given sets T; T 0 of subsumption tuples, hp; qi 2 T is true if there are p0; q0 such that hp0; q0i 2 T , p p0, and q q0; T T 0 is true if 8t 2 T ) t 2 T 0 holds. fhp1; s1ig [ fhp2; s2ig is de ned as fhp2; s1 [ s2ig if p1 p2 and fhp1; s1i; hp2; s2ig otherwise. The map operator is de ned as '(A; T ) = fhp [ fAg; qi j hp; qi 2 T g with A 2 CA . T
Our saturation rules interface the ILP component via the predicate infeasible(S) which transforms all QCRs in S to a corresponding system of inequalities and returns true if this system is infeasible. Otherwise it returns false. If S contains no QCRs it also returns false. A node v is called numerically satis able or feasible, if the set Q L(v) of QCRs is feasible. A concept A is called feasible if its node vA is feasible. The number of possible solutions for a feasible node can be huge1 and quite a few solutions might eventually cause logical unsatis ability. In order to ensure termination and logically constrain the number of possible solutions for a node v as much as possible, the ILP component makes use of concept information derived from a Tbox T and its saturation graph G. For a node v 2 VP [ VA we de ne Qv = fC j ./ n R:C 2 L(v)g [ f:D j 0 R:D 2 L(v)g as the set of QCR quali cations occurring in L(v). The information about concept unsatis ability and subsumption, which is used by the ILP component, is de ned by the set unsat = Sv2VP [VA unsat v, which contains sets of concepts whose conjunction is unsatis able, and the set subsv = Sv2VP [VA subsv, which contains sets of tuples representing entailed subsumption relationships of the form A v B or A1 u A2 v B. unsat v = ffAg j A 2 Qv; ? 2 L(vA)g [ fq j q Qv; ? 2 L(vq); vq 2 VAg [
ffAi; Aj g j :Ai 2 L(vAj ); fAi; Aj g \ Qv 6= ;; i; j 2 1::2; i 6= jg 1In [FH10c, Sec. 4.1.1] it was shown that if a node label contains p (q) QCRs of the form cases/solutions can exist with N = Pip=1 ni.
ni Ri:Ci ( mj Rj0:Cj0 ), then 2qN subsv = fhfA1; A2g; Bi j fA1; A2g Qv; C1 u C2 v D 2 T ; Ci 2 L(vAi ); B 2 L(vD); i 2 1::2g [ fhfAg; Bi j B 2 L(vA); A 2 Qvg
In case a node v is numerically satis able, the set (v) contains solutions for feasible inequality systems denoted by the QCRs in L(v). A QCR solution is described by a set of tuples of the form hr; q; ni with r RT and q CTA [ CT:A sets of roles and concepts respectively, and n denotes the cardinality of the set of r-successors that are instances of all concepts contained in q.
A saturation graph G is initialized with representative nodes for all concepts in CA . For instance, for a concept T A a node vA is created with L(vA) = f>; Ag and LP (vA) = LP: (vA) = ;. The saturation rules are applied to an initialized saturation graph until no rule is applicable anymore. Only the vP4 -Rule and vP:4 -Rule with v 2 VC can be applied to a node v if ? 2 L(v).
This algorithm computes the named subsumers for all prede ned nodes and, thus, decides satis ability and sBub2suLm(pvAti)o.n Tfohre atlolpcosneccteipotns oi nf FCiTAg u.reA1ccoonncteapitnsA vise srautliess.abTlehei v?-Ru2=leL((vvA:-)R,ualned) aAlloiwsssuabsQuCmRedorbynaBmeid concept on its right-hand (left-hand) side. The v -Rule ensures that L(v) contains all QCRs and (negated) named concepts inherited from its subsumers. The vu-Rule is a standard E L rule complemented by its contrapositive version (vu:-Rule). The second section contains two rules that deal with role successors where # denotes the cardinality of an anonymous node. If hr; q; ni 2 (v) the l-rule and e-rule ensure that an edge r L(v; vq) exists that connects v to an anonymous successor vq with L(vq) = q and #vq = n, i.e., vq represents n identical r-successors of v.
For a node v the ?-Rule records clashes by adding ? to L(v). For a node v0 created by the l-rule there is no need to propagate ? to its predecessor v because v0 represents one of possibly many existing QCR solutions for v. If all QCR solutions for v fail, the ILP component eventually determines that v is infeasible and thus unsatis able.
The fourth section of Figure 1 contains ve rules that create and maintain subsumption tuples. Only three of these rules (P./-Rule, P.:/-Rule, Pu-Rule) derive tuples from axioms. The other two rules propagate tuples up (vP -Rule) or down (vP: -Rule) the subsumption hierarchy.
The bottom section of Figure 1 lists rules that discover subsumptions or disjointness due to subsumption tuples. Q(v; S) is de ned as Shp;qi2S fq j p L(v)g and contains applicable QCRs selected from the set S of subsumption tuples. The relation clone V (CTA [ CT:A) V keeps track of subsumption or disjointness tests and their associated QCR clones. For instance, a QCR clone v0 2 VC of vA contains all QCRs contained in L(vA) and LP (vB) (LP: (vB)) and represents the test whether A is subsumed by (disjoint to) B. If v0 becomes unsatis able, then B (:B) is added to L(vA). The vP1 -Rule creates necessary QCR clones, the vP2 -Rule (vP3 Rule) ensures that Q(vA; LP (vB)) (L(vA) \ CTQ ) is contained in L(v0). The vP4 -Rule adds B to L(vA) if vA's corresponding clone is unsatis able. The other four rules deal with disjointness in an analogous way. 3
We demonstrate our calculus with a small ALCQ Tbox T which entails C v D1 u :D2 (see below). A slightly di erent example (C-SAT-exp-ELQ) is also used in our synthetic benchmark (see Section 6) and surprisingly none of the tested reasoners besides Avalanche and Racer can classify the version with n = 10 within a time limit of 1000 seconds.
C v 20 R:> u 10 R:A u 10 R:B C v D1 t D2 D1 v 10 R::A, D2 v 9 R::B The following steps show our rewriting of T into T 0, which is a normalized E LQ Tbox that is a conservative extension of T .
1. We remove the occurrence of t and add the entailment C v D1 t D2 using fresh concepts X3; X4 and a fresh role S1.
C v 20 R:> u 10 R:A u 10 R:B C u 1 S1:(X3 u X4) v D1 o These two axioms entail C v D1 t D2 C u 2 S1:> v D2 D1 v 10 R::A
D2 v 9 R::B 2. We normalize the axioms (but allow a conjunction on the right-hand side for sake of brevity) and replace :A; :B by notA; notB and new axioms using fresh roles S2; S3 such that :notA v A and :notB v B are v-Rule if A v 2 T ; 2= L(vA)
then add to L(vA) v:-Rule if v A 2 T ; :A 2 L(v); :_ 2= L(v)
then add :_ to L(v) v -Rule if A 2 L(v); 2 L(vA); 2= L(v)
then add to L(v) vu-Rule if A1 u A2 v B 2 T ; fA1; A2g L(v); B 2= L(v)
then add B to L(v) vu:-Rule if Ai u Aj v B 2 T ; f:B; Aig L(v); :Aj 2= L(v)
then add :Aj to L(v) l-Rule if hr; q; ni 2 (v); :9 vq 2 V : q L(vq); #vq n
then create vq 2 VA with L(vq) q and #vq n e-Rule if hr; q; ni 2 (v); q L(vq); #vq n; r * L(v; vq)
then add r to L(v; vq) ?-Rule if ? 2= L(v) ^ (infeasible(L(v)) _ fA; :Ag L(v))
then add ? to L(v) P./-Rule if ./ n R:A v B 2 T ; is new( :_(./ n R:A); LP (vB))
then add to( :_(./ n R:A); LP (vB)) P.:/-Rule if A v ./ n R:B 2 T ; is new(./ n R:B; LP: (vB))
then add to(./ n R:B; LP: (vB)) P -Rule if B 2 L(vA); LP (vA) 6 LP (vB)
then add to(LP (vA); LP (vB)) P :-Rule if B 2 L(vA); LP: (vB) 6 LP: (vA) then add to(LP: (vB); L: (vA))
P Pu-Rule if Ai u Aj v B 2 T ; '(Ai; LP (vAj )) 6 LP (vB)
then add to('(Ai; LP (vAj )); LP (vB)) vP1-Rule if Q(v; LP (vB)) 6= ;; fB; :Bg \ L(v) = ;; clone(v; B) = ;
then create v0 2 VC; L(v0) f>g; clone(v; B) fv0g vP2-Rule if v0 2 clone(v; B); fB; :Bg \ L(v) = ;; Q(v; LP (vB)) * L(v0)
then add to(Q(v; LP (vB)); L(v0)) vP3-Rule if v0 2 clone(v; B); fB; :Bg \ L(v) = ;; L(v) \ CTQ * L(v0) \ CT Q then add to(L(v) \ CQ; L(v0)) vP4-Rule if fB; :Bg \ L(v) = ;; v0 2 clone(v; B); ? 2 L(v0)
then add B to L(v) vP:1-Rule if Q(v; LP: (vB)) 6= ;; fB; :Bg \ L(v) = ;; clone(v; :B) = ;
then create v0 2 VC; L(v0) f>g; clone(v; :B) fv0g vP:2-Rule if v0 2 clone(v; :B); fB; :Bg \ L(v) = ;; Q(v; LP: (vB)) * L(v0)
then add to(Q(v; LP: (vB)); L(v0)) vP:3-Rule if v0 2 clone(v; :B); fB; :Bg \ L(v) = ;; L(v) \ CTQ * L(v0) \ CT Q then add to(L(v) \ CQ; L(v0)) vP4:-Rule if fB; :Bg \ L(v) = ;; v0 2 clone(v; :B); ? 2 L(v0) then add :B to L(v) entailed. This Tbox T 0 additionally entails C v X5 u :X7.
C v 20 R:> u 10 R:A u 10 R:B C u X5 v D1
1 S1:X6 v X5 X3 u X4 v X6 C u X7 v D2
2 S1:> v X7 D1 v 10 R:notA D2 v 9 R:notB 1 S2:> v notA 1 S2:> v A 1 S3:> v notB 1 S3:> v B o These two axioms entail :notA v A o These two axioms entail :notB v B subs = fhfC; X5g; D1i; hfC; X7g; D2i; hfX3; X4g; X6ig unsat = ; 3. Known subsumptions or unsatis ability of concept conjunctions are derived from T 0. 4. After applying the rules v, P./, P.:/, Pu we get the following node labels (for sake of better readability we denote vA, where A is a concept name, simply as A when used for the labels L; LP ; LP: ; anonymous and clone nodes are denoted as vai and vcj respectively).
L(C) = f>; C; 1 S1:X3; 1 S1:X4; 20 R:>; 10 R:A; 10 R:Bg
(C) = fhfRg; f:A; :B; :notB g; 20i; hfS1g; fX3; X4; X6g; 1ig LP: (C) = fhf>g; f 1 S1:X3gi; hf>g; f 1 S1:X4gi; hf>g; f 20 R:>gi; hf>g; f 10 R:Agi; hf>g; f 10 R:Bgig L(D1) = f>; D1; 10 R:notAg LP: (D1) = fhf>g; f 10 R:notAgig LP (D1) = fhf>; Cg; f 0 S1:X6gi L(D2) = f>; D2; 9 R:notB g LP: (D2) = fhf>g; f 9 R:notB gig LP (D2) = fhf>; Cg; f 1 S1:>gi LP (X5) = fhf>g; f 0 S1:X6gig LP (X7) = fhf>g; f 1 S1:>gig LP (notA) = fhf>g; f 2 S2:>gig LP (A) = fhf>g; f 0 S2:>gig LP (notB ) = fhf>g; f 2 S3:>gig
LP (B) = fhf>g; f 0 S3:>gig 5. After applying the rules vP:1 , vP:2 , vP:3 (is C disjoint to D2?) and creating the clone vc1 clone(C; :D2) vc1
L(vc1 ) = f>; 1 S1:X3; 1 S1:X4; 20 R:>; 10 R:A; 10 R:B; 9 R:notB g 6. After applying the l- and e-rule for vc1 and the rules v:, ? for va1
(vc1 ) = fhfRg; f:A; :B; :notB g; 20i; hfS1g; fX3; X4; X6g; 1ig L(vc1 ; va1 ) = fRg L(va1 ) = f>; :A; :B; :notB ; 0 S2:>; 0 S3:>; 2 S3:>; ?g, #va2 = 20 L(vc1 ; va2 ) = fS1g L(va2 ) = f>; X3; X4; X6g, #va2 = 1 Based on the unsatis ability of va1 we add f:A; :B; :notB g to unsat .
L(vc1 ; va4 ) = fRg
L(va4 ) = f>; :A; B; :notB ; 0 S2:>; notA; 2 S3:>g, #va4 = 1 7. After applying the l- and e-rule for vc1 again, the rules v:, ? for va3 (vc1 ) = fhfRg; f:A; :B; notB g; 9i; hfRg; f:A; B; :notB g; 1i; hfRg; fA; :B; :notB g; 10i,
hfS1g; fX3; X4; X6g; 1ig L(vc1 ; va3 ) = fRg L(va3 ) = f>; :A; :B; notB ; 0 S2:>; 0 S3:>g, #va3 = 9 L(vc1 ; va5 ) = fRg L(va5 ) = f>; A; :B; :notB ; 0 S3:>; notB ; ?g, #va2 = 10 Based on the unsatis ability of va5 we add fA; :B; :notB g to unsat . Together with the previous addition to unsat we learned that f:B; :notB g is unsatis able. 8. The ?-rule adds ? to L(vc1 ) because infeasible(L(vc1 )) is true due to f:B; :notB g 2 unsat .
10. The rules vu: and v: add :X7 and
1 S1:> to L(C). 11. After applying the rules vP1 , vP2 , vP3 (is C subsumed by X5?) and creating the clone vc2 clone(C; X5) vc2
L(vc2 ) = f>; 1 S1:X3; 1 S1:X4; 20 R:>; 10 R:A; 10 R:B; 1 S1:>; 0 S1:X6g 12. The ?-rule adds ? to L(vc2 ) because infeasible(L(vc2 )) is true due to role S1. 13. The vP4 -rule adds X5 to L(C). 14. The vu-rule adds D1 to L(C).
Other rules are still applicable but for sake of brevity we do not illustrate their application. Furthermore, no other concept subsumptions are entailed w.r.t. T .
We now present the large-scale optimization framework we have designed for solving the system of QCRs in the DL ELQ. It is based on a decomposition technique, called DantzigWolfe decomposition or more commonly column generation technique [Las70, Chv83], combined with a branch-and-price technique [BJN+98] in order to either detect that the system is infeasible, or to compute an optimal solution of the system.
Given T , v 2 V and S containing QCRs, de ne the qualifying role set of v as SQ = f (./ nR:C) j ./ nR:C 2 Sg [ fC j ./ nR:C 2 Sg [ f>; ?g, where de nes a mapping between a QCR and its associated (proxy) subrole of R that is new in T , e.g., (./ nR:C) = R0 with R0 v R and R0 new in T . The role partitioning PSQ of a qualifying role set SQ is de ned as the power set of SQ (without the empty set). Note that a qualifying concept can be a member of a partition only if the partition also contains at least one role. For each partition p 2 PSQ , we de ne pI = l (v; p) \ ( I n SY 2SQnp l (v; Y )) where l (v; p) = Te2p l (v; e) and l (v; e) = eI if e is a concept and l (v; e) = fyI j (vI ; yI ) 2 eI g if e is a role. The semantics of role partitions in PSQ is de ned in such a way that their interpretations are pairwise disjoint. The absence of a role or concept in a partition implies the presence of its semantic negation. We now de ne a mapping from S to a linear inequality system as follows:
P - ( nR:C) = f q2PSQ jR02q xq
ng with R0 = ( nR:C), - ( nR:D) = fP
R00 = ( nR:D).
q2PSQ jR002q xq ng [ Sq2Qfxq
0g, such that Q = fp 2 PSQ j D 2 p ^ R00 2= pg, with
In order to determine whether (S) = S./nR:C2S (./ nR:C) is feasible using a highly scalable solution, we propose a column generation ILP formulation for expressing (S) as a mathematical ILP model, which will be solved using a branch-and-price algorithm [BJN+98].
Given T , v 2 V , S, SQ and PSQ , the ILP model associated with the feasibility problem of (S) can be written as follows:
min subject to:
p2PSQ
X apR0 xp p2PSQ
X apR0 xp p2PSQ xp 2 Z+ R0
R0 2 SQrole p 2 PSQ ; (1) (2) (3) (4) where SQrole = f ( nR:C) j nR:C 2 Sg, SQrole = f ( nR:C) j nR:C 2 Sg, SQrole = SQrole [ SQrole, R0 ( R0 ) is the cardinality of an at-least (at-most) restriction on a subrole R0 2 SQrole, and xp represents a partition of the set PSQ . costp is de ned as the number of concepts in partition p.
When the set of inequalities has a non empty solution set, we are interested in partitions that only contain the entailed concepts, i.e., the minimum number of concepts that are needed to satisfy all the axioms. Consequently, in the objective, costp ensures that output partitions only contain the entailed concepts, i.e., the minimum number of concepts that are needed to satisfy all the axioms.
In order to design a scalable solution of (1)-(4), which has an exponential number of variables, we consider
a solution scheme that makes use of an implicit representation of the constraint matrix. This corresponds to
using a branch-and-price method, a generalization of a branch-and-bound method [NW88] in which the linear
relaxation of (1)-(4) is solved with a column generation algorithm ([Las70], [Chv83]). The linear relaxation is
de ned by (1)-(3) and constraint (40), which is written as follows:
(40)
(400)
(5)
(6)
(7)
(8)
(9)
(
p 2 PSQ : xp 2 R+ p 2 PS0Q ; Next step is to use an implicit representation of all the variables of (1)-(40). Therefore, instead of de ning the variables for p 2 PSQ , we do it for p 2 PS0Q PSQ , leading to the so-called restricted ILP or restricted master problem in the mathematical programming literature, in which constraints (40) are replaced by constraints with PS0Q = ; at the outset. We next have an iteration solution process in which, at each iteration, the column generation algorithm tries to generate an improving partition p, i.e., a partition such that, if added to the current PS0Q , improves the objective of formulation (1)-(400). The partition generator (PG), also called pricing problem in the mathematical programming literature, is a mathematical ILP model with two sets of decision variables: aR0 = 1 if role R0 is in the generated partition, 0 otherwise ; bC = 1 if concept C 2 SQconcept is in the generated partition, 0 otherwise, where SQconcept containing all the concepts of SQ and no subrole. The (PG) model can be stated as: (PG)
min subject to: aR0 bC aR0 b> bC bC b? = 0
X C2SQconcept bC
X R02SQrole aR0 ^R0
X R02SQrole
aR0 !^R0 R0 2 SQrole; C = R0:qualif ier R0 2 SQrole; C = R0:qualif ier
bC ; aR0 2 f0; 1g
R0 2 SQrole; C 2 SQconcept = SQ n SQrole;
where ^R0 and !^R0 are the optimal values of the dual variables of problem (1)-(400) (see [Chv83] if not familiar
with linear programming concepts). The objective function (5) is the so-called reduced cost of a partition (or
column, see again [Chv83] for more details on the column generation method). Constraints (6)-(
(PG) returns a valid partition of PSQ , assuming no other information is provided. In its feasibility space, it contains a 1-to-1 mapping between the said partitions and algebraic inequalities. If other informations such as: (i) subsumption (T j= A v B), (ii) binary subsumption (A u B v C) and (iii) disjointness (T j= A1 u u An v ?; n 1) are provided, the cardinality of some partitions p 2 PSQ might need to be 0. Depending on the information received, the semantics can be implemented by (in)equalities, using a 1-to-1 mapping presented below.
- For every T j= A v B, set SQconcept = SQconcept [ fA; Bg and add bA bB to (PG), in order to guarantee that if a generated partition contains a certain concept, it does contain all its subsumers. - For every T j= A u B v C, update SQconcept = SQconcept [ fA; B; Cg and add bA + bB
Then, if (PG) generates a partition containing A and B, it must contain C as well. 1 bC to (PG). - For every disjointness relation T j= A1 u u An v ?; n 1, set SQconcept = SQconcept [ fA1; : : : ; Ang and add Pin=1 bAi n + 1 b? to (PG). This inequality ensures that if all the concepts Ai, i = 1; : : : ; n are present in a partition; this partition cannot be generated since otherwise it would contain ? as well. - If there is some concept C with :C 2 SQconcept, the relationship of C and :C can be modelled with equality bC + b:C = 1. This implies that every generated partition contains exactly one of C and :C.
Every partition generated by (PG), which possibly contains some of the above inequalities or equalities, satis es all the input axioms except the QCRs, which are taken care of in (1)-(400). The column generation method is an iterative process in which (1)-(400) and (PG) are alternatively solved until (PG) cannot provide any new improving partitions, i.e., when the optimal value of the objective of (PG) is positive. This corresponds to one of the optimality conditions when solving a linear program, see, e.g., [Chv83] for more details.
In the branch-and-price algorithm, an implicit enumeration scheme with a breadth rst search (BFS) exploration strategy, branching is done upon a subrole R0 selected as follows:
R0 = arg max
R02SQrole 8 < X :p2P0 aR0 p max fx^p bx^pc; dx^pe
(11) x^pg 9 = ; ; leading to two branches, one with aR0 = 0 and the other one with aR0 = 1. This branching scheme is clearly exhaustive and valid (see [Van11] and [NW88]). The branch-and-price algorithm terminates when either an integer feasible solution for (1)-(4) is found, or an infeasibility is detected, i.e., either the linear programming relaxation (1)-(400) has no solution (in most of the infeasibility cases) or the branch-and-price algorithm fails to nd a feasible integer solution, see [NW99]. A owchart is provided in Figure 2 to summarize the solution process.
Soundness and Completeness The mapping presented in the previous paragraphs is a one-to-one mapping between the axioms and the algebraic inequalities. Thus, the feasibility space de ned by (2)-(4) represents all the instances that satisfy all axioms. Following the decomposition ILP model that is proposed, constraints related to satisfying QCRs are addressed in (2)-(4), while all other axioms are embedded in (PG). The branch-and-price algorithm, if (1)-(4) is feasible, returns one set of valid partitions, and the selection of them is made by the objective (1).
The result of the proposed solution process is sound. Indeed, every model produced by the large-scale optimization framework, i.e., ILP model (1)-(4) and branch-and-price algorithm, satis es all the axioms that are fed to the ILP component. It is also complete, because the feasibility spaces of the (1)-(400) and (PG) consider all the possible models through the one-to-one mapping that leads to ILP model (1)-(4). In addition, the branching rule in the branch-and-price algorithm considers a partitioning of the overall solution space, therefore no solution is left out. 5 Due to lack of space we can only sketch the soundness and completeness proofs for our saturation rules. Given the presentation in the previous section we know that the algorithms implementing the ILP component are sound and complete and terminate in nite time for deciding whether a set of QCRs is feasible, i.e., numerically satis able.
Intuitively speaking our soundness proof is an extension of the one for E L but all subsumptions or disjointness involving QCRs are based on QCR infeasibility tests performed by the ILP component. Once a subsumption or disjointness has been proven, its evidence as an element of a node label becomes part of the saturation graph. Since QCRs can interact with one another a QCR solution and its corresponding model is not proof enough for a subsumption unless it is known to be the only possible solution. In order to test QCR-based entailment the label sets LP and LP: of potential (non-)subsumer nodes together with node labels are used for a feasibility test. If such a set of QCRs has been proven to be infeasible, the corresponding subsumption or disjointness can be added to the graph. Thus, only entailed subsumptions or disjointness will be inferred.
Lemma (Soundness). Let G be the saturation graph for a normalized Tbox T after the application of all saturhaotlidosnthrautles i2n LF(ivgCur)e. 1 has terminated and C 2 CTA and D 2 CTA [ f?g; 2 fD; :_Dg. Then T j= C v if it Proof. Let us assume that each rule application creates a new saturation graph and the sequence of rule applications until termination produce a sequence of graphs G1; : : : ; Gm with Gi = (Vi; Ei; Li; LP iLP: i) and i 2 1::m. Let F R;C (x) = fy 2 CI j (x; y) 2 RI g, and Q(v; S) = Shp;qi2S fq j p L(v)g. For all m 2 N, models I of T , r RT , and x 2 CI we claim the following holds: (i) if 2 Lm(vC ) then T j= C v ; (ii) if r Lm(vC ; vq); #vq n then there exist yi 2 I with (x; yi) 2 TR2r RI ; yi 2 Tq02q q0I ; i 2 1::n.
We prove our claim by induction on m. We start with m = 0 and assume that I is a model for T . For G0 we have L0(vC ) = f>; Cg; L0(vC ; vD) = ; implying that D = C. It is trivial to see that our claim holds. For the induction step we make a case distinction according to applicable rules. v-Rule Let 2 Lm(vC ) n Lm 1(vC ) and x 2 CI . Then there exists C 2 Lm 1(vC ) and C v model of T it holds x 2 I .
v C 2 T . v:-Rule Let :_ 2 Lm(v) n Lm 1(v) and x 2
Since I a model of T it holds x 2 I n I . v -Rule Let 2 Lm(v) n Lm 1(v) and x 2 CI . Then there exists of T it holds x 2 I . 2 Lm 1(vC ) and CI
holds that x 2 ?I . vu-Rule Let D 2 Lm(v) n Lm 1(v) and x 2 C1I ; x 2 C2I . Then there exists C1; C2 2 Lm 1(v) and C1 u C2 v
D 2 T . Since I a model of T it holds x 2 C1I \ C2I and thus x 2 DI . vu:-Rule Let :Cj 2 Lm(v) n Lm 1(v) and x 2 I n DI ; x 2 CiI . Then there exists :D; Ci 2 Lm 1(v) and
Ci u Cj v D 2 T . Since I a model of T it holds x 2 CiI [ ( I n CjI ) [ ( I n DI ) and thus x 2 I n CjI . l-Rule, e-Rule Let vq 2 Vm n Vm 1, r Lm(vC ; vq) such that q Lm(vq) and #vq n, Q = Lm 1(vC ) \ CTQ , and let x 2 Tq02Q q0I . Due to the soundness and completeness of the ILP component and since I is a model of T , w.l.o.g. we can assume that that a solution hr; q; ni 2 (vC ) exists and we have yi with (x; yi) 2 TR2r RI ; yi 2 Tq02q q0I with i 2 1::n, and it holds 8q0 2 Q : x 2 q0I . ?-Rule Let ? 2 Lm(vC ) n Lm 1(vC ), then either fA; :Ag Lm 1(vC ) and x 2 AI ; x 2 I n AI or infeasible(Lm 1(vC )) and by the soundness of the ILP component x 2 Tq2Lm 1(vC)\CQT qI . In both cases it P./-Rule Let hf>g; f :_(./ n R:C)gi 2 LP m(vD) n LP m 1(vD). The newly created tuple is correct. Assume for a node vF that ./ m R:E 2 Lm 1(vF ) and x 2 F I . If the ILP component determines f./ m R:E; :_(./ n R:C)g as infeasible, then it holds x 2 (./ m R:E)I , (./ m R:E)I (./ n R:C)I DI because I is a model of T and ./ n R:C v D 2 T .
P.:/-Rule Let hf>g; f./ n R:Cgi 2 LP m(vD) n LP m 1(vD). The newly created tuple is correct. Assume for a node vF it holds ./ m R:E 2 Lm 1(vF ) and x 2 F I . If the ILP component determines the set f./ m R:E; ./ n R:Cg as infeasible, then x 2 (./ m R:E)I , ./ m R:EI I n (./ n R:C)I I n DI because I is a model of T and D v ./ n R:C 2 T .
P -Rule Let hp; qi 2 LP m(vD) n LP m 1(vD), CI DI , and w.l.o.g. let hp; qi 2 LP m 1(vC ). The newly created tuple is correct because I is a model of T and a subsumption condition for C is also one for D since x 2 CI implies x 2 DI .
P :-Rule Let hp; qi 2 LP: m(vC ) n LP: m 1(vC ), CI DI , and w.l.o.g. let hp; qi 2 LP m 1(vD). The newly created tuple is correct because I is a model of T and a subsumption condition for :D is also one for :C since x 2 I n DI implies x 2 I n CI .
Pu-Rule Let hp [ fCig; qi 2 LP m(vD) n LP m 1(vD), and w.l.o.g. let hp; qi 2 LP m 1(vCj ). The newly created tuple is correct because I is a model of T , Ci u Cj v D 2 T , and if CiI DI then a subsumption condition for Cj is also one for D.
Rules vP1 ; vP2 ; vP3 ; vP4 Let ? 2 Lm(v0) n Lm 1(v0), v0 2 clone(vC ; D), x 2 CI . The rule vP1 added v0 to Vk1 , the rules vP2 ; vP3 red at least once and added the corresponding QCRs to Lk2 (v0) with k1 < k2 m 1. We de ne QIP (v) = I n Tq2Q(v;LPm (vD)) qI as the domain complement of all QCRs contained in Q(v; LPm (vD)) and QI (v) = Tq2Lm(v)\ CQ qI as the domain of all QCRs contained in Lm(v). W.l.o.g. we only consider the case that infeasible(L(v0))T caused the unsatis ability of v0. Due to the composition of Lm(v0) and since I is a model of T , it holds x 2 QI (vC ), QI (vC ) QIP (vC ) DI .
The rules vP:1 ; vP:2 ; vP:3 ; vP:4 are analogous to vP1 ; vP2 ; vP3 ; vP4 and for lack of space we omit this part of the soundness proof here.
Lemma (Completeness). Let G be the saturation graph for a normalized Tbox T after the application of all sa2turLa(tvioAn), riuflTes j=inAFvigur.e 1 has terminated, and let A 2 CTA , B 2 CTA [ f?g, and 2 fB; :_Bg. Then, Proof. We show the contrapositive. We assume that if D 2= L(vC ), then T j= C 6v D. In the following we show that a model for C 6v D can be derived from the saturation graph G, i.e., by constructing a canonical model I(C) w.r.t. T such that x 2 CI n DI . I(C) is de ned iteratively starting with I(C0). We de ne I0(C) := fxC g and DI0(C) := fxC j D = Cg for all D 2 CA .
T v-Rule In case = D then for every x 2 ( Ii \ CIi ) n DIi+1 add x to DIi+1 . In case
construction is done in the l- and e-Rule. v:-Rule In case = D then for every x 2 ( Ii n CIi ) n ( Ii+1 n DIi+1 ) add x to = ./ n R:C the model construction is done in the l- and e-Rule item below. = ./ n R:C the model
v -Rule This rule has no impact on the model construction. vu-Rule For every x 2 ( Ii \ C1Ii \ C2Ii ) n DIi add x to DIi+1 . vu:-Rule For every x 2 ( Ik \ CiIk ) n (CjIk [ DIk ) add x to DIk+1 (i; j 2 1::2; i 6= j). l-Rule, e-Rule Let rIi = TR2r RIi , qIi = Tq02q q0Ii , and k 2 1::n. For every x 2
(x; yk) 2 rIi+1 with yk 2 qIi+1 exist, introduce new individuals yk to and add (x; yk) to RIi+1 for every R 2 r.
Rules vP1 ; vP2 ; vP3 ; vP4 Let QIPi = Tq2Q(v;LP (vF )) qIi , QIPi: = Ii n QIPi , QvIi = Tq2LvE \ CQT qIi , E; F 2 CTA , and x 2 EIi . By the composition rules for LP and the infeasibility result of the ILP component we know that EIi QIPi: F Ii because EIi \ QIPi = ;. Now for every x 2 ( Ii \ EIi ) n F Ii+1 add x to F Ii+1 .
The rules vP:1 ; vP:2 ; vP:3 ; vP:4 are analogous to vP1 ; vP2 ; vP3 ; vP4 and for lack of space we omit this part of the completeness proof here.
The construction of a model is performed in a fair manner, i.e., every rule applicable to already existing elements in Ii is applied before applying rules to new elements. The constructed model I(C) is indeed a model of C w.r.t T . Due to lack of space we cannot prove this in detail but we argue informally. Although our rules deal with E LQ, a subset of these deal with E L if one assumes that only QCRs of the form 1R:C are allowed. Thus, we claim that our rules are complete for E L. Due to the semantics of QCRs and their allowed occurrence on the left- and and right-hand side of axioms, these can entail subsumptions that are not possible in E L. In order to ensure completeness we introduced the labels LP and LP: that aggregate possible (non-)subsumption conditions caused by QCRs. In order to prove subsumption or disjointness we create corresponding QCR clones. In case a clone is satis able after all rules have terminated this clone can serve as a model for the non-subsumption or non-disjointness. In case additional entailed information is added to the saturation graph that causes the unsatis ability of a QCR clone, we will add the entailed subsumption or disjointness to the sets subs and unsat that are used by the ILP component. Regarding the l- and e-rule there could exist another possible incompleteness because a numerically satis able set of QCRs could eventually cause the unsatis ability of a created anonymous node due to entailed information missing in the graph at the time of the feasibility test. However, if such an anonymous node becomes unsatis able, the cause of unsatis ability is learned by adding its cause to the sets subs and unsat . This ensures that a previously computed solution is monotonically constrained until either an anonymous node is determined as satis able or the set of QCRs becomes eventually infeasible. Again, this ensures that no model for non-subsumption or non-disjointness is overlooked and no subsumption or disjointness is missed.
Lemma (Termination). For every normalized E LQ Tbox over CT and RT the application of the saturation rules in Figure 1 will terminate in nite time.
Proof. The algorithm terminates naturally because the saturation graph is nite and its number of nodes is bounded by the size of the power set of CT and RT respectively, cycles are avoided by reusing nodes in accordance to standard subset blocking. Finally, the number of concepts, edges, QCRs, and subsumption tuples that can be added to L, LP , and LP: is again bounded by the size of the power set of CT and RT respectively. All rules extend labels monotonically. Once the precondition of a rule is true for elements of a graph G and the rule has red, it cannot re again for the same set of elements, thus, any series of rule applications is nite. 6
We developed a prototype system called Avalanche that implements our calculus as proof of concept.2 Its ILP component is based on IBM ILOG CPLEX Optimization Studio [IBM] that is freely available for academic research. Avalanche currently parses only E LQ ontologies expressed in RDF/XML syntax. For this rst release our focus is on a sound, complete, and terminating implementation. We did not optimize Avalanche for E L ontologies yet and many of our saturation rules are implemented very ine ciently. Deciding subsumption for named concepts where LP and/or LP: are not empty is currently computed very naively. We generate a QCR clone for each possible subsumption or disjointness via QCRs and the number of clones is bounded by n2 if the Tbox contains n named concepts.
Avalanche has been written in the Java programming language. It consists of two main components: a reasoner and an external ILP module. The ILP module is needed for feasibility testing of QCRs. The reasoner executes in the following way: First, it parses the input ontology le. The axioms in the le must conform to our E LQ syntax. If an axiom in the ontology does not conform to the E LQ syntax restrictions an exception will be raised and the system will terminate. After the parsing is completed, the input axioms are rewritten to our internal normal form. Then, we build nodes representing all concepts declared in the original ontology le as well as the ones obtained during the normalization phase.
Our reasoning process is divided into two phases: an unfolding and a rule application phase. During the unfolding phase we apply the rules v, v./, v.:/, P , and P :. In this phase, each rule is applied only once to each node. Afterwards, during the rule application phase, we apply all rules rules except v, v./, and v.:/. The rules do not have to be applied in any particular order. We apply all matching rules to all the nodes. The system calls the external ILP module when it needs to solve a system of inequalities.
2Avalanche web page: https://users.encs.concordia.ca/%7Ehaarslev/Avalanche/ Ontology Name canadian-parliament-factions-1 canadian-parliament-factions-2 canadian-parliament-factions-3 canadian-parliament-factions-4 canadian-parliament-factions-5 canadian-parliament-full-factions-1 canadian-parliament-full-factions-2 canadian-parliament-full-factions-3 canadian-parliament-full-factions-4 canadian-parliament-full-factions-5 C-SAT-exp-ELQ C-UnSAT-exp-ELQ genomic-cds rules-ELQ-fragment-1 genomic-cds rules-ELQ-fragment-2
The experiments were performed on a MacBook Pro (2.6 GHz Intel Core i7 processor, 16GB memory) using only one core. The comparison results (average of 3 runs) are shown in Figure 4. We compared Avalanche with major OWL reasoners: FaCT++ (1.6.4) [FaC], HermiT (1.3.8) [Her], Konclude (0.6.2) [Kon], and Racer (3.0) [HM01, HHMW12, Rac], which is the only other available OWL reasoner using an ILP component for reasoning about QCRs. The algorithms implementing Racer's ILP component are in general best-case exponential to the number of QCRs given for one concept. Some metrics about the benchmark ontologies are shown in Figure 3.
The rst benchmark (see top part of Figure 4) uses variants of two real-world ontologies modelling a component of the Canadian Parliament, namely the House of Commons, which is a democratically elected body that had 308 members in the last Parliament (most members elected in 2011) [Can]. For each Canadian province a faction is de ned [Can] that is composed of members elected in the same province. In order to ensure subsumptions based on QCRs we de ned four concepts categorizing factions as tiny, small, medium, or big, based on the number of faction members. Each faction belongs to exactly one of these faction categories. The second version adds a concept de ning for the House of Commons the number of members from each province [Can]. The only reasoners that can classify all variants of the simplest of these ontologies within the given time limit are Avalanche and Racer. Avalanche still exhibits an exponential runtime increase but it is the only reasoner that can classify all variants of these ontologies. The performance of Racer for the simpler ontology is a good indication that Avalanche can achieve similar runtimes with optimized reasoning algorithms.
The second benchmark (see middle part of Figure 4) uses synthetic concept templates that are similar to the example used in Section 3. The original ALCQ concepts are shown below the table. They were manually rewritten into normalized E LQ as demonstrated in Section 3. The concept templates use a variable n that is increased exponentially. The numbers used in the template are bounded by the value of 2n. The rst template is satis able and the second one unsatis able. Only Avalanche and Racer can classify all variants of these small ontologies within the time limit.
The third benchmark (see bottom part of Figure 4) uses two E LQ fragments of a real world ontology, genomiccds rules [Sam13, Sam14], which was developed for pharmacogenetics and clinical decision support. It contains many concepts using QCRs of the form = 2 has:Ai. However, in these fragments the concepts (Ai) occurring in the quali cation of the QCRs do not interact with one another. This simpli es the reasoning and all reasoners except Racer perform well. Avalanche and HermiT as well as FaCT++ and Konclude have similar runtimes. These fragments are interesting because the concept <#human> contains several hundred QCRs using the same role. This is one of the reasons why Racer timed out for both fragments. 7
We presented the rst calculus that combines saturation and ILP-based reasoning to decide subsumption for E LQ. Our preliminary experiments indicate that this calculus o ers a better scalability for quali ed cardinality restrictions than approaches combining both tableaux and ILP as well as traditional (hyper)tableau methods. We already started to improve the e ciency of our implementation and expect a signi cant speedup for our next n 40 20 10 5 3 release. We plan to add a preprocessing phase that automatically rewrites ALCQ ontologies to our E LQ syntax. Our next steps are to extend our calculus to cover role hierarchies and inverse roles. [ADF09]
H. M. B. Amor, J. Desrosiers, and A. Frangioni. On the choice of explicit stabilizing terms in column generation. Discrete Applied Mathematics, 157(6):1167{1184, 2009.
F. Baader, S. Brandt, and C. Lutz. Pushing the E L envelope. In Proc. of IJCAI, pages 364{369, 2005. [Can]
Canadian Parliament. https://en.wikipedia.org/wiki/House of Commons of Canada.
V. Chvatal. Linear Programming. Freeman, 1983.
FaCT++. http://owl.cs.manchester.ac.uk/tools/fact/. [Her]