Parameterized Complexity of Some Prefix-Vocabulary Fragments of First-Order Logic

Abstract

We analyze the parameterized complexity of the satisfiability problem for some prefix-vocabulary fragments of First-order Logic with the finite model property. Here we examine three natural parameters: the quantifier rank, the vocabulary size and the maximum arity of relation symbols. Following the classical classification of decidable prefix-vocabulary fragments, we will see that, for all relational classes of modest complexity and some classical classes, fixed-parameter tractability is achieved by using the above cited parameters.

Appendix

1.1 Appendix 1

We reproduce the classification and computational complexity of the classes with modest complexity without function symbols from [4, Sect. 6.4].

Table 5. Prefix-vocabulary classes of modest complexity

We summarize the results of Sect. 4 here.

Table 6. Prefix-vocabulary classes of modest complexity in which their satisfiability problem is in FPT with respect to some parameter.

1.2 Appendix 2

In this appendix, we reproduce the proofs of some theorems.

Proof

(Theorem 3) Using the same idea of Theorem 2, and the finite model property from Lemma 1(ii), we can describe an fpt-reduction from p-(qr+vs)-SAT$([\text {all}, (\omega )]_{=})$ to p-SAT.

For a satisfiable formula $\varphi \in [\text {all}, (\omega )]_{=}$ with at most $m = \text {vs}(\varphi )$ monadic relation symbols and quantifier rank $q = \text {qr}(\varphi )$, there is a model with at most $q \cdot 2^m$ elements by Lemma 1(ii). The number of steps on the conversion will be bounded by $O((q\cdot 2^m)^q \cdot n)$ where n is the formula size. Each atomic formula will be converted into a propositional variable, and this number is a function of q and m. Hence the whole process can be done in FPT.    $\square$

Proof

(Theorem 4) Let $\varphi$ be a satisfiable formula in $[\exists ^*\forall ^*, \text {all}]$ in the form $\exists x_1 \cdots \exists x_k \forall y_1 \cdots \forall y_{\ell } \psi$. By Lemma 1(iii), $\varphi$ has a model of size at most $k \le \text {qr}(\varphi )$. Then it will be necessary at most $\text {vs}(\varphi ) \cdot k^{\text {ar}(\varphi )}$ propositional variables to represent the whole structure data. Applying the propositionalization described in Theorem 2, we will produce a satisfiable propositional formula with the number of variables bounded by $g(\text {qr}(\varphi ), \text {vs}\varphi ), \text {ar}_{\varphi })$, for some computable function g. Clearly, this reduction can be done in FPT.

The same argument can be applied to the Ramsey’s class $[\exists ^*\forall ^*, \text {all}]_{=}$.    $\square$

Proof

(Theorem 5) We will consider the satisfiability problem of $[\exists ^*\forall ^2\exists ^*,\text {all}]$. Let $\varphi := \exists x_1 \cdots \exists x_k \forall y_1 \forall y_2 \exists z_1 \cdots \exists z_{\ell } \psi$ be a first-order formula in a vocabulary with $\text {vs}(\varphi )$ relation symbols of maximum arity $\text {ar}(\varphi )$. By Lemma 1(iv), there is a model of size bounded by $s := 4^{10 \cdot \text {vs}(\varphi ) \cdot \ell ^2 \cdot 2^{\text {ar}(\varphi )} \cdot (k+1)^{\text {ar}(\varphi )+4}} + k$ that satisfies $\varphi$. Considering the propositionalization, the number of propositional variables will be bounded by $\text {vs}(\varphi ) \cdot s^{\text {ar}(\varphi )}$. By structural induction on $\varphi$, apply the conversion of existential quantifiers into big disjunctions, and universal quantifiers into big conjunctions. Then it introduces one propositional variable to each possible assignment of tuples and relation symbols. This conversion is clearly a function of $s, \text {vs}(\varphi ), \text {ar}(\varphi )$ and n, the size of $\varphi$. This lead to an fpt-reduction to p-SAT.

The same argument can be applied to the Ackermann’s class $[\exists ^*\forall \exists ^*, \text {all}]$.    $\square$