Reducing Domino Problems to TBox Consistency

Once Lemma 3.6 has been proved, it is easy to reduce the bounded domino problem to $\ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}}$ consistency. We use the standard reduction that has been applied in the DL context, e.g., in [BS99].

Lemma 3.7
Let $\mathcal{D} = (D,V,H)$ be a domino system. Let $w = w_0 \dots w_{n-1} \in D^*$ . There is a $\ensuremath{\text{T\hspace{-1pt}}_C\hspace{-1pt}\text{Box}}$ $T(n,\mathcal{D},w)$ such that:

$T(n,\mathcal{D},w)$ is consistent iff $\mathcal{D}$ tiles U(2ⁿ,2ⁿ) with initial condition w.
$T(n,\mathcal{D},w)$ can be computed in time polynomial in n.

Proof. We define $T(n,\mathcal{D},w):= T_n\cup T_\mathcal{D} \cup T_w$ , where T_n is defined in Figure 3, $T_\mathcal{D}$ captures the vertical and horizontal compatibility constraints of the domino system $\mathcal{D}$ , and T_w enforces the initial condition. We use an atomic concept C_d for each tile $d \in D$ . $T_\mathcal{D}$ consists of the following cardinality restrictions:

$\begin{gather*}(\forall \ \underset{d \in D}{\bigsqcup} C_d), \quad (\forall \ ... ...it{north}}\xspace. \underset{(d,d') \in V}{\bigsqcup} C_{d'}))). \end{gather*}$

$\begin{displaymath}(\forall \ (C_{(0,0)} \rightarrow C_{w_0})), \dots, (\forall \ (C_{(n-1,0)} \rightarrow C_{w_{n-1}}) , \end{displaymath}$

The main result of this section is now an immediate consequence of Lemma 2.2, Lemma 3.7, and Corollary 3.3:

Theorem 3.8
Consistency of $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}$ - $\ensuremath {\text {T\hspace {-1pt}}_C\hspace {-1pt}\text {Boxes}}$ is $\textsc{NExp\-Time}$ -complete, even if unary coding of numbers is used in the input.

Recalling the note below the proof of Lemma 3.6, we see that the same argument also applies to $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}\xspace$ if we allow binary coding of numbers.

Corollary 3.9
Consistency of $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}\xspace$ - $\ensuremath {\text {T\hspace {-1pt}}_C\hspace {-1pt}\text {Boxes}}$ is $\textsc{NExp\-Time}$ -hard, if binary coding is used to represent numbers in cardinality restrictions.

It should be noted that it is open if the problem can be decided in $\textsc{NExp\-Time}$ , if binary coding of numbers is used, since the reduction of $\ensuremath{C^2}$ only yields decidability in 2- $\textsc{NExp\-Time}$ .

In the following section, we will see that, for unary coding of numbers, deciding consistency of $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}$ - $\ensuremath {\text {T\hspace {-1pt}}_C\hspace {-1pt}\text {Boxes}}$ can be done in $\textsc{Exp\-Time}$ (Corollary 4.8). This shows that the coding of numbers indeed has an influence on the complexity of the reasoning problem. It is worth noting that the complexity of pure concept satisfiability for $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}}$ does not depend on the coding; the problem is $\textsc{PSpace}$ -complete both for binary and unary coding of numbers [Tob00].

For unary coding, we needed both inverse roles and cardinality restrictions for the reduction. This is consistent with the fact that satisfiability for $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}$ concepts with respect to TBoxes consisting of terminological axioms is still in $\textsc{Exp\-Time}$ , which can be shown by a reduction to the $\textsc{Exp\-Time}$ -complete logics $\mathcal{CIN}$ [De 95] or CPDL [Pra79]. This shows that cardinality restrictions on concepts are an additional source of complexity. One reason for this might be that $\ensuremath{\mathcal{A}\!\mathcal{L}\!\mathcal{C}\!\mathcal{Q}\!\mathcal{I}}$ with cardinality restrictions no longer has the tree-model property.