We present a hybrid tableau calculus for the description logic SHIQ that decides ABox consistency and uses an algebraic approach for more informed reasoning about qualified number restrictions (QNRs). Benefiting from integer linear programming and several optimization techniques to deal with the interaction of QNRs and inverse roles, our approach provides a more informed calculus. A prototype reasoner based on the hybrid calculus has been implemented that decides concept satisfiability for ALCHIQ. We provide a set of benchmarks that demonstrate the effectiveness of our hybrid reasoner.
It is well known that standard tableau calculi for reasoning with qualified number
restrictions (QNRs) in description logics (DLs) have no explicit knowledge about set
cardinalities implied by QNRs. This lack of information causes significant performance
degradations for DL reasoners if the numbers occurring in QNRs are increased. Over
the last years a family of hybrid tableau calculi has been developed that address this
inefficiency by integrating integer linear programming (ILP) with DL tableau methods,
where ILP is used to reason about these set cardinalities. We developed hybrid calculi
for the DLs ALCQ [
Informally speaking this line of research is based on several principles: (i) role
successors are semantically partitioned into disjoint sets such that all members of one set
are indistinguishable w.r.t. to their restrictions; (ii) cardinalities of partitions are
denoted by non-negative integer variables and the cardinality of a union of partitions can
be expressed by the sum of the corresponding partition variables; (iii) all members of
a non-empty partition are represented by a proxy element [
In this section we briefly describe syntax and semantics of SHIQ and its basic
inferences services. Furthermore, we define a rewriting that reduces SHIQ to SHIN n in
order to apply the atomic decomposition technique [
Let I be a set of individual names. A SHIQ ABox A w.r.t. a role hierarchy R
:
is a finite set of assertions of the form of a : C, ha; bi : R, and a 6= b with IA
I the set of individuals occurring in A and a; b 2 IA and R a role. We assume an
interpretation I = ( I ; :I ), where the non-empty set I is the domain of I and :I is
an interpretation function which maps each concept to a subset of I and each role to
a subset of I I . Semantics and syntax of the DL SHIQ are presented in [
An interpretation I holds for a role hierarchy R iff RI SI for each R v S 2 R. An interpretation I satisfies a TBox T iff CI DI for every GCI C v D 2 T . An interpretation I satisfies an ABox A if it satisfies T and R and all assertions in: A such that aI 2 CI if a : C 2 A, haI ; bI i 2 RI if ha; bi : R 2 A, and aI 6= bI if a 6= b 2 A. Such an interpretation is called a model of A. An ABox A is consistent iff there exists a model I of A. A concept description C is satisfiable iff CI 6= ;.
Let E be a concept expression, then clos(E) defines the usual closure of all
concept names occurring in E. Therefore, for a TBox T if C v D 2 T , then clos(C)
clos(T ) and clos(D) clos(T ). Likewise for an ABox A, if (a : C) 2 A then
clos(C) clos(A). Inspired by [
Definition 1 (unQ). Let R0 be a new role in NR with R := R [ fR0 v Rg for each transformation. unQ rewrites the axioms as follows: unQ(C) := C if C 2 NC , unQ(:C) := :C if C 2 NC otherwise unQ( :_C), unQ(8R:C) := 8R:unQ(C), unQ(C u D) := unQ(C) u unQ(D), unQ(C t D) := unQ(C) t unQ(D),
P7 P5 ST R ST
P6
RT P4 T
P2 R α(v001) = P1, α(v010) = P2, α(v100) = P4, α(v011) = P3, α(v110) = P6, α(v101) = P5,
α(v111) = P7 unQ(> nR:C) := > nR0 u 8R0:unQ(C), unQ(6 nR:C) := 6 nR0 u 8(R n R0): unQ( :_C: ), unQ(a : C) := a : unQ(C), unQ(ha; bi : R) := ha; bi : R, : unQ(a 6= b) := a 6= b.
Note that this rewriting generates a unique new role for each QNR. For instance,
unQ(> nR:C u 6 mR:C u > kR :D) is rewritten to > nR1 u 8R1:C u 6 mR2 u
8(R n R2)::C u > kR3 u 8R3:D and fR1 v R; R2 v R; R3 v R g R. SHIN n
is not closed under negation due to the fact that unQ(6 nR:C) itself creates a
negation which must be in NNF before further applying unQ. In order to avoid the whole
negating problem for the concept description generated by unQ(6 nR:C) and unQ(>
nR:C) the calculus makes sure that the application of unQ starts from the innermost
part of an axiom, therefore such concept descriptions will never be negated.
Atomic decomposition A so-called atomic decomposition for reasoning about sets was
proposed in [
for nodes x and y with R 2 L(hx; yi) and R v S, y is called S-successor of x and x is Inv(S)-predecessor of y. If y is an S-successor or an Inv(S)-predecessor of x then y is called and S-neighbor of x. In addition, if R 2 L(hx; yi) then y is an R-filler (role-filler) for x. The R-fillers of x are defined as F il(x; R) = fy j hxI ; yI i 2 RI g. Definition 4 (Precedence). Due to the existence of inverse roles for each pair of individuals x; y, R 2 L(hx; yi) imposes Inv(R) 2 L(hy; xi). A global counter PR keeps the number of nodes and is increased by one when a new node x is created, setting PRx = PR. Hence, each node is ranked with a PR. A successor of x with the lowest PR is called parent (parent successor) of x and others are called its children. Accordingly, a node x has a lower precedence than a node y if x has a lower rank compared to y. Also, each node has a unique rank and no two nodes have the same rank. Definition 5 ( ). Assuming a set of variables V, a unique variable v 2 V is associated with a set of role names RV v. Let VR = fv 2 V j R 2 RV vg be the set of all variables which are related to a role R. The function maps number restrictions to inequations such that (R; ./;n) := (Pvi2VR vi) ./ n.
Definition 6 (Distinct partitions). Rx is defined as the set of related roles for x such that Rx = fS j f (S; >;n); (S; 6;m)g \ LE (x) 6= ;g. A partitioning Px is defined as Px = SP Rx fP g n f;g. For a partition Px 2 Px, PxI = (TS2Px F ilI (x; S)) n (SS2(RxnPx) F ilI (x; S)) with F ilI (x; S) = fyI j y 2 F il(x; S)g. Let be a mapping : V $ Px for a node x, each variable v 2 V is assigned to a partition Px 2 Px such that (v) = Px.
The definition clearly demonstrates that the fillers of x related to the roles of partition Px are not the fillers of the roles in Rx n P (other partitions). Therefore, by definition the fillers of x associated with the partitions in Px are mutually disjoint w.r.t. the interpretation I. An arithmetic solution is defined using the function : V ! N mapping each variable in V to a non-negative integer. Let Vx be the set of all variables assigned to a node x such that Vx = fvi 2 V j vi 2 LE (x)g, a solution for a node x is (x) := f (v) = n j n 2 N; v 2 Vxg. The inequation solver uses an objective function to determine whether to minimize the solution or maximize it. We minimize the solution in order to keep the size of the forest small.
The example in Fig. 1 depicts the process of finding an arithmetic solution in more detail. Let L(x) = f6 2S; > 1R; 6 2T ; > 3T g be the label of node x. Applying the atomic decomposition for the related roles Rx = fS; R; T g results in seven disjoint partitions such that Px = fPi j 1 6 i 6 7g where P1 = fSg, P2 = fRg, P4 = fT g, P3 = fS; Rg, P5 = fS; T g, P6 = fR; T g, P7 = fR; S; T g as shown in Fig. 1. In order to simplify the mapping between variables and partitions, each bit in the binary coding of a variable index represents a specific role in Rx. Therefore, in this example the first bit from right represents S, the second R, and the last T . Since jRxj = 3, the number of variables in Vx becomes 23 1. The mapping of variables and the resulting inequations in LE (x) are also shown in Fig. 1.
Definition 7 (Node Cardinality). The cardinality associated with proxy nodes is defined by the mapping card : V ! N.
Since the hybrid algorithm requires to have all numerical restrictions encoded as a set of inequations, three functions are defined to map number restrictions (NRs) to inequations and/or further constrain variables. Function (see Def. 5) is used in the >-Rule and 6Rule as shown in Fig. 2. Function and & also add new inequations to the label LE of a node and modify the variables. The functions and & are respectively used in the IBE-Rule and resetIBE -Rule as shown in Fig. 2.
Definition 8 ( ). For a set of roles RO and k 2 N, the function (RO; k) maps number restrictions to inequations via the function for each Rj 2 RO. (RO; k) returns a set of inequations such that (RO; k) = f (Rj ; >; k) j Rj 2 ROg [ f (Rj ; 6; k) j Rj 2 ROg. For v 2 VRj , if Rj 2 (v) ^ (v) * RO then v 6 0 is also returned. Definition 9 (&). For a set of roles RO and k 2 N, the function &(RO; k) maps number restrictions to inequations via the function for each Rj 2 RO. &(RO; k) returns a set of inequations such that &(RO; k) = f (Rj ; >; k) j Rj 2 ROg [ f (Rj ; 6; k) j Rj 2 ROg. For v 2 VRj , if RO = (v) then v = k is also returned.
Definition 10 (Proper Sub-Role). For each role in existing number restrictions a set will be assigned which contains a specific type of sub-role called proper sub-role. A proper sub-role <(R) for a role R is defined as <(R) = fRi j (R 2 NR [ Inv(R)) ^ Ri v Rg.
This makes specializing the edges between nodes possible. Therefore, in our algorithm when a role set is assigned to L(hx; yi) a new proper sub-role Si will be created for each role S 2 L(hx; yi), where <(S) = <(S) [ fSig, and will be assigned to the edge label. A role in <(S) cannot have any proper sub-role. Only roles that occur in number restrictions and their inverses can have proper sub-roles. Since these proper sub-roles do not appear in the logical label of nodes, they do not violate the correctness of our algorithm.
Definition 11 (Blocked Node). Since SHIQ does not have the finite model property
pair-wise blocking [
>-Rule and 6-Rule: all number restrictions from L(x) are collected via these two rules. The function maps them to inequations according to the proper atomic decomposition and adds them to LE (x).
IBE-Rule: this rule considers the implied back edge as a set of NRs, maps them to a set of inequations, add the inequations to the LE , and determines potential variables that can represent the IBE through elimination of the non-related variables. Assume that for a node x a successor y has been created with L(hx; yi). This implies a back edge for
Fig. 2. The complete tableaux expansion rules for SHIQ-ABox y with a label LI (y) = Inv(L(hx; yi)). This back edge is considered as a set of NRs of the form > 1Ri; 6 1Ri where Ri 2 Inv(L(hx; yi)). The IBE-Rule transforms the implied back edge into a set of inequations in LE (y) of the form (Pvj2VRi vj ) > 1 and (Pvj2VRi vj ) 6 1 using the function &. Since the inequations representing the back edge are restricted to the value one, only one common variable vk in these inequations will be (vk) = 1. In addition, & ensures that the potential variables for IBE include all the roles in LI (y) (see Def. 9).
resetIBE -Rule: this rule extends LE as follows. If for a node y and its parent node x, L(hx; yi) 6= Inv(L(hy; xi)), then it implies that a new role should be considered in LE (x) due to the restrictions of its child y. Therefore, the resetIBE -Rule fires for x where extends LE (x) to consider Inv(L(hy; xi)) and ensures that the specific variable representing it is included in the solution as in Def. 8.
reset-Rule: if a new number restriction with a new role R is added to the logical label of a node x, all its children are discarded from the tree and LE (x) = ;.
BE-Rule: this rule fills a label of the back edge a node to its parent due to the solution of the inequation solver. If a variable v in a solution exists such that (v) = 1 and LI (y) (v), then v represents the back edge and the BE-Rule fires and fills the edge label.
We adjust the edges between a pair of nodes to satisfy the nature of the inverse roles between them. Interactions of IBE-Rule, BE-Rule, and resetIBE -Rule maintain this characteristic.
RE-Rule: this rule sets the edge between two root nodes. For nodes a; b 2 IA, (a; b) : R is considered as a : > 1Rab; a : 6 1Rab, b : > 1Inv(Rab); b : 6 1Inv(Rab) with Rab v R and Inv(Rab) v Inv(R). Therefore, a variable with the value of 1, (v) = 1, for node a that contains Rab represents this edge. The RE-Rule fires and fills the edge label.
merge-Rule: the merge-Rule merges root nodes. Assume three root nodes a; b; c 2 IA where b; c are respectively R-successor and S-successor of a. These assertions will be translated such that we have a : > 1Rab; a : 6 1Rab; a : > 1Sac; a : 6 1Sac with Rab v R and Sac v S. If there exists a variable v in an arithmetic solution of node a with Rab; Sac 2 (v), it means that c and b need to be merged. The merge-Rule merges b and c and w.l.o.g replaces every occurrence of b with c and all outgoing/incoming edges of b become outgoing/incoming edges of c.
ch-Rule: this rule is necessary to ensure the completeness of the algorithm. The partitions of the atomic decomposition represent all possible combinations of the successors of a particular node. The inequation solver has no knowledge about logical reasons that can force a partition to be empty. Thus, from a semantic branching point of view we need to distinguish between the two cases v 6 0 and v > 1, where v denotes the cardinality of a partition.
f il-Rule: the f il-Rule has the lowest priority among the completion rules. This rule is the only one that generates new nodes, called proxy nodes. For example, if a solution for a node x includes a variable v with (v) = 2, the f il-Rule creates a proxy node y with cardinality of 2 and sets the edge label and LI (y) as shown in Fig. 2. Since this rule generates proxy nodes based on an arithmetic solution that satisfies all the inequations, there is no need to merge the generated proxy nodes later.
The algorithm preserves role hierarchies in its pre-processing phase. If there occurs
a variable v 2 LE (x), where R 2 (v) and S 2= (v) and R v S, then v 6 0.
Therefore, the variables that violate the role hierarchy are set to zero. Due to the space
limitations, we refer for the proof to [
In this section, we discuss the complexity of our algorithm and evaluate its behavior in
practical reasoning. Let k be the number of all roles occurring in NRs in a TBox after
pre-processing and transforming all QNRs to unqualified ones considering inverse roles.
The search space of the hybrid algorithm depends on the number of variables occurring
in LE labels. Since there are k roles, the number of partitions and their associated
variables is bounded by 2k 1. The ch-Rule creates two branches for each variable: v >
1 or v 6 0. Consequently, 22k cases could be examined by the inequation solver and the
worst-case complexity of the algorithm is double exponential. Moreover, the Simplex
method which is used in the hybrid algorithm is NP in the worst case. However, in [
In most cases, in order to utilize these theoretical algorithms in practice, optimization
techniques are required. Due to the complexity of the algorithm, achieving a good
performance may seem infeasible. However, optimization techniques can dramatically
decrease the size of the search space by pruning many branches. For instance, a
standard technique such as axiom absorption [
Variable initialization: the inequation solver starts with the default v 6 0 for all
variables and later sets some to v > 1 to satisfy the inequations according to at-least
restrictions. Since the ch-Rule is invoked 22k times in the worst case to check variables
for v 6 0 or v > 1, default zero setting of variables prevents unnecessary invocations of
the ch-Rule. Moreover, the boundary value of some of the variables can be determined
from the beginning according to the occurrence of the numbers in at-most or/and
atleast restrictions. For example, if a variable occurs in an at-least restriction but not in an
at-most restriction, then it does not have any arithmetic restriction and is called a don’t
care variable [
Algebraic Reasoning for SHIQ at-least at-most )s 106 d n o c e s i l l im103 n i ( e m i t n R100 u and it is not a sub-role of any role R in a concept of the form 88(R \n S).:C 22 L(x), then it cannot be in ↵ (v) where v represents a back edge for node x.
Dependency-directed bbaacckkttrraacckkiinngg::wweeuusseebbaacckktrtaracckki ninggtetcohfinniqduseosutorcfiesndofsolougrci-es ocafllcolgaischaelscalansdhethseanncdonthseidnecrothnesicdaeursteheofcaucsleasohfina scelattsihnginthseebttoinugndthareiebsooufnvdariaebsloesf vinarniaebwlessoliuntinoenws. sTohluistiroenssu.ltTs hinisprreusnuilntsg ibnrapnrcuhneinsgwbhriacnhcwheosulwdhleicahd wtootuhled slaemade tcolatshhe. sIfama eclcalsahsho. cIcfuarscilnashnoodcecuxr,s winhincohdweaxs, cwrehaictehdwdausectroeaatevdardiuaebletova wvaitrhiabl(ev)v =witkh an(dv)k= 2k aNnd; kk 2 N1,,k then1, vthemnuvstmbuestsbeet steot tzoerzoe.roT.hTishisisisccaallleleddssiimmppllee backtracking. The previous technique can be improved: if a logical clash is encountered due to {fA,; ¬:A}g 22 L(x), then the source for propagation of these two concepts to L(x) could be the roles occurring in 88 or 88\n constructs. In this case, the variables which contain all these roles are set to zero. This is called complex backtracking. These techniques eliminate many branches in the search space and consequently improving the average complexity of the algorithm.
In order to evaluate our hybrid algorithm, a prototype reasoner has been implemented in Java using the Web Ontology Language API. The reasoner decides satisfiability of ALCHIQ concepts.
We show the performance of the hybrid reasoner by a set of three benchmarks. Fig. 3 demonstrates the performance of different DL reasoners for testing the satisfiability of the concept Test 1 defined as C u > 2kRu88R.:(> kR .:Cu 6 kR .:C), where k = 2i,; 2 i 10. Fig. 3 compares the reasoning time of our hybrid reasoner with Pellet, FaCT++, and Hermit.1 All reasoners determine the satisfiability of the concept in less than ⇠ 100 ms before reaching k = 24. While our hybrid reasoner maintains its rreeaassoonniinngg ttiimmee ((ccoonnssttaannttllyy uunnddeerr 100 mmss)),, PPeelllleett,, HHeerrmmiitt,, aanndd FFaaCCTT++++ ssttaarrtt eexxhhiibbiittiinngg exponential growth in the reasoning time for values higher than k = 24. For example, for k = 29 Pellet’s reasoning time is more than 18 minutes and for k = 210 it did not finish within the time limit of 1000 seconds. This example demonstrates the independent behavior of our hybrid calculus in the presence of higher values in QNRs interacting with inverse roles. 1 We used an AMD 3.4GHz quad core CPU with 16 GB of RAM. dd nn oo cc i i nn i i (( ee 1100
22 mm i i t t nn uu RR1100
00 mm mm nn uu RR1100 00
RRoooosstataPPoouurr&&HHaaarsrslelevv
220000 440000 660000 with P defined as ./ 1M :C wwitihthPPddeefifinneeddaassfu/ . / . k . Fig. 4 shows the effect of increasing the kkg. .FFi gig. .44sshhoowwsst htheeeeffefecct tooffi ninccrereaassininggt hthee number of at-least and at-most restrictions in reasoning for Test . In a model for the nnuummbbeerrooffaat-tl-eleaassttaannddaat-tm-moossttreresstrtircictitoionnssi ninrereaassoonni ninggfoforrTTeesstt2. .InInaammooddeel lfoforrt hthee 22 concept Test , the concept expression P is propagated back and will be added to the ccoonncceeppt tTTeesstt2, ,t htheeccoonncceeppt teexxppreresssioionnPP isispproroppaaggaat eteddbbaacckkaannddwwilillbbeeaaddddeeddt otot hthee 22 l alabbeel looffaannooddeewwhhi cichhaalrlereaaddyyhhhaaasss>>>11RR. B.B, ,t htheererefoforere, ,wweehhaavvee((kk++11))QQNNRRss..SSi ninccee label of a node which already 1R:B, therefore, we have (k + 1) QNRs. Since for each node which has a parent, an IBE will be considered as a set of two inequations foforreeaacchhnnooddeewwhhi cichhhhaassaappaarerennt,t,aannIBIBEEwwilillbbeeccoonnssidideerereddaassaasseet toofft wtwooi nineeqquuaatitoionnss
LLEE in the of the node. As shown in Fig. 4, increasing the number of QNRs decreases i nint htheeLE oofft htheennooddee. .AAsssshhoowwnni ninFFi gig. .44, ,i ninccrereaassininggt htheennuummbbeerrooffQQNNRRssddeeccrereaasseess the performance of the hybrid reasoner. This is due to the fact that a large number of t htheeppeerfroformrmaanncceeoofft htheehhyybbrirdidrereaassoonneer.r.TThhisisisisdduueet otot htheefafacct tt hthaat taal alargrgeennuummbbeerrooff roles in the QNRs increases the number of variables and the size of the search space. rorol elessi nint htheeQQNNRRssi ninccrereaasseesst htheennuummbbeerrooffvvaariraiabbl elessaannddt htheessizizeeoofft htheesseeaarcrchhssppaaccee. . Comparing the two diagrams in Fig. 4a and 4b shows that by increasing the number CCoommppaarirninggt htheet wtwooddi aiaggrarammssi ninFFi gig. .44aaaanndd44bbsshhoowwsst hthaat tbbyyi ninccrereaassininggt htheennuummbbeerr of at-most QNRs the reasoning time for the arithmetic reasoner increases faster than ooffaat-tm-moossttQQNNRRsst htheerereaassoonni ninggtitmimeefoforrt htheeaarirtihthmmeetitcicrereaassoonneerri ninccrereaasseessfafassteterrt hthaann for at-least restrictions. The reason is the heuristic that we explained in Section 4.1. By foforraat-tl-eleaassttreresstrtircictitoionnss..TThheerereaassoonnisist htheehheeuurirsistitcict hthaat twweeeexxppl alai nineeddi ninSSeecctitoionn44. 1.1. .BByy means of this heuristic, if a role occurs in an at-least restriction and not in any at-most mmeeaannssoofft hthisishheeuurirsistitcic, ,ififaarorol eleoocccuursrsi ninaannaat-tl-eleaassttreresstrtircictitoionnaannddnnoot ti ninaannyyaat-tm-moosstt restriction and satisfies the pre-conditions that are mentioned in Section 4.1, then the reresstrtircictitoionnaannddssaatitsisfifieesst htheepprere-c-coonndditiitoionnsst hthaat taareremmeenntitoionneeddi ninSSeecctitoionn44. 1.1, ,t htheennt hthee potential variables for IBE which contain this role are set to zero. Therefore, the number ppoot etenntitaial lvvaariraiabbl elessfoforrIBIBEEwwhhi cichhccoonnt atai nint hthisisrorol eleaareresseet tt otozzeeroro. .TThheererefoforere, ,t htheennuummbbeerr of variables in the search space is decreased. ooffvvaariraiabbl elessi nint htheesseeaarcrchhssppaacceeisisddeeccrereaasseedd. .
FFFooorrrtthhtheeetthhthiirridrddbbbeeennnccchhhmmmaaarrkrkkwwweeecccooonnnsssiiddideeerrrtthhtheeecccooonnnccceeeppptttTTTeeesssttt3 dddeeefififinnneeedddaaasss>>>888SSS.:AA.Au666999SSS.:AA.A 33 u8SSS.:((.(>>>kkRR. C.C u 6666TT. D.D u >>55TT. D.D))u 8SS. 8.RRR.:((.(>>>22TT. D.D
kR:C 6 6T :D > 5T :D) S: 2T :D uu88 uu uu uu8 8 8 8 6 3T :D) S: R: T : u 6633TT. D.D))u 8SS. 8.RR. 8.TT. . uu uu8 8 8 8 8 8 uu
T : R :P with R 8TT . 8.RR . P.P wwitihth fRR v 8 8 8 8 {{ vv
M MMg 2 }} 2 2
and k 100; : : : ; 1000 . Fig. 5a displays the R aannddkk 2 f110000, ,. . . ., ,11000000g. .FFi gig. .55aaddisisppl alayysst hthee
RR 2 2 {{ }} rurunntitmimeessfoforrTTeesstt3, ,wwhheererePPisisddeefifinneeddaaasss666((kk runtimes for Test , where P is defined (k 33
22))MM.(.(CCt DD))..InInt hthisiseexxaammppl elePPisis tt propagated back and causes the unsatisfiability of Test . Fig. 5b shows the runtimes for pproroppaaggaat eteddbbaacckkaannddccaauusseesst htheeuunnssaatitsisfifiaabbiliiltiytyooffTTeesstt3. .FFi gig. .55bbsshhoowwsst htheerurunntitmimeessfoforr 33 TTeesstt3 wwhheererePPisisddeefifinneeddaaasss666((kk++11))MM.(.(CCtDD))..InInt hthisiseexxaammppl elePPisisaalslsoopproroppaaggaat etedd Test where P is defined (k + 1)M:(C D). In this example P is also propagated 33 back but does not result in the unsatisfiability of Test . As expected the hybrid reasoner bbaacckkbbuut tddooeessnnoot treressuultlti nint htheeuunnssaatitsisfifiaabbiliiltiytyooffTTeesstt3. .AAsseexxppeecct eteddt htheehhyybbrirdidrereaassoonneerr 33 remains stable while the execution times of the other reasoners increase according to reremmaai ninsssstatabbl elewwhhilielet htheeeexxeeccuutitoionntitmimeessoofft htheeoot htheerrrereaassoonneersrsi ninccrereaasseeaacccoordrdi ninggt oto the values occurring in the QNRs. As shown in Fig. 5a and 5b, Hermit’s behavior is t htheevvaal ulueessoocccuurrirninggi nint htheeQQNNRRss..AAsssshhoowwnni ninFFi gig. .55aaaanndd55bb, ,HHeermrmiti’ts’sbbeehhaavvi oiorrisis the worst among all the reasoners. Hermit and Pellet show a rapid exponential growth t htheewwoorsrsttaammoonnggaal llt htheerereaassoonneersrs..HHeermrmititaannddPPeel lelet tsshhoowwaararappi dideexxppoonneenntitaial lggrorowwt hth in their reasoning times as a function of k. For k > 400, Hermit did not finish within i nint htheeirirrereaassoonni ninggtitmimeessaassaafufunncctitoionnooffkk. .FFoorrkk>>440000, ,HHeermrmititddi didnnoot tfifinnisishhwwitihthi nin the time limit of 1000 seconds. FaCT++ solves the problem in a more reasonable time, t htheetitmimeelilmimititooff11000000sseeccoonnddss..FFaaCCTT++++ssool vlveesst htheepprorobbl elemmi ninaammoorererereaassoonnaabbl eletitmimee, , however, it demonstrates its dependency on the value of k as its runtime increases. In hhoowweevveer,r,ititddeemmoonnsstrtarat etessitistsddeeppeennddeennccyyoonnt htheevvaal ulueeooffkkaassitistsrurunntitmimeei ninccrereaasseess..InIn addition, Fig. 5 shows the behavior of our hybrid algorithm using simple (Hybrid-S) aadddditiitoionn, ,FFi gig. .55sshhoowwsst htheebbeehhaavvi oiorrooffoouurrhhyybbrirdidaal glgoorirtihthmmuussininggssimimppl ele(H(Hyybbrirdid-S-S)) tt and complex (Hybrid-C) dependency-directed backtracking. The complex backtracking outperforms simple backtracking since it prunes more branches that would lead to the same sort of clash. In addition to improving the performance of the reasoner the optimization techniques used in hybrid reasoner can make its performance more stable.