
## 3.3 Reducing Domino Problems To T C Box Consistency

Once Lemma 3.6 has been proved, it is easy to reduce the bounded domino problem to T Box consistency. We use the standard reduction that has been applied in the DL context, e.g., in (Baader & Sattler, 1999).

Lemma 3.7 Let D = ( D, V, H ) be a domino system. Let w = w 0 . . w n − 1 ∈ D * . There is a TcBox T(n, D, w) such that:
- T ( n, D, w ) is consistent iff D tiles U ( 2 n, 2 n) with initial condition w .

- T ( n, D, w ) can be computed in time polynomial in n .

Proof.  We define T(n, D, w) := T, UT, UT, where T, is defined in Figure 3, T, captures the vertical and horizontal compatibility constraints of the domino system D, and Tw enforces the initial condition. We use an atomic concept C d for each tile d E D. T D consists of the following cardinality restrictions:

$$(\forall\prod_{d\in D}C_{d}),\quad(\forall\prod_{d\in D}\prod_{d\in D\setminus\{d\}}\neg(C_{d}\cap C_{d^{\prime}})),$$  $$(\forall\prod_{d\in D}(C_{d}\to(\forall\,\mathit{east}.\prod_{(d,d^{\prime})\in H}C_{d^{\prime}}))),\quad(\forall\prod_{d\in D}(C_{d}\to(\forall\,\mathit{north}.\prod_{(d,d^{\prime})\in V}C_{d^{\prime}}))).$$  
$$C_{(n-1,0)}\to C_{w_{n-1}}\,),$$

Tw consists of the cardinality restrictions
(A (C(0,0) -> Cwo )), . . . , (V (C(n-1,0) -> Cwn-1 ),
where, for each x,y, C(x,y) is a concept that is satisfied by an element a iff pos(a) = (x,y),
defined similarly to C (0,0) and C (2 n –1,2 n –1) .

From the definition of T ( n, D, w ) and Lemma 3.6, it follows that each model of T ( n, D, w )
immediately induces a tiling of U (2 n , 2 n ) and vice versa. Also, for a fixed domino system D, T(n, 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 ACCQI-T c Boxes is NEXPTIME-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 ALCQ if we allow binary coding of numbers.

## Corollary 3.9

Consistency of AXQ-T c Boxes is NEXPT IME -hard, if binary coding is used to represent nmbers in cardinality restrictions.

It should be noted that it is open if the problem can be decided in NEXP TIME, if binary coding of numbers is used, since the reduction of C 2 only yields decidability in 2-NEXP-
TI ME.