Reducing Domino Problems to TBox Consistency

Once Lemma 3.6 has been proved, it is easy to reduce the bounded domino problem to 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 $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*}$$

$\mathcal{T}_w$ consists of the cardinality restrictions

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

where, for each x,y, C_(x,y) is a concept that is satisfied by an element a iff $\textit{pos}\xspace(a) = (x,y)$, defined similarly to C_(0,0) and C_{(2ⁿ-1,2ⁿ-1)}. From the definition of $T(n,\mathcal{D},w)$ and Lemma 3.6, it follows that each model of $T(n,\mathcal{D},w)$ immediately induces a tiling of U(2ⁿ,2ⁿ) and vice versa. Also, for a fixed domino system $\mathcal{D}$, $T(n,\mathcal{D},w)$ is obviously polynomially computable.

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 - is -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$- is -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 , if binary coding of numbers is used, since the reduction of only yields decidability in 2- .

In the following section, we will see that, for unary coding of numbers, deciding consistency of - can be done in (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 does not depend on the coding; the problem is -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 concepts with respect to TBoxes consisting of terminological axioms is still in , which can be shown by a reduction to the -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 with cardinality restrictions no longer has the tree-model property.