# A Compendium of Parameterized Problems at Higher Levels of the Polynomial Hierarchy
## 4 Knowledge Representation and Reasoning Problems
### Disjunctive Answer Set Programming
We use the usual definition of truth of a first-order logic sentence \(\varphi\) over the vocabulary \(\tau\) in a \(\tau\)-structure \(\mathcal{A}\). We let \(\mathcal{A}\models\varphi\) denote that the sentence \(\varphi\) is true in structure \(\mathcal{A}\). \(\Sigma^{\mathsf{P}}_{2}[k*]\)-MC

_Instance:_ A first-order logic sentence \(\varphi=\exists x_{1},\ldots,x_{k}.\forall y_{1},\ldots,y_{n}.\psi\) over a vocabulary \(\tau\), where \(\psi\) is quantifier-free, and a finite \(\tau\)-structure \(\mathcal{A}\). _Parameter:_\(k\). _Question:_ Is it the case that \(\mathcal{A}\models\varphi\)? **Complexity:**\(\Sigma^{\mathsf{P}}_{2}[k*]\)-complete [41]. ### Quantified Fagin Definability

The W-hierarchy can also be defined by means of Fagin-definable parameterized problems [22], which are based on [PERSON]'s characterization of NP. We provide an additional characterization of the class \(\Pi^{\mathsf{P}}_{2}[k*]\) by means of some parameterized problems that are quantified analogues of Fagin-defined problems. Let \(\tau\) be an arbitrary vocabulary, and let \(\tau^{\prime}\subseteq\tau\) be a subvocabulary of \(\tau\). We say that a \(\tau\)-structure \(\mathcal{A}\)_extends_ a \(\tau^{\prime}\)-structure \(\mathcal{B}\) if (i) \(\mathcal{A}\) and \(\mathcal{B}\) have the same domain, and (ii) \(\mathcal{A}\) and \(\mathcal{B}\) coincide on the interpretation of all relational symbols in \(\tau^{\prime}\), i.e., \(R^{\mathcal{A}}=R^{\mathcal{B}}\) for all \(R\in\tau^{\prime}\). We say that \(\mathcal{A}\)_extends_\(\mathcal{B}\)_with weight_\(k\) if \(\sum_{R\in\tau\setminus\tau^{\prime}}|R^{\mathcal{A}}|=k\). Let \(\varphi\) be a first-order formula over \(\tau\) with a free relation variable \(X\) of arity \(s\). We let \(\Pi_{2}\) denote the class of all first-order logic formulas of the form \(\forall y_{1},\ldots,y_{n}.\exists x_{1},\ldots,x_{m}.\psi\), where \(\psi\) is quantifier-free. Let \(\varphi(X)\) be a first-order logic formula over \(\tau\), with a free relation variable \(X\) with arity \(s\). Consider the following parameterized problem. \(\Pi^{\mathsf{P}}_{2}[k*]\)-\(\mathsf{FD}^{(\tau,\tau^{\prime})}_{\varphi}\)

_Instance:_ A \(\tau^{\prime}\)-structure \(\mathcal{B}\), and an integer \(k\). _Parameter:_\(k\). _Question:_ Is it the case that for each \(\tau\)-structure \(\mathcal{A}\) extending \(\mathcal{B}\) with weight \(k\), there exists some relation \(S\subseteq A^{s}\) such that \(\mathcal{A}\models\varphi(S)\)? **Complexity:** in \(\Pi^{\mathsf{P}}_{2}[k*]\) for each \(\varphi(X)\), \(\tau^{\prime}\) and \(\tau\); \(\Pi^{\mathsf{P}}_{2}[k*]\)-hard for some \(\varphi(X)\in\Pi_{2}\), \(\tau^{\prime}\) and \(\tau\)[7]. Note that this means the following. We let \(T\) denote the set of all relational vocabularies, and for any \(\tau\in T\) we let \(\mathrm{FO}_{\tau}^{X}\) denote the set of all first-order logic formulas over the vocabulary \(\tau\) with a free relation variable \(X\). We then get the following characterization of \(\Pi_{2}^{\mathrm{P}}[k*]\)[7]:

\[\Pi_{2}^{\mathrm{P}}[k*]=[\ \{\ \Pi_{2}^{\mathrm{P}}[k*]\text{-}\mathrm{FD}_{ \varphi}^{(\tau^{\prime},\tau)}:\tau\in T,\tau^{\prime}\subseteq\tau,\varphi \in\mathrm{FO}_{\tau}^{X}\ \}\ ]^{\mathrm{fpt}}.\]

Additionally, the following parameterized problem is hard for \(\Pi_{2}^{\mathrm{P}}[*k,1]\). [style=]

\(\Pi_{2}^{\mathrm{P}}[*k]\text{-}\mathrm{FD}_{\varphi}^{(\tau,\tau^{\prime})}\)

_Instance:_ A \(\tau^{\prime}\)-structure \(\mathcal{B}\), and an integer \(k\). _Parameter:_\(k\). _Question:_ Is it the case that for each \(\tau\)-structure \(\mathcal{A}\) extending \(\mathcal{B}\), there exists some relation \(S\subseteq A^{s}\) with \(|S|=k\) such that \(\mathcal{A}\models\varphi(S)\)? **Complexity:**\(\Pi_{2}^{\mathrm{P}}[*k,1]\text{-}\mathrm{hard}\) for some \(\varphi(X)\in\Pi_{2}\)[7]. ### Symbolic Model Checking for Temporal Logics

The following problems are concerned with the task of verifying whether a temporal logic formula is true in a Kripke structure.