# What is the impact of encodings of sparse structures on the complexity of the model checking problem?

Some preliminaries first. Consider a purely-relational structure (a.k.a. database) $$\mathfrak{A} = (A, R_1^{\mathfrak{A}}, \ldots, R_{|\tau|}^{\mathfrak{A}})$$ over some finite signature $$\tau = \{ R_1, R_2, \ldots, R_{|\tau|} \}$$, where each relational symbol $$R_i$$ has an associated arity $$\mathsf{ar}(R_i)$$. We assume that $$A$$ is ordered in some way, just for the sake of encodings.

There are two different ways to represent $$\mathfrak{A}$$ in the memory: one way comes from finite model theory, the second one from database theory. Let me call them the matrix encoding and the list encoding and define $$|\mathfrak{A}|$$ as the size of its encoding.

1. In the matrix encoding the structure $$\mathfrak{A}$$ is represented as $$1^{|A|} \cdot 0 \cdot \mathsf{enc}(R_1) \cdot \mathsf{enc}(R_2) \cdot \ldots \cdot \mathsf{enc}(R_{|\tau|})$$, where $$\mathsf{enc}(R_i)$$ is an $$|A|^{\mathsf{ar}(R_i)}$$ bit string, with the intended meaning that its $$j$$-th bit is 1 iff the $$j$$-th $$\mathsf{ar}(R_i)$$-tuple of $$A$$ belongs to $$R_k^{\mathfrak{A}}$$.
2. In the list encoding we encode the structure $$\mathfrak{A}$$ as $$1^{|A|} \cdot 0 \cdot \mathsf{enc}(R_1) \cdot \mathsf{enc}(R_2) \cdot \ldots \cdot \mathsf{enc}(R_{|\tau|})$$, but this time $$\mathsf{enc}(R_i)$$ just lists all the tuples included in $$R_i^{\mathfrak{A}}$$.

Hence, $$|\mathfrak{A}| \approx |A| + \Sigma_{i=1}^{|\tau|} |A|^{\mathsf{ar}(R_i)}$$ in the matrix encoding, while $$|\mathfrak{A}| \approx |A| + \Sigma_{i=1}^{|\tau|} \mathsf{ar}(R_i) \cdot |R_i^{\mathfrak{A}}|$$ in the list encoding. Note that the difference between the encoding is when we have a symbol $$S$$ of high-arity, let's say $$n$$ and there are only a few tuples in $$S^{\mathfrak{A}}$$. Then in the list encoding we will have only a few tuples included, so the representation of $$\mathfrak{A}$$ will be short, while in the matrix encoding we will store all the possible bits, no matter whether a tuple belongs to the relation $$S^{\mathfrak{A}}$$ or not. This seems to be also crucial when we have queries with negation: the relation itself can be "small" but its complement can be "huge", but the complement is not stored directly.

Finally, here comes my question. Do you know any logic (or query language) $$\mathcal{L}$$ for which the combined complexity of the model-checking problem (or query evaluation problem) differs (i.e. we have $$\mathfrak{A}$$ and a formula $$\varphi$$ as an input and we ask if $$\mathfrak{A} \models \varphi$$ holds)? Of course the signature may differ for different structures. And we need to exploit negations and higher-arity relations somehow.

• Note that for the guarded fragment GF, guarded negation fragment GNFO, unary negation fragment UNFO, first-order logic FO, k-variable first-order logic FO^k, modal logics, description logics and many others the complexity of model checking stays the same, no matter on what encoding you choose. I'm not sure what happens, e.g. with conjunctive queries with negation or RPQs with negation. Aug 12, 2021 at 5:01

First, we know that for every QBF formula $$\psi$$ there exists a sentence $$\varphi_\psi$$ of FO over the vocabulary $$\{P\}$$, where $$P$$ is unary, such that $$\psi$$ is true iff $$\mathfrak{A} := (\{0,1\},P^\mathfrak{A}) \models \varphi_\psi$$, where $$P^\mathfrak{A} = \{1\}$$, and the sentence $$\varphi_\psi$$ can be computed from $$\psi$$ in polynomial time (it is the obvious translation). If $$width(\varphi) := \max_{\theta \in Subf(\varphi)} |Free(\theta)|$$, then the following logic works $$\{\exists x_1 \dots \exists x_n R(x_1,\dots,x_n) \land \varphi_\psi \mid \text{\psi is a QBF and n = width(\varphi_{\psi})}\}$$ Now notice that if we are using matrix encoding, then the combined complexity of the MC for this logic is in $$P$$, since the extra relation $$R$$ guarantees that the size of the encoding of the model is at least $$2^n$$, and thus we can easily evaluate $$\varphi_\psi$$ in polynomial time.
On the other hand, if we are using list encoding, then we can easily reduce QBF to the MC problem of this logic, since we can construct the model in polynomial time (e.g. $$(\{0,1\},P^\mathfrak{A},R^\mathfrak{A})$$, where $$R^\mathfrak{A} = \{(1,\dots,1)\}$$, works).