We consider reasoning problems in description logics and variants of first-order logic under the fixed-domain semantics, where the model size is finite and explicitly given. It follows from previous results that standard reasoning is NP-complete for a very wide range of logics, if the domain size is given in unary encoding. In this paper, we complete the complexity overview for unary encoding and investigate the effects of binary encoding with partially surprising results. Most notably, fixed-domain standard reasoning becomes NEXPTIME for the rather low-level description logics E LI and E LF (as opposed to EXPTIME when no domain size is given). On the other hand, fixed-domain reasoning remains NEXPTIME even for first-order logic, which is undecidable under the unconstrained semantics. For less expressive logics, we establish a generic criterion ensuring NP-completeness of fixed-domain reasoning. Amongst other logics, this criterion captures all the tractable profiles of OWL 2.
Description logics (DLs, [2, 14]) and other fragments of first-order logic are popular knowledge representation (KR) formalisms. Traditionally, the semantics underlying these formalisms do not constrain the number of elements of the described domain of interest; classical KR even admits models of infinite size. In many realistic knowledge representation scenarios, however, it is known that the domain must be finite, or even a bound on its size is given. In such scenarios, the classical semantics allowing for models of arbitrary (even infinite) size does not adequately reflect the reasoning requirements. Consequently, KR research has recently started to consider alternative semantics, leading to numerous novel (un)decidability and complexity results.
The finite model semantics, inspired by database theory, requires models to be finite (but of arbitrary size). Finite satisfiability checking and finite query entailment have been considered for a variety of description logics [11, 5, 13, 15]. Still, in some situations just requiring finiteness of the domain is not restrictive enough; sometimes the complete set of domain elements (or at least their precise number) are known, leading to the notion of the fixed-domain semantics [8]. First complexity investigations have shown that standard reasoning tasks are NP-complete for a wide range of DLs, when ? A version of this paper has been accepted for publication at EPIA (2017). the elements of the fixed domain are explicitly enumerated. These results directly carry over to the case where only the number of domain elements is provided but this number is given in unary encoding.
Previous work has left open (or has been too unspecific on) important questions regarding fixed-domain reasoning. First, it was not explicitly investigated, if and how the complexity results would be affected if the domain size would be considered as a fixed parameter rather than a variable part of the input. Second, reasoning complexities of (fragments of) first-order logic (which are undecidable under classical and finite-model semantics but become decidable when fixing the domain) have not been investigated thoroughly. Third, the effect of representing the size of the domain in binary encoding has not been considered at all. In this paper, we clarify the complexity landscape for fixed-domain standard reasoning in first-order logic and description logics by making the following contributions.
– We show that for unrestricted first-order logic, standard reasoning is NEXPTIME, no matter if the domain size is a fixed parameter or given in unary or binary as part of the input. For fixed size or unary encoding, the complexity drops to PSPACE when bounding the predicate arity, and to NP when the number of variables is bounded. – We show that for the binary encoding, the complexity remains NEXPTIME, even when the logic is drastically restricted. In particular, we show corresponding hardness results for E LI and E LF terminologies. – Finally, we establish NP-completeness for the binary encoding case for a wide range of lightweight logics by introducing a model-theoretic property shared by these logics and showing that it warrants NP-membership. 2 2.1
We assume the reader to be familiar with the basics of DLs [2, 14], as well as with the DL S ROIQ [9], of which we briefly recap some fragments we will use throughout this paper.
E L / E LI / E LF Terminologies E L terminologies are knowledge bases with only axioms of the form C v D, where C; D are concept expressions built from concept and role names using only top, conjunction, and existential quantification. We consider two extensions: E LI terminologies additionally allow the usage of role inverses, while E LF terminologies admit role functionality axioms of the shape > v 61 r:C. DLmin Knowledge Bases With DLmin, we refer to a minimalistic description logic that merely allows TBox axioms of the form A v :B, with A; B 2 NC . Moreover, only atomic assertions of the form A(a) are admitted. It is immediate that (finite) satisfiability checking in DLmin is in AC0.
First-Order Logic We assume the reader to be familiar with syntax and semantics of first-order predicate logic (FOL). By default, we assume that the only functions occurring are of arity zero (i.e., constants). We use FOL= to denote FOL with equality. By bounded-arity FOL(=) we denote FOL(=) using only predicates of arity smaller or equal to a given bound. By bounded-variable FOL(=) we denote FOL(=) using only a bounded number of variables. For uniformity, we use the typical DL notation also for first-order interpretations and we refer to FOL(=) sentences as (FOL(=)) axioms and to FOL(=) as (FOL(=)) knowledge bases. We recall that virtually all mainstream DLs (including SROIQ) can be expressed in bounded-arity FOL=. We also recall that Datalog denotes the function-free first-order Horn clauses. 3
In this paper, we investigate the effects of fixing the domain size of models. Given some s 2 N, we say a knowledge base K is s-satisfiable, if it has a model I = ( I ; I ) with j I j = s (referred to as an s-model) and an axiom ' is s-entailed by K (written: K j=s ') if every s-model of K is a model of '. We define s-subsumption accordingly.
Depending on how we treat the size parameter s, we distinguish three versions of the fixed-domain entailment decision problem (where, the function jj jj determines the size of a knowledge base or axiom according to some usual encoding): – assuming s fixed, the input is (K; '); the problem size is jjKjj+jj'jj – the input is (K; '; s) with s in unary; the problem size is jjKjj+jj'jj+s – the input is (K; '; s) with s in binary; the problem size is jjKjj+jj'jj+dlog2 se
In all cases, the output is “yes” if K j=s ' and “no” otherwise. We define the three versions of the fixed-domain satisfiability problem accordingly. 4 4.1
We first consider the case of unrestricted first-order logic, rectifying an incorrect result from the literature. Without giving a proof, Gaggl et al. [8] claim that this problem is PSPACE-complete, sketching an argument based on the assumption that any FOL model with polynomially many domain elements can be represented in polynomial space, which, however, only holds when the maximum predicate arity is bounded (see our results below). In fact, we can show that even for domain size 2, the problem is NEXPTIME-hard (even when no constants are used). We use a reduction from the TILING-problem, as it can be found in [12], which is known to be NEXPTIME-hard. Definition 1 (n n Tiling Problem). Given a set of square tile types T = ft0; : : : ; tkg, together with two relations H; V T T (horizontal and vertical compatibility, respectively), as well as an integer n in binary. An n n tiling is a function f : f1; : : : ; ng f1; : : : ; ng 7! T such that (a) f (1; 1) = t0, and (b) for all i; j (f (i; j); f (i+ 1; j)) 2 H, and (f (i; j); f (i; j + 1)) 2 V . TILING is the problem of deciding, given T; H; V , and n, whether an n n tiling exists. We refer to given T ,H,V , and n as tiling system T = (T; H; V; n).
8~x; ~y: 8~x; ~y::(ti(~x; ~y) ^ tj (~x; ~y))
^ i2f0:::m 1g 8~x; ~y; ~z:next (~x; ~y) ! i2f0:::m 1g
_ (ti;tj)2H (0(xi) ^ 0(yi)) ! t0(~x; ~y) 9x; y:1(x) ^ 0(y)
8x:1(x) $ :0(x) 8x; y:same(x; y) $ (1(x) $ 1(y)) 8~x; ~y: ipi (~x; ~y) $ 8~x; ~y:next (~x; ~y) $
ipi (~x; ~y)
^ (1(xj ) ^ 0(yj )) ^ 0(xi) ^ 1(yi) ^ ^ same(xj ; yj ) (
_
Theorem 1. The 2-satisfiability problem for constant-free FOL is NEXPTIME-hard.
Proof. We provide a reduction from TILING. Let n be the size of the grid. W.l.o.g.
we assume n = 2m. We now provide a FOL knowledge base (of size polynomial in
m) which is satisfiable iff a tiling exists. In the following, ~x stands for the sequence
x0; : : : ; xm 1 of variables (likewise ~y and ~z).
(
ti(~z; ~x) ^ tj (~z; ~y) _ (ti;tj)2V
With this knowledge base and a domain of size two, we use the two elements as 0 and 1 to encode the coordinates in the grid (0 : : : 2m 1) in binary, using m positions in the predicate for each coordinate. With this encoding, the next predicate is axiomatized to contain any pair of consecutive m-bit numbers. Then the ti predicates indicate the coordinate pairs of grid positions where the tile ti is positioned.
A matching upper bound will be provided through Theorem 4. The proof of the preceding theorem suggests that an unbounded predicate arity is essential for the result. Indeed, when bounding the maximal arity, the complexity can be shown to be PSPACEcomplete.
Theorem 2. The fixed-domain satisfiability problem for bounded-arity FOL(=) is PSPACE-complete when the domain size is fixed or given unary.
Proof. We show PSPACE-hardness of FOL satisfiability for domain size 2 by providing a reduction from the validity problem of quantified Boolean formulae (QBFs). We recap that for any QBF, it is possible to construct in polynomial time an equivalent QBF that has the specific shape = Q1x1Q2x2 : : : Qnxn' with Q1; : : : Qn 2 f9; 8g and ' being a propositional formula over the propositional variables x1; : : : ; xn. Let the firstorder sentence 0 be obtained from by replacing every occurrence of a propositional variable xi by true(xi) (thus reinterpreting the propositional variables as first-order variables and introducing true as the only unary predicate). It is now easy to see that is true iff 0 ^ 9x:true(x) ^ 9x::true(x) has a model with two elements.
We show PSPACE membership of FOL(=) satisfiability checking for domain size given in unary encoding by providing a PSPACE decision procedure for a given K and domain size s. Let k = jjKjj and ` = k + s. Let a be the upper bound on the arity. There can be at most k predicates, hence the size needed to represent a model is upperbounded by k sa ` `a, i.e., polynomial. Then we guess a polynomial size model representation and verify it in PSPACE [17]. This gives an NPSPACE algorithm which by Savitch’s theorem [16] can be turned into a PSPACE one. tu
Again, inspecting the previous proof, it seems to be essential that the number of used variables is unbounded. The subsequent theorem confirms that bounding the number of variables will lead to NP-membership.
Theorem 3. The fixed-domain satisfiability problem for bounded-variable FOL= is in NP when the domain size is given in unary encoding.
Proof. Let v be the upper bound on the number of variables. Let K be a FOL knowledge base with at most v variables, let s be the prescribed domain size and let ` = jjKjj + s. We now describe a nondeterministic polytime procedure for checking s-satisfiability of K. Let ' = V 2K and let I be a model of ' (and, hence, of K) with j I j = s. We guess cI for every free constant c occurring in K. We also guess for every subformula of ' the set Z of variable assignments : freevars(') ! I for which I; j= . We determine an upper bound for the size of the guessed information: ' has not more than 2` subformulae each of which has maximally v free variables, hence the size to store all Z is bounded by 2` sv and hence by 2` `v, i.e., polynomial in the input.
Verifying that the guessed information indeed satisfies the abovementioned property requires four checks: first, Z' must contain the empty function. Second, every Z must be compatible with the variable assignments of ’s subformulae in the following way (where ranges over I ):
Z: = ( I )freevars( ) n Z Z 1^ 2 = f 2 ( I )freevars( 1^ 2) j Z 1 Z 1_ 2 = f 2 ( I )freevars( 1_ 2) j Z 1
Z9x: = f 2 ( I )freevars(9x: ) j 9 : Z8x: = f 2 ( I )freevars(8x: ) j 8 : and Z 2
g or Z 2
g [ f(x; )g 2 Z g [ f(x; )g 2 Z g Third, for any atomic subformula which is an equality atom t1 =: t2, we need to check that 2 Z exactly if (t1) = (t2) where, given a , we let denote the extension of to arbitrary terms, mapping constants c to cI (as guessed before). Fourth, for any two atomic subformulae 1 = p(t1; : : : ; tk) and 2 = p(t01; : : : ; t0k), referring to the same predicate p, we need to check that they do not contradict each other w.r.t. any k-tuple being or not being in pI . This is checked by verifying if f( (t1); : : : ; (tk) j 2 Z 1 )g \ f( (t01); : : : ; (t0k) j 2 ( I )freevars( ) n Z 2 )g = ;; with defined as before. Note that the sets in this condition do only have polynomially many elements. All these checks can be done in polynomial time. Hence we obtain an NP upper bound for checking satisfiability. tu 4.2
We recall from Gaggl et al. [8] that fixed-domain standard reasoning in SROIQ with unary encoding is in NP. Note that this result is not subsumed by Theorem 3 since encoding number restrictions may require an unbounded number of variables. For one lower bound, we recall that 3-satisfiability is already NP-hard for DLmin [8], a very minimalistic DL that is subsumed by all tractable profiles of OWL. To also provide a lower bound for logics without ABox, we add a hardness result for terminologies. Proposition 1. Deciding 3-subsumption in E L terminologies is CONP-hard. Proof. We provide a reduction from the 3-colorability problem to non-3-subsumption. For a graph (V; E) with V = fv1; : : : ; vng, we introduce a concept name Avi for every vertex and one distinguished concept name Clash. Then we let the terminology K consist of the axioms Avi u Avj v Clash for every fvi; vj g 2 E. Then the graph is not 3-colorable iff K j=3 9r:Av1 u ::: u 9r:Avn v 9r:Clash. tu 5 5.1
Theorem 4. The fixed-domain satisfiability problem for FOL= with the domain size given in binary is in NEXPTIME.
Proof. Let K be a FOL knowledge base, s the prescribed domain size and let ` = jjKjj + dlog2 se. We now describe a nondeterministic exponential time procedure to cohfeKck) ws-isthatjisfiIajbi=litys aonfdKf.orLeevte'ry=suVbfo2rmKul a. Weofg'uewsseagmueosdsetlheI soeft 'Z (aonfdv,ahreianbclee, assignments : freevars(') ! I for which I; j= .
We determine an upper bound for the size of the guessed information: ' can contain at most ` different predicates and ` is also an upper bound for the arity of the predicates used in '. Therefore, the size to store I is bounded by ` s` and hence by ` (2`)` = ` 2`2 . ' has not more than 2` subformulae each of which has maximally ` free variables, hence the size to store all Z is bounded by 2` s` and hence by 2` (2`)` = 2` 2`2 . Verifying the claimed properties of I and all Z then can be done in polynomial time w.r.t. the exponential size input. Hence we obtain a NEXPTIME upper bound for checking satisfiability. tu This result subsumes NEXPTIME membership of fixed-domain satisfiability in all mainstream description logics. Also, by reducibility to FOL satisfiability checking, it follows that axiom entailment, conjunctive query entailment and even entailment of arbitrary Datalog queries (subsuming all kinds of navigational queries) is in CO-NEXPTIME.
We show CO-NEXPTIME hardness for subsumption in E LI and E LF terminologies under the fixed-domain semantics in binary encoding. Note that for both logics, the problem is EXPTIME-complete under the classical or finite-model semantics [10]. We show that constraining the domain size allows for encoding tiling problems. Similar constructions for much more expressive DLs have been described before [4, 18]. Reducing Tiling Problems to ELI Subsumption Given T = (T; H; V; n) (cf. Section 4.1), we construct an E LI terminology KT such that every model of KT not satisfying a certain subsumption (called countermodel) represents a tiling. For simplicity, we assume n = 2m. The countermodels we axiomatize shall consist of two types of domain elements: elements corresponding to grid positions and elements representing tile types. The former will be endowed with their x- and y-coordinates in binary representation, using concept names Xiz; Yiz, with (0 i < m) and z 2 f0; 1g to encode the each of the m bits of each coordinate. By means of the following axioms, we axiomatize the n n grid: 9h :(Xj0 u Xi0) v Xi0 9h :(Xj0 u Xi1) v Xi1(0 j < i) 9h :((X01 u : : : u Xi1 1) u Xi0) v Xi1 9h :((X01 u : : : u Xi1 1) u Xi1) v Xi0 9v :Xiz v Xiz
Xi0 u Xi1 v C? 9h:C? v C?
Origin v X00 u : : : u Xm0 1 u Y00 u : : : u Ym0 1
with 0 i < m and z 2 f0; 1g. Likewise, we let KT contain axioms obtained from
axioms (
We now turn to the domain elements representing the tile types. We will make sure that every countermodel contains one element per tile type and that every grid element is associated with one tile type via the tiledBy role. Regarding the tiling conditions in T; H; V , the following axioms are used:
Tilei v Tile (0 i k)
Tilei u Tilej v C? (0 i < j Origin v 9tiledBy :Tile0
Grid v 9tiledBy :Tile
Grid u Tile v C?
Origin v 9req :Tile1 u : : : u 9req :Tilek
9tiledBy :Tilei u 9h:9tiledBy :Tilej v C?
9tiledBy :Tilei u 9v :9tiledBy :Tilej v C?
where for each (ti; tj ) 62 H and (ti; tj ) 62 V we find an instance of (
(() By the arguments above it is immediate that from every correct tiling, a countermodel for the subsumption Origin v C? can be extracted. tu We want to emphasize that the imposed domain size is crucial for a) enforcing a grid of exponential size, and b) for exploiting the non-deterministic choice in tile assignments. Theorem 5. Subsumption in E LI under the fixed-domain semantics with binary encoding is CO-NEXPTIME-hard.
Proof. Note that for a given T = (T; H; V; 2m), the corresponding E LI terminology KT is of polynomial size in m. From Lemma 1 it then follows that, subsumption in E LI is CO-NEXPTIME-hard. tu
We finish the section by showing the same complexity for E LF by virtue of a small adaptation of the above argument.
Theorem 6. Subsumption in E LF under the fixed-domain semantics with binary encoding is CO-NEXPTIME-hard.
Proof. We reuse the construction made for E LI with the following modification: for r 2 fh; vg we add the axioms > v 61 r:> and we turn every axiom of the shape 9r :C1 v C2 into the axiom C1 v 9r:C2. It can be readily checked that the resulting knowledge base is an E LF terminology. Moreover, the countermodels obtained for E LI satisfy the functionality restriction imposed. Finally, in the presence of functionality of r, C1 v 9r:C2 entails 9r :C1 v C2, hence all the arguments in Lemma 1 carry over to this case. tu 5.3
We recall that even for a domain of fixed size and not part of the input, standard reasoning is already NP-hard for DLmin knowledge bases and E L terminologies (cf. Section 4.1, Theorem 1). Obviously these hardness results carry over to the unary and binary encoding case and to any logic subsuming any of the two. We now show that a generic property that is shared by many tractable DLs ensures NP-membership of standard reasoning tasks with domain size given in binary. We start with some modeltheoretic considerations.
Definition 2. We call a model nontrivial if its domain size is larger than 1. A knowledge base is called nontrivially satisfiable, if it has a nontrivial model. A logic L has the polynomial nontrivial model property if there is a polynomial function p : N ! N such that every nontrivially satisfiable L knowledge base of size k has a nontrivial model with at most p(k) elements.
This property has been shown to hold for a variety of prominent tractable logics. Among those, the recently introduced role-safety-acyclic Horn-S HOIQ [6] is rather general and subsumes the tractable profiles OWL QL and OWL RL of the Web Ontology Language. Another logic satisfying this property is E L++, even the version extended by reflexive roles and range restrictions [3, 1] subsuming the third tractable OWL profile OWL EL. Finally, the property holds trivially for Datalog, since there is always a model containing only as many individuals as there are constants.
In the following, we will introduce two kinds of model transformations and state some logics for which modelhood is preserved under these operations. Definition 3. Let I = ( I ; I ) and J = ( J ; J ) be interpretations. The product interpretation of I and J , denoted I J is the interpretation K with K = I
I , aK = (aI ; aJ ) for all a 2 NI , AK = AI AK for all A 2 NC , and rK = f(( ; 0); ( ; 0)) j ( ; ) 2 rI ; ( 0; 0) 2 rJ g for all r 2 NR.
A very helpful observation is that the classes of models of Horn (description) logics are closed under taking products [7]: given a Horn KB K and two interpretations I and J with I j= K and J j= K, it follows that I J j= K. The next model transformation that we describe consists in picking one element and “copying” it (as well as all its atomic class memberships and relation to other elements) n times.
Definition 4. Let n be a natural number, let I = ( I ; I ) be an interpretation and let 2 I . The n-fold duplication of in I creates an interpretation dupn(I; ) = J with J = (f0g I ) [ (f1 : : : ng f g) as well as aJ = (0; aI ) for all a 2 NI and for every predicate p of arity k holds ((n1; 1); : : : (nk; k)) 2 pJ if ( 1; : : : ; k) 2 pI . Definition 5. We call a logic L non-counting, if modelhood is preserved under arbitrary duplication of anonymous elements (i.e., elements 2 I with 6= aI for all a 2 NI ).
Note that FOL (without equality) is non-counting, and consequently all mainstream description logics without functionality and cardinality restrictions (that is, all DLs subsumed by SROI) are non-counting as well. Subsequent finding allows us to conclude NP-membership of satisfiability checking for a wide variety of (description) logics. Theorem 7. Let L be a non-counting Horn logic with bounded maximal predicate arity satisfying the polynomial nontrivial model property. Then fixed-domain satisfiability checking of L knowledge bases is in NP when using binary encoding. Proof. We describe a guess-and-check procedure. Let s be the prescribed domain cardinality and k = jjKjj be the size of the knowledge base. Let p be the polynomial as in the definition above. If s (p(k))2, we guess and polytime-verify a model of size s (the guessed model takes polynomial space as L has bounded arity by assumption). Otherwise, we guess and polytime-verify a nontrivial model I of some cardinality s~ p(k).
It remains to show that the existence of I ensures the existence of a model J of cardinality s. Let I0 = I I. Obviously, I0 has s~2 (p(k))2 elements and is again a model (since L is a Horn logic by assumption). Also by construction, I0 contains anonymous individuals (namely all elements of the form ( ; ) with 6= , existence guaranteed due to I being nontrivial). Let ( ; ) be one such anonymous individual. We obtain J by (s s~2)-fold duplication of ( ; ). Since L is non-counting, J is a model of the knowledge base. tu Corollary 1. Fixed-domain satisfiability checking with binary encoding is in NP for the logics: bounded-arity Datalog, role-safety-acyclic (RSA) Horn-SHOI, E L++ with reflexivity and ranges, and all tractable profiles of OWL: OWL EL, OWL QL, and OWL RL.
We investigated the complexities of standard reasoning under the fixed-domain semantics for first-order and a large range of description logics. We thereby specifically account for the encoding of the imposed domain size, and distinguish between fixed, unary, and binary. Table 1 summarizes our findings. We obtain quite uniform results of NP-completeness on the full range of description logics for the case of a fixed or unary encoded domain size. Contrariwise, in case of a binary encoding, little expressivity is needed to have standard reasoning jump to NEXPTIME where it remains for all formalisms subsumed by full first-order logic. Thus, regarding fixed-domain standard reasoning (i.e. satisfiability and non-entailment), we were able to complete the complexity landscape, and leave non-standard reasoning tasks, such as query answering as future work. Moreover, we consider a more fine granular investigation regarding data complexity.
This work is supported by DFG in the Research Training Group QuantLA (GRK 1763). We thank Franz Baader for asking the right questions, and are grateful for the valuable feedback from the anonymous reviewers, which helped greatly to improve this work.