Pushing the Boundaries of Reasoning About Qualified Cardinality Restrictions

Abstract

We present a novel hybrid architecture for reasoning about description logics supporting role hierarchies and qualified cardinality restrictions (QCRs). Our reasoning architecture is based on saturation rules and integrates integer linear programming. Deciding the numerical satisfiability of a set of QCRs is reduced to solving a corresponding system of linear inequalities. If such a system is infeasible then the QCRs are unsatisfiable. Otherwise the numerical restrictions of the QCRs are satisfied but unknown entailments between qualifications can still lead to unsatisfiability. Our integer linear programming (ILP) approach is highly scalable due to integrating learned knowledge about concept subsumption and disjointness into a column generation model and a decomposition algorithm to solve it. Our experiments indicate that this hybrid architecture offers a better scalability for reasoning about QCRs than approaches combining both tableaux and ILP or applying traditional (hyper)tableau methods.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The performance of the original $\mathcal {ALCQ}$ tableau algorithm [19] that is implemented by most description logic (DL) reasoners covering qualified cardinality restrictions¹ (QCRs) is not optimal. To perform a concept satisfiability test, the tableau algorithm creates role successors to satisfy at-least restrictions, e.g., ${\ge 20\, R.C}$. Given at-most restrictions, e.g., ${\le 10\, R.D}$, ${\le 10\, R.E}$, the algorithm resolves each R-successor as either D or $\lnot D$, and E or $\lnot E$. If an at-most restriction for R is violated (${\le 10\, R.D}$), the algorithm nondeterministically merges two R-successors that are instances of D. This uninformed process is highly inefficient, especially when the algorithm has to deal with larger cardinalities and/or large sets of related QCRs. In [11, Sect. 4.1.1] it was shown that if a set of QCRs contains p at-least (${\ge n_{i}\, R_{i}.C_{i}}$) and q at-most restrictions (${\le m_{j}\, R_{j}'.C'_{j}}$), then roughly $2^{qN} \prod _{i=0}^{M-2}\left( {\begin{array}{c}M-i\\ 2\end{array}}\right) /(M-1)!$ branches need to be explored in the worst case by the standard $\mathcal {ALCQ}$ algorithm (assuming that M $R'_{j}$-successors exist in $C'_{j}$ with $M > m_{j}$ and $N = \sum _{i=1}^{p} n_{i}$).

In our previous work (inspired by [26]) we have shown that algebraic tableaux can improve reasoning on QCRs dramatically for DLs such as $\mathcal {SHQ}$ [11], $\mathcal {SHIQ}$ [28], and $\mathcal {SHOQ}$ [9, 10]. The basic idea in these calculi is to transform a set of QCRs into a linear optimization problem that will be solved accordingly. These algorithms need to explore $2^{2^{p+q}}$ branches in the worst case but they are independent of N, M. If there is a feasible solution to the problem then the corresponding set of QCRs is satisfiable provided completion rules encounter no logical clashes for the returned solution. The prototypes implementing the above-mentioned approaches on algebraic tableaux [10, 11, 28] could demonstrate runtime improvements by several orders of magnitude for reasoning about QCRs (and nominals). However, we identified the following two disadvantageous characteristics.

(i) Given n QCRs (and nominals) the naive encoding of the corresponding system of inequalities requires n rows and $2^{m}$ columns, where m is the cardinality of the set P of all pairs of roles and their qualifications occurring in the n given QCRs. Let us illustrate this with a small example: ${\ge 2 R.C} \sqcap {\ge 2 R.D} \sqcap {\le 2 R.E}$. In this case, $P=\{R_{C},R_{D},R_{E}\}$, $n=3$, $m=3$. In order to represent the QCRs as inequalities we create $\sum x_{C_{i}} \ge 2$, $\sum x_{D_{j}} \ge 2$, and $\sum x_{E_{k}} \le 2$. For instance, the variables $x_{C_{i}}$ represent the cardinalities of all elements in the power set of P that contain $R_{C}$. The same holds for the other variables respectively. As an additional constraint we specify that all variables must have values in $\mathbb {N}$. Our objective function minimizes the sum of all variables. Intuitively speaking, the above-mentioned concept conjunction is feasible and also satisfiable in this trivial case if the given system of inequalities has a solution in $\mathbb {N}$. It is easy to see that the size of such an inequality system is exponential with respect to m. Furthermore, in order to ensure completeness, in our previous work we required a so-called choose rule that implements a semantic split that nondeterministically adds for each variable x either the inequality $x\le 0$ or $x\ge 1$. Unfortunately, this uninformed choose-rule could fire $2^{2^{m}}$ times in the worst case and cause a severe performance degradation.

(ii) The employed integer linear programming (ILP) algorithms were best-case exponential in the number of occurring QCRs due to the explicit representation of $2^{m}$ variables. In [9, 10] we developed an optimization technique called lazy partitioning that tries to delay the creation of ILP variables but it cannot avoid the creation of $2^{m}$ variables in case m QCRs are part of a concept model. Our experiments in [9,10,11] indicated that quite a few ILP solutions can cause clashes due to lack of knowledge about known subsumptions, disjointness, and unsatisfiability 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 to create an R-successor as an instance of $C \sqcap D$. 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 sacrifice 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 satisfiable), dedicated saturation rules determine whether the returned solutions are logically satisfiable. In case of logical unsatisfiability a corresponding unsatisfiable 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 unsatisfiability are eliminated. For instance, the example above would be deemed as infeasible once ILP knows that C, D are subsumed by E and C, D are disjoint.

The avoidance of characteristic (ii) is motivated by the observation that only a small number of the $2^{m}$ 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., [6]. Moreover, in practice, only a limited number of variables have a non-zero value in the integer optimal solution. In addition, linear programming techniques such as column generation [7, 13] 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 efficiency of the branch-and-price method, which is required in order to derive an optimal ILP solution, e.g., [3, 23, 31], 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). Furthermore, our new ILP approach considers known subsumptions, disjointness, and unsatisfiability of concept conjunctions and uses a different 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) [32]; (ii) feasibility of QCRs is decided by ILP (in contrast to [4]); (iii) our revised encoding of inequalities, which incorporates role hierarchies, the aggregation of information about subsumption, disjointness, and unsatisfiability of concept conjunctions, allows a more informed mapping of QCR satisfiability 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 [24]. This work extends our previous research on the $\mathcal {ELQ}$ Avalanche reasoner [32].

2 Preliminaries

Description logics are a family of knowledge representation languages that form a basis for the Web Ontology Language (OWL). The DL $\mathcal {ALCHQ}$, which is a core subset of OWL, allows role hierarchies ($\mathcal {H}$) and the concept-forming constructors conjunction, disjunction, negation, at-least and at-most restriction ($\mathcal {Q}$). The semantics of $\mathcal {ALCHQ}$ concepts and roles is defined by an interpretation $\mathcal {I} = (\varDelta ^{\mathcal {I}}, \cdot ^{\mathcal {I}})$ that maps a concept C to ${C^{\mathcal {I}} \subseteq \varDelta ^{\mathcal {I}}}$ and a role R to $R^{\mathcal {I}} \subseteq {\varDelta ^{\mathcal {I}}\times \varDelta ^{\mathcal {I}}}$. For convenience we use the concepts $\top$ and $\bot$ with $\top ^{\mathcal {I}} = \varDelta ^{\mathcal {I}}$ and $\bot ^{\mathcal {I}} = \emptyset$.

$\mathcal {ALCHQ}$ concepts are inductively defined from concept and role names using the constructors as follows ($n,m \in \mathbb {N},\, n\ge 1$, $\Vert \cdot \Vert$ denotes set cardinality, $F^{R,C}(x)=\{y \in C^{\mathcal {I}} \,|\, (x,y) \in R^{\mathcal {I}}\}$): (i) $(C \sqcap D)^{\mathcal {I}} = C^{\mathcal {I}} \cap D^{\mathcal {I}}$; (ii) $(C \sqcup D)^{\mathcal {I}} = C^{\mathcal {I}} \cup D^{\mathcal {I}}$; (iii) $(\lnot C)^{\mathcal {I}} = \varDelta ^{\mathcal {I}} \setminus C^{\mathcal {I}}$; (iv) $(\ge n\, R.C)^{\mathcal {I}} = \{x \,|\, \Vert F^{C,R}(x)\Vert \ge n\}$; (v) $(\le m\, R.C)^{\mathcal {I}} = \{x \,|\, \Vert F^{C,R}(x)\Vert \le m\}$. The latter two constructors are called QCRs. A concept C is satisfiable if there exists an $\mathcal {I}$ such that $C^{\mathcal {I}} \ne \emptyset$.

An $\mathcal {ALCHQ}$ Tbox $\mathcal {T}$ is defined as a finite set of axioms of the form ${C \sqsubseteq D}$ or ${R \sqsubseteq S}$, where C, D are concepts and R, S roles, and such axioms are satisfied by $\mathcal {I}$ if $C^{\mathcal {I}} \subseteq D^{\mathcal {I}}$ or $R^{\mathcal {I}} \subseteq S^{\mathcal {I}}$. We call $\mathcal {I}$ a model of $\mathcal {T}$ if it satisfies all axioms in $\mathcal {T}$. A Tbox $\mathcal {T}$ entails an axiom if all models of $\mathcal {T}$ satisfy that axiom.

One of the main tasks of a DL reasoner is to classify a Tbox by computing all subsumptions between named concepts. Tableau-based algorithms [2] are the most applied reasoning algorithms to date. Consequence-based or saturation-based algorithms [4, 30] are algorithms that accumulate or saturate entailed knowledge in a bottom-up way while tableaux attempt to prove entailment in a goal-oriented or top-down way. The idea of saturating knowledge comes from the one-pass saturation algorithm for the DL $\mathcal {EL}^{++}$ [1]. $\mathcal {EL}$ only allows conjunction and existential value restriction (${\exists R.C} \equiv {\ge 1\, R.C}$). Different optimization techniques exist for different types of tasks performed by DL reasoners. In this work, we are interested in applying linear optimization in order to handle qualified number restrictions [9,10,11] in ontologies expressed in $\mathcal {ELQ}$, which is a superset of $\mathcal {EL}$ that additionally allows QCRs. It is well-known that $\mathcal {ELQ}$ is a syntactic variant of $\mathcal {ALCQ}$ [1].

Atomic decomposition was initially proposed in [26] to reason about sets, however it can also be used to reason about role fillers of qualified number restrictions in description logics. This technique allows us to reduce the problem of deciding feasibility of qualified number restrictions to solving a linear program. The example below illustrates how to transform qualified number restrictions into inequalities. Let us assume the following three qualified number restrictions ${\ge 3\, hasColor.Blue }$, ${\ge 4\, hasColor.Red }$, ${\le 5\, hasColor.Green }$. We denote the partition of the set $\{b,r,g\}$ ($b = blue$, $r = red$, $g = green$) as $\{b,r,g, br, bg, rg, brg \}$ where the absence of a letter indicate the implied presence of its negation, e.g., b stands for the intersection of blue, not red, not green. Then, we get the corresponding inequalities ($| \, . \, |$ denotes set cardinality).

In such a way we preserve the semantics of qualified number restrictions and reduce a satisfiability problem to a feasibility problem, i.e., whether a 0–1 linear program is feasible.

3 Column Generation and Branch-and-Price Methods

We discuss here how to check the feasibility of a 0–1 linear program with a column generation model, i.e., with an exponential number of variables. It consists in first checking whether its linear relaxation, a linear program with an exponential number of variables, is feasible. We next provide a brief overview of linear programming (LP for short) and column generation.

Linear Programming was recognized as one of the most important scientific achievements of the 20th century. It allows the solution of complicated problems that concern allocation of scarce resources with respect to various constraints in a minimum amount of time. There exist different approaches to solve linear programs. One of them is the simplex method that was proposed in 1947 by George B. Dantzig. Although the simplex method requires an exponential number of iterations in the worst case, it performs very well in practice. In 1979 the ellipsoid method was proposed by Leonid Khachiyan, and could solve linear programming problems in polynomial time. Nevertheless, the simplex method, despite being worst-case exponential is more efficient in practice than the ellipsoid method. The interior-point method is another polynomial-time algorithm that was proposed in 1984 by Narendra Karmarkar and its recent refinements [12] are competitive with the simplex algorithm.

The algorithms mentioned above have been integrated into different commercial and open source solvers, e.g., CPLEX, Gurobi, XPRESS. These solvers are capable of solving very large linear programming problems, i.e., with up to hundreds of thousands of variables. When it comes to millions of variables, their performance starts to deteriorate. We can then use the column generation method. The idea behind this method is that only a subset of all variables (columns) have non zero values in the optimal LP solution. Indeed, there are no more than the number of constraints, i.e., the number of so-called basic variables in linear programming. Numerous large-scale optimization problems are now using it [23].

Back to feasibility checking, column generation can easily detect infeasible linear programs. However, infeasible integer linear programs do not necessarily have an infeasible linear programming relaxation. In order to detect infeasibility in such cases, it is then required to use a branch-and-price algorithm [3] (i.e., a branch-and-bound algorithm [25] in which the linear relaxation is solved with a column generation method).

In the context of our work, we create very large integer linear programs with numerous variables. Therefore, we choose to solve the continuous relaxation with the column generation method to address scalability issues, following the success of using it for, e.g., deciding the consistency of a set of clauses in the context of probabilistic logic [17, 20]. In order to produce integer solutions, column generation is combined with a branch-and-price algorithm [3] to either conclude that the model has no solution or to obtain an integer solution.

Column generation together with the branch-and-price method have been implemented into a system that we decided to call QMediator. QMediator is a middle layer or a mediator that facilitates communication between Avalanche and CPLEX. This process will be described in detail in Sect. 5. In short, whenever Avalanche needs to process qualified number restrictions it calls QMediator. QMediator in turn creates a corresponding integer linear program based on the received information and solves it by means of column generation and branch-and-price methods. To actually solve the integer linear program QMediator calls CPLEX.

The example below illustrates how column generation works in practice, without the need of a branch-and-price method for this particular example.

Consider the axiom $D \sqsubseteq {\ge 2\, R.A} \sqcap {\ge 3\, R.B} \sqcap {\le 4\, R.C}$. Initially we assume that there is no known subsumption relationship between the QCR qualifications A, B, C. Since we have only one role, we can ignore its name and only focus on $Q_D = Q^{\ge }_D \cup Q^{\le }_D$, which is our base set for partitioning, with $Q^{\ge }_D = \{A, B\}$ and $Q^{\le }_D = \{C\}$. The complete decomposition set (or partition) is $\mathcal {D}_D = \{\{A\}, \{B\}, \{C\}, \{A, B\}$, $\{A, C\}$, $\{B, C\}$, $\{A, B, C\}\}$ where each partition element p represents the intersection of p’s elements plus the intersection of all $\lnot e_{i}$ with $e_{i} \in Q_D {\setminus } p$. We denote the elements of $\mathcal {D}_D$ by the variables $x_{A}, x_{B}$, $x_{C}$, $x_{AB}, x_{AC}, x_{BC}$, $x_{ABC}$. In the context of the ILP model, note that each variable is associated with a column, so we may use either terms in the sequel.

First Example. The QCRs for concept D result in the following ILP problem.

$$\begin{aligned} \min \quad \sum _{p \in \mathcal {D}_D} x_{p} \end{aligned}$$

(1)

subject to:

$$\begin{aligned} x_{A} + 0x_{B} + 0x_{C} + x_{AB} + x_{AC} + 0x_{BC} + x_{ABC}&\ge 2 \quad \leadsto {\ge 2\, R.A} \end{aligned}$$

(2)

$$\begin{aligned} 0x_{A} + x_{B} + 0x_{C} + x_{AB} + 0x_{AC} + x_{BC} + x_{ABC}&\ge 3 \quad \leadsto {\ge 3\, R.B} \end{aligned}$$

(3)

$$\begin{aligned} 0x_{A} + 0x_{B} + x_{C} + 0x_{AB} + x_{AC} + x_{BC} + x_{ABC}&\le 4 \quad \leadsto {\le 4\, R.C} \\ x_p \in \mathbb {N}, \qquad \text {for } p \in \mathcal {D}_D. \nonumber \end{aligned}$$

(4)

The optimal solution is $x_{B} = 1$, $x_{AB} = 2$, and all other variables are equal to zero.

However, since the size of $\mathcal {D}_D$ is exponential with respect to the size of $Q_D$, in general one cannot afford to enumerate all variables. In order to use a column generation modelling, model (1)–(4) is decomposed into a restricted master problem (RMP), made of a subset of columns, and the pricing problem (PP), which can be viewed as a column generator. The RMP contains the inequalities (rows) representing the QCRs, with a very restricted set of variables. Initially one can start with an empty set P of variables $x_{p}$, and a set of artificial variables $h_{q}$, one for each constraint, i.e., for each element in $Q_D$ (here $n=3$) using an arbitrarily large cost W (here ${W=10}$). Those artificial variables define an initial artificial feasible solution, however, in order to be feasible, the QCR set must not use any of them in its solution.

The cost of a partition element p is defined as the number of elements it contains. Consequently, the objective function of the RMPs is defined as $\sum _{p \in P} \mathrm {cost}_{p} x_{p} + W \sum _{i=1}^{n} h_{i}$. The choice of the cost is related to the selection of partition elements of smaller sizes and thus of less restricted solutions. Indeed, it promotes the reuse of nodes in Avalanche’s saturation graph. The optimal solution² of (RMP 1) has a cost 50, and contains two non-zero artificial variables.

The objective of the PP is equal to the so-called reduced cost in linear programming (see, e.g., Chvatal [6] if not familiar with linear programming). It uses the dual price values as coefficients of the variables associated with a potential partition element, i.e., binary variables $b_{q}, r_{q}$ ($q \in Q_D$) to ensure the description logics semantics of QCRs. The variables $b_{q}$ indicate whether role successors must be an instance of q and $r_{q}$ whether an R-successor that is an instance of q must exist. For each at-least QCR with a role and its qualification, P must contain a corresponding variable, e.g., for ${\ge 2\, R.A}$ if $r_{A}=1$ a variable b containing A in its subscript must exist ($r_{A} - b_{A} \le 0$). If P contains a qualification of an at-most QCR, then a corresponding variable must be present, e.g., if C occurs in P ($b_{C}=1$), then a variable r containing C in its subscript must exist ($b_{C} - r_{C} \le 0$). The objective function of the PP can then be written as

$$\begin{aligned} \sum \limits _{q \in Q_D} b_{q} - \sum _{q \in Q^{\ge }_D} \pi _{q} r_{q} - \sum _{q \in Q^{\le }_D} \omega _{q} r_{q} \end{aligned}$$

(5)

Based on this formula we can define (PP 1). In its objective function the only non-zero dual price values (coefficients) are $\pi _{A}, \pi _{B}$ due to (RMP 1).

Since the values of $r_{A},r_{B}$ are 1, we add the variable $x_{AB}$ to the next RMP ($P = \{\{A,B\}\}$). The cost of its solutions is reduced, from 50 in (RMP 1) to 6 in (RMP 2).

In the objective of (PP 2) the only non-zero dual price value is $\pi _{B}$ (see also (5)).

Since the value of $r_{B}$ is 1, we add the variable $x_{B}$ to the next RMP ($P = \{\{B\}$, $\{A,B\}\}$), whose cost is further reduced, from 6 in (RMP 2) to 5 in (RMP 3).

In the objective of (PP 2) the only non-zero dual price values are $\pi _{A},\pi _{B}$.

At this point all variables $h_{i}$ in (RMP 3) and $r_{q}$ in (PP 3) are zero indicating that we have reached a feasible solution. Moreover, since the reduced cost of the problem is always positive no “improving” column can be added. This allows us to conclude that we have reached the optimal solution of the LP. Lastly, as this LP optimal solution is integer, we can also claim that it defines the optimal set of partition elements. The inequality system (1) is feasible and the solution in (RMP 3) results in creating one R-successor that is an instance of B with cardinality 1 ($x_{B} = 1$) and one R-successor that is an instance of $A \sqcap B$ with cardinality 2 ($x_{AB} = 2$). Obviously, this solution satisfies the initial inequalities since the successor $A \sqcap B$ satisfies $\ge 2\, R.A$ and $\ge 2\, R.B$. Thus, the B successor together with the ${A \sqcap B}$ successor will satisfy $\ge 3\,R.B$.

Second Example. This example adds to the first example the axioms $A \sqsubseteq C$ and $B \sqsubseteq C$. The original inequality system (1) and (RMP 1) remain unchanged. The new pricing problem below accommodates the added subsumptions, e.g., $A \sqsubseteq C$ is modelled as ${b_{A} \le b_{C}} \Longleftrightarrow {b_{A} - b_{C} \le 0}$.

Since the values of $r_{A},r_{B},r_{C}$ are 1 we add the variable $x_{ABC}$ to the next version of our RMP ($P = \{\{A,B,C\}\}$), which reduces the cost from 50 to 9 in (RMP 5).

Since the values of $r_{B},r_{C}$ are 1 we add the variable $x_{BC}$ to the next version of our RMP ($P = \{\{B,C\}, \{A,B,C\}\}$), which reduces the cost from 9 to 8 in (RMP 6).

All variables $r_{q}$ are zero, so, no variable can be added to minimize (RMP 6) further. The inequality system (1) is feasible and according to (RMP 6) we create an R-successor that is an instance of $B \sqcap C$ with cardinality 1 and an R-successor that is an instance of $A \sqcap B \sqcap C$ with cardinality 2. Since we have 3 R-successors that instances of C, the QCR $\le 4\, R.C$ is satisfied.

Third Example. This example adds to the second example the axiom $A \sqcap B \sqsubseteq \bot$. The original inequality system (1) and (RMP 1) remain unchanged. The new pricing problem below accommodates the added disjointness, i.e., $A \sqcap B \sqsubseteq \bot$ is modelled as ${b_{A} + b_{B} \le 1}$.

Since the values of $r_{A},r_{C}$ are 1 we add the variable $x_{AC}$ to the next version of our RMP ($P = \{\{A,C\}\}$), which reduces the cost from 50 to 34 in (RMP 8).

Since the values of $r_{B},r_{C}$ are 1 we add the variable $x_{BC}$ to the next version of our RMP ($P = \{\{B,C\}, \{A,C\}\}$), which reduces the cost from 34 to 14 in (RMP 9).

All variables $r_{q}$ are zero, so, no variable can be added to minimize (RMP 9) further. However, the inequality system (1) is now infeasible because (RMP 9) still contains the non-zero artificial variable $h_{2}$. The infeasibility is caused by the disjointness between the QCR qualifications A and B.

Fig. 1.

Optimization chart

The process described above is summarized in Fig. 1. We first define RMP and apply column generation to produce new columns until we obtain an optimal solution. Then, if the solution is infeasible the submitted QCRs are infeasible as well. Otherwise, if the solution is feasible then we proceed with applying the branch-and-price method. If the problem is not feasible, then it will be detected at some iteration in the branch-and-price, while solving the linear relaxation with the column generation algorithm. Otherwise, if the problem is feasible, then the branch-and-price will output a feasible solution.

4 Role Hierarchies

Role hierarchies can easily be mapped to ILP. We illustrate the methodology first with a small example and later with one that entails role subsumption. However, please note that they have not yet been integrated in the current version of Avalanche.

Simple Example. Let $A \sqsubseteq {\ge 2\, S.B} \sqcap {\ge 2\, U.C} \sqcap {\le 3\, R.\top }$ with S, U subroles of R. The concept A is satisfiable and its least constrained model must have at least one SU-successor that is an instance of $B \sqcap C$. Role hierarchies only need to be considered if an at-most QCR referring to a superrole (R) is restricting other QCRs referring to subroles (S, U) of R. The semantics of role hierarchies is encoded in the inequalities generated for the corresponding at-most QCRs.

We define $Q^{\ge }_{A} = \{S_{B}, U_{C}\}$ and $Q^{\le }_{A} = \{R\}$. Since S, U are subroles of R, any partition element containing a subrole and its superrole can be simplified by removing the superrole because their intersection is equal to the subrole, e.g., $\{S_{B},R\}$ is equal to $\{S_{B}\}$. Additionally, R can be removed from $Q_{A}$ because no at-least QCR mentioning R exists. The complete decomposition set is $\mathcal {D}_{A} = \{\{S_{B}\}, \{U_{C}\}, \{S_{B}, U_{C}\} \}$. We denote these partition elements by the variables $x_{S_{B}}, x_{U_{C}}, x_{S_{B}U_{C}}$.

The QCRs for concept A result in the following ILP problem.

(6)

The optimal solution is $x_{S_{B}} = 1$, $x_{U_{C}} = 1$, $x_{S_{B}U_{C}} = 1$. We create one SU-successor that is an instance of $B \sqcap C$, one S-successor that is an instance of B, and one U-successor that is an instance of C. All three successors have a cardinality of 1.

Example with Entailed Role Subsumption. The combination of role hierarchies and QCRs can be used to entail role subsumptions. Let us assume a Tbox $\mathcal {T} = \{ \top \sqsubseteq {\le 1\, R.\top }$, ${\ge 1\, S.\top } \sqsubseteq C$, $C \sqsubseteq {\ge 1\, U.\top }$, $A \sqsubseteq {\ge 1\, S.B} \sqcap {\le 0\, U.B}\}$ with S, U subroles of R. $\mathcal {T}$ entails that S is a subrole of U and thus $A \sqsubseteq \bot$. It is easy to see that A is subsumed by C via the role S. Thus the QCRs applicable to A are ${\le 1\, R.\top },{\ge 1\, S.B}, {\le 0\, U.B}$, ${\ge 1\, U.\top }$.

We define $Q^{\ge }_{A} = \{S_{B}, U\}$ and $Q^{\le }_{A} = \{R,U_{B}\}$. After applying the simplifications from above we get $\mathcal {D}_{A} = \{\{U\}, \{S_{B}\}, \{U_{B}\}$, $\{U, S_{B}\}, \{S_{B}, U_{B}\} \}$. We denote these partition elements by the variables $x_{U}, x_{S_{B}}, x_{U_{B}}, x_{US_{B}}$, $x_{S_{B}U_{B}}$.

The QCRs for concept A result in the following ILP problem.

(7)

The system’s infeasibility is caused by the encoding of the entailed role subsumption $S \sqsubseteq U$ (first three inequalities) and ${\le 0\, U.B}$ (fourth inequality). If any of these four inequalities is removed, the remaining system becomes feasible.

5 Communication of Avalanche with QMediator

Avalanche is a complex rule-based system that implements a consequence-based reasoning algorithm presented in [32]. The algorithm manages the application of rules to an input ontology by traversing the completion graph. A dedicated module QMediator is called when a rule needs to expand the underlying graph or when a clash has been detected in a node due to the presence of qualified number restrictions. With the help of the module we can reduce the problem of deciding satisfiability of qualified number restrictions to the feasibility of inequalities, which gives us a clear advantage over other existing systems. To avoid circular dependencies between the two systems (considered an anti-pattern in software design) QMediator cannot call or access any data from Avalanche. Avalanche in its turn cannot directly call CPLEX.

During the execution of the algorithm the rules are being applied to an input ontology and a directed completion graph is constructed to store the inferred information. There can be four types of nodes in the graph – identified nodes, anonymous nodes, auxiliary nodes, and two types of cloned nodes – a positive clone to test subsumption between concepts and a negative clone to test disjointness between concepts. If a positive/negative node becomes unsatisfiable then the subsumption/disjointness holds. Each node in a given completion graph is uniquely identified by its representative concept. A representative concept is either a concept (a concept name) declared in the original ontology or a concept created during the reasoning process. All nodes contain a set of subsumers and only identified nodes contain a set of possible subsumers. Subsumers are other concepts that subsume the representative concept of a node. Possible subsumers are collected by a dedicated rule and are needed for subsumption testing. As it can be guessed from their name, possible subsumers represent the subsumers that can possibly subsume the representative concept of a node. Thus, we can avoid performing unnecessary subsumption tests.

Fig. 2.

Clash detection

When a node is subsumed by qualified number restrictions it has to call the graph expansion rule. The rule in its turn will call QMediator and pass the corresponding information: the qualified number restrictions, the subsumers of the qualifications and their unsatisfiable concept conjunctions. After that, the mediator will transform this information into a linear program, and it will call CPLEX to solve it or in other words to find a model. The result of this call is returned to the rule. Thus, the rule will have all the necessary information to expand the graph or to make the node unsatisfiable by adding $\bot$ (bottom) to its subsumers. As a result, the expansion rule may create additional nodes in the graph - the anonymous nodes. An anonymous node represents a situation when a role filler is not a single concept (e.g., A) but rather an intersection of concepts ($A \sqcap B$).

In Fig. 2 we show how the call to QMediator is integrated into the clash detection process. If a node becomes unsatisfiable, then the cause of the unsatisfiability has to be identified. If there is a logical clash (e.g., A and $\lnot A$ are present in the node) then the corresponding ancestors of the node will be made unsatisfiable. However, if the clash is due to the presence of qualified number restrictions then the mediator should be called and it should be asked to recompute a more constrained model. If a new model was computed, the rules can continue to be applied. If there is no model and the node is an identified node, then the corresponding ancestors of the node should be made unsatisfiable. If the node is an anonymous node this information will be recorded to avoid having the QMediator recompute the same model. Otherwise, the node in question must be a positive/negative cloned node. In this case it can be concluded that the subsumption/disjointness holds and the node will be marked as unsatisfiable.

Fig. 3.

Metrics of benchmark ontologies (# = Number of ..., A = Axioms, C = Concepts, R = Roles)

6 Performance Evaluation

We extended the test suite that we used in our previous work to evaluate the performance of Avalanche [32]. The test suite is composed of three different collections of test ontologies that will be presented below. We chose these ontologies to be classified to stress test the performance of Avalanche with respect to different applications of qualified cardinality restrictions. Some metrics about the test ontologies are shown in Fig. 3. The ontologies differ by the number of axioms, concepts, roles, and qualified number restrictions.

The first test collection models the House of Commons of the Canadian parliament [5] (see top part of Fig. 4). It is our own collection of $\mathcal {ELQ}$ ontologies where we represent a real-world situation. There are two versions of this benchmark - short and full, each consisting of six variants. The variants differ by the number of included factions [5]. The only reasoners that can classify all variants of the simplest of these ontologies within the given time limit are Avalanche and Racer. Avalanche is the only reasoner that can classify all variants of these ontologies.

The second test collection (see middle part of Fig. 4) uses synthetic concept templates. The original $\mathcal {ALCQ}$ concepts are shown below the table. They were manually rewritten into normalized $\mathcal {ELQ}$. 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 first template is satisfiable and the second one is unsatisfiable. Only Avalanche and Racer can classify all variants of these small ontologies within the time limit.

The third test collection (see bottom part of Fig. 4) uses four $\mathcal {ELQ}$ fragments of a real world ontology, genomic-cds_rules [29], which was developed for pharmacogenetics and clinical decision support. It contains many concepts using QCRs of the form $= 2\, has .A_{i}$. However, in these fragments the concepts ($A_{i}$) occurring in the qualification of the QCRs do not interact with one another. This simplifies reasoning and all reasoners except Racer perform well. Avalanche (with the exception of the fourth fragment) and HermiT as well as FaCT++ and Konclude have similar runtimes. These fragments are interesting because the concept $\texttt {{<}\#human{>}}$ contains several hundred QCRs using the same role. This is one of the reasons why Racer times out for all fragments. At the moment we can classify only the above mentioned fragments of the ontology in question. Our ultimate goal is classify the entire ontology. As we know, no other reasoner can do it yet.

Fig. 4.

Benchmark runtimes in seconds with a timeout of 1000 s (TO = timeout, #F = Number of Factions, Ava = Avalanche, Fac = FaCT++, Her = HermiT, Kon = Konclude, Rac = Racer)

As compared to our previous work [32], the performance of Avalanche has already been greatly improved. However, we expect to achieve even better results in future. Avalanche’s speed for the Canadian Parliament ontologies has been improved by several orders of magnitude. Previously it could not classify the version of Canadian Parliament with 10 factions within 10,000 s. The reason for such a change is mainly due to the improved communication with QMediator. Previously we delegated all computations that concerned qualified number restrictions to the dedicated module. After a scrupulous analysis of Avalanche’s runtime we noticed that a lot of time is spent in the module to solve rather simple cases. It appears that Linear Programming methods are typically used to solve feasible problems. If a problem is infeasible then it should be considered as erroneous and it has to be remodelled. However, in our case we do not consider infeasible models to be erroneous. On the contrary, they help us to discover valuable knowledge about the ontology in question, e.g. subsumption or disjointness. As a result, we identified several cases where feasibility/infeasibility information can be discovered without CPLEX. For example, we do not need to call QMediator when we have only at-least or only at-most restrictions. In the former case we simply connect with an edge the node that contains the number restrictions and the nodes that contain role fillers as their representative concepts. In the latter case we do not need to do anything because at-most inequalities do not require us to create successors (remember that 0 will satisfy $\le 5 R.C$). We have a special treatment when we have a set of at-least and at-most inequalities and all at-most inequalities are of cardinality 0. We also check if we can reduce all at-least inequalities and all at-most inequalities to only one inequality. For example, $\ge 3 R.C$ and $\ge 5 R.C$ could be replaced by $\ge 5 R.C$. Similarly, $\le 0 R.C$ and $\le 6 R.C$ could be replaced by $\le 0 R.C$. Further, we have other ways to determine early infeasibility. For example, $\le 3 R.C$ and $\ge 1 R.D$ would be infeasible if C is subsumed by D. Thus, QMediator is now called only when it cannot be avoided.

Although Racer can classify some of the test ontologies faster than Avalanche, we are not discouraged by this fact because we know exactly how we have to improve Avalanche in order to achieve comparable or even better results. In particular, we will be working on a reimplementation of the strategy that is used to apply rules to nodes.

The experiments were performed on a MacBook Pro (2.6 GHz Intel Core i7 processor, 16 GB memory). The comparison results (average of 3 runs) are shown in Fig. 4. We compared Avalanche with major OWL reasoners: FaCT++ (1.6.4) [8], HermiT (1.3.8) [18], Konclude (0.6.2) [22], and Racer (3.0) [14, 15, 27]. In fact, Racer is the only other available OWL reasoner using an ILP component for reasoning about QCRs in contrast to [21] where ILP is used in the context of probabilistic reasoning. The algorithms implementing Racer’s ILP component are in general best-case exponential with respect to the number of QCRs given for one concept. Another reasoning approach for $\mathcal {ALCQ}$ [16] used SMT with a theory that is a specific and computationally much cheaper subcase of Linear Arithmetic under the Integers but this approach suffers from inefficiencies for nested QCRs where reasoning involves backtracking. It would also not scale well for role hierarchies and its extension to inverse roles is an open problem.

7 Conclusion

In this work we presented a hybrid architecture for reasoning about description logics supporting role hierarchies and QCRs. It allows us to reduce the QCR satisfiability problem to a feasibility problem. We tested our system and identified ontologies that cannot be classified by other reasoners in a reasonable amount of time. We almost finished extending the architecture to cover $\mathcal {ALCHQ}$. Our ultimate goal is to extend our architecture to the DL $\mathcal {ALCHIQ}$ by adding inverse roles ($\mathcal {I}$).