<p>I don't know of any natural logic, but the following is in any case a logic for which the combined complexity of the model-checking problem is different for matrix and list encodings.</p>
<p>First, we know that for every QBF formula <span class="math-container">$\psi$</span> there exists a sentence <span class="math-container">$\varphi_\psi$</span> of FO over the vocabulary <span class="math-container">$\{P\}$</span>, where <span class="math-container">$P$</span> is unary, such that <span class="math-container">$\psi$</span> is true iff <span class="math-container">$\mathfrak{A} := (\{0,1\},P^\mathfrak{A}) \models \varphi_\psi$</span>, where <span class="math-container">$P^\mathfrak{A} = \{1\}$</span>, and the sentence <span class="math-container">$\varphi_\psi$</span> can be computed from <span class="math-container">$\psi$</span> in polynomial time (it is the obvious translation). If <span class="math-container">$width(\varphi) := \max_{\theta \in Subf(\varphi)} |Free(\theta)|$</span>, then the following logic works <span class="math-container">$$\{\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})$}\}$$</span>
Now notice that if we are using matrix encoding, then the combined complexity of the MC for this logic is in <span class="math-container">$P$</span>, since the extra relation <span class="math-container">$R$</span> guarantees that the size of the encoding of the model is at least <span class="math-container">$2^n$</span>, and thus we can easily evaluate <span class="math-container">$\varphi_\psi$</span> in polynomial time.</p>
<p>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. <span class="math-container">$(\{0,1\},P^\mathfrak{A},R^\mathfrak{A})$</span>, where <span class="math-container">$R^\mathfrak{A} = \{(1,\dots,1)\}$</span>, works).</p>

CC BY-SA 4.0
2021-08-13T17:34:01.773Z
2021-09-11T09:14:54.637Z
2021-09-11T09:14:54.637Z
Reijo Jaakkola
<p>Some preliminaries first.
Consider a purely-relational structure (a.k.a. database) <span class="math-container">$\mathfrak{A} = (A, R_1^{\mathfrak{A}}, \ldots, R_{|\tau|}^{\mathfrak{A}})$</span> over some finite signature <span class="math-container">$\tau = \{ R_1, R_2, \ldots, R_{|\tau|} \}$</span>, where each relational symbol <span class="math-container">$R_i$</span> has an associated arity <span class="math-container">$\mathsf{ar}(R_i)$</span>. We assume that <span class="math-container">$A$</span> is ordered in some way, just for the sake of encodings.</p>
<p>There are two different ways to represent <span class="math-container">$\mathfrak{A}$</span> 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 <span class="math-container">$|\mathfrak{A}|$</span> as the size of its encoding.</p>
<ol>
<li>In the matrix encoding the structure <span class="math-container">$\mathfrak{A}$</span> is represented as <span class="math-container">$1^{|A|} \cdot 0 \cdot \mathsf{enc}(R_1) \cdot \mathsf{enc}(R_2) \cdot \ldots \cdot \mathsf{enc}(R_{|\tau|})$</span>, where <span class="math-container">$\mathsf{enc}(R_i)$</span> is an <span class="math-container">$|A|^{\mathsf{ar}(R_i)}$</span> bit string, with the intended meaning that its <span class="math-container">$j$</span>-th bit is 1 iff the <span class="math-container">$j$</span>-th <span class="math-container">$\mathsf{ar}(R_i)$</span>-tuple of <span class="math-container">$A$</span> belongs to <span class="math-container">$R_k^{\mathfrak{A}}$</span>.</li>
<li>In the list encoding we encode the structure <span class="math-container">$\mathfrak{A}$</span> as <span class="math-container">$1^{|A|} \cdot 0 \cdot \mathsf{enc}(R_1) \cdot \mathsf{enc}(R_2) \cdot \ldots \cdot \mathsf{enc}(R_{|\tau|})$</span>, but this time <span class="math-container">$\mathsf{enc}(R_i)$</span> just lists all the tuples included in <span class="math-container">$R_i^{\mathfrak{A}}$</span>.</li>
</ol>
<p>Hence, <span class="math-container">$|\mathfrak{A}| \approx |A| + \Sigma_{i=1}^{|\tau|} |A|^{\mathsf{ar}(R_i)}$</span> in the matrix encoding, while <span class="math-container">$|\mathfrak{A}| \approx |A| + \Sigma_{i=1}^{|\tau|}  \mathsf{ar}(R_i) \cdot |R_i^{\mathfrak{A}}|$</span> in the list encoding.
Note that the difference between the encoding is when we have a symbol <span class="math-container">$S$</span> of high-arity, let's say <span class="math-container">$n$</span> and there are only a few tuples in <span class="math-container">$S^{\mathfrak{A}}$</span>. Then in the list encoding we will have only a few tuples included, so the representation of <span class="math-container">$\mathfrak{A}$</span> will be short,  while in the matrix encoding we will store all the possible bits, no matter whether a tuple belongs to the relation <span class="math-container">$S^{\mathfrak{A}}$</span> or not. This seems to be also crucial when we have queries with negation: the relation itself can be &quot;small&quot; but its complement can be &quot;huge&quot;, but the complement is not stored directly.</p>
<p>Finally, here comes my question. Do you know any logic (or query language) <span class="math-container">$\mathcal{L}$</span> for which the combined complexity of the model-checking problem (or query evaluation problem) differs (i.e. we have <span class="math-container">$\mathfrak{A}$</span> and a formula <span class="math-container">$\varphi$</span> as an input and we ask if <span class="math-container">$\mathfrak{A} \models \varphi$</span> holds)? Of course the signature may differ for different structures. And we need to exploit negations and higher-arity relations somehow.</p>

CC BY-SA 4.0
2021-08-12T05:01:39.243Z
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.
Bartosz Bednarczyk
<complexity><db.databases><query-complexity><model-checking><finite-model-theory>
What is the impact of encodings of sparse structures on the complexity of the model checking problem?
Bartosz Bednarczyk
# What is the impact of encodings of sparse structures on the complexity of the model checking problem?

(Asked by: username_0 on 2021-08-10)

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.

**Tags:** complexity, db.databases, query-complexity, model-checking, finite-model-theory
> **Comments:**
> **username_0**: 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.  

---

## 1 answers

### Answer by username_1 on 2021-08-13. Score: 4 | Accepted answer

I don't know of any natural logic, but the following is in any case a logic for which the combined complexity of the model-checking problem is different for matrix and list encodings.

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).


---

