††thanks: ††thanks: ††thanks: ††thanks:

Preliminary version appeared in the proceedings of the WG 2017 conference
[27].

# Simplified Algorithmic Metatheorems Beyond MSO:
Treewidth and Neighborhood Diversity

Dušan Knop  Algorithmics and Computational Complexity, Faculty IV, TU Berlin,
Berlin, Germany
Faculty of Information Technology, Czech Technical University in Prague,
Prague, Czech Republic<EMAIL_ADDRESS>Martin Koutecký  Faculty of IE&M,
Technion – Israel Institute of Technology, Haifa, Israel
Computer Science Institute, Charles Univesity, Prague, Czech Republic
<EMAIL_ADDRESS>Tomáš Masařík  Department of Applied Mathematics,
Charles University, Prague, Czech Republic<EMAIL_ADDRESS>Tomáš
Toufar  Computer Science Institute, Charles University, Prague, Czech Republic
<EMAIL_ADDRESS>
###### Abstract.

This paper settles the computational complexity of model checking of several
extensions of the monadic second order (MSO) logic on two classes of graphs:
graphs of bounded treewidth and graphs of bounded neighborhood diversity.

A classical theorem of Courcelle states that any graph property definable in
MSO is decidable in linear time on graphs of bounded treewidth. Algorithmic
metatheorems like Courcelle’s serve to generalize known positive results on
various graph classes. We explore and extend three previously studied MSO
extensions: global and local cardinality constraints (CardMSO and MSO -LCC)
and optimizing the fair objective function (fairMSO).

First, we show how these extensions of MSO relate to each other in their
expressive power. Furthermore, we highlight a certain “linearity” of some of
the newly introduced extensions which turns out to play an important role.
Second, we provide parameterized algorithm for the aforementioned structural
parameters. On the side of neighborhood diversity, we show that combining the
linear variants of local and global cardinality constraints is possible while
keeping the linear (FPT) runtime but removing linearity of either makes this
impossible. Moreover, we provide a polynomial time (XP) algorithm for the most
powerful of studied extensions, i.e. the combination of global and local
constraints. Furthermore, we show a polynomial time (XP) algorithm on graphs
of bounded treewidth for the same extension. In addition, we propose a general
procedure of deriving XP algorithms on graphs on bounded treewidth via
formulation as Constraint Satisfaction Problems (CSP). This shows an alternate
approach as compared to standard dynamic programming formulations.

###### keywords:

MSO extensions, metatheorem, parameterized complexity, neighborhood diversity,
treewidth

###### 1991 Mathematics Subject Classification:

Theory of computation $\rightarrow$ Parameterized complexity and exact
algorithms; Theory of computation $\rightarrow$ Logic; Theory of computation
$\rightarrow$ Graph algorithms analysis

##  1\. Introduction

It has been known since the ’80s that various NP-hard problems are solvable in
polynomial time by dynamic programming on trees and “tree-like” graphs. This
was famously captured by Courcelle [9] in his theorem stating that any
property definable in Monadic Second Order (MSO) logic is decidable in linear
time on graphs of bounded treewidth. Subsequently, extensions to stronger
logics and optimization versions were devised [3, 11] while still keeping
linear runtime.

However, several interesting problems do not admit an MSO description and are
unlikely to be solvable in linear time on graphs of bounded treewidth due to
hardness results. In the language of parameterized complexity, Courcelle’s
theorem runs in fixed-parameter tractable (FPT) time, that is, in time
$f(|\varphi|,\tau)n^{\mathcal{O}(1)}$, where $n$ is the number of vertices of
the input graph, $\tau$ its treewidth, $\varphi$ is an MSO formula, and $f$ is
a computable function. On the other hand, the “hard” (specifically, W[1]-hard)
problems have algorithms running at best in XP time $n^{g(|\varphi|,\tau)}$,
for some computable function $g\in\omega(1)$. This led to examination of
extensions of MSO which allow greater expressive power.

Another research direction was to improve the computational complexity of
Courcelle’s theorem, since the function $f$ grows as an exponential tower in
the quantifier depth of the MSO formula. However, Frick and Grohe [18] proved
that this is unavoidable unless ${\sf P}={\sf NP}$ which raises a question: is
there a (simpler) graph class where MSO model checking can be done in single-
exponential (i.e., $2^{k^{\mathcal{O}(1)}}$) time? This was answered in the
affirmative by Lampis [31], who introduced graphs of bounded neighborhood
diversity. The classes of bounded treewidth and bounded neighborhood diversity
are incomparable: for example, paths have unbounded neighborhood diversity but
bounded treewidth, and vice versa for cliques. Bounded treewidth has become a
standard parameter with many practical applications (cf. a survey [4]);
bounded neighborhood diversity is of theoretical interest [1, 2, 6, 16, 19,
21, 35] because it can be viewed as representing the simplest of dense graphs.

Courcelle’s theorem proliferated into many fields. Originating among automata
theorists, it has since been reinterpreted in terms of finite model theory
[34], database programming [22], game theory [25] and linear programming [29].

###  1.1. Related work

For a recent survey of algorithmic metatheorems see e.g. Grohe et al. [23].

Objective functions. A linear optimization version of Courcelle’s theorem was
given by Arnborg, Lagergren and Seese [3]. An extension to further objectives
was given by Courcelle and Mosbah [11]. Kolman, Lidický and Sereni [30]
introduce MSO with a fair objective function (fairMSO) which, for a given MSO
formula $\varphi(F)$ with a free edge set variable $F$, minimizes the maximum
degree in the subgraph given by $F$, and present an XP algorithm. This is
justified by the problem being W[1]-hard, as was later shown by Masařík and
Toufar [35], who additionally give an FPT algorithm on graphs of bounded
neighborhood diversity for MSO1 and an FPT algorithm on graphs of bounded
vertex cover for MSO2. Those results were extended to graphs of bounded twin
cover by Knop, Masařík and Toufar [26].

Extended logics. Along with MSO, Courcelle also considered counting MSO (cMSO)
where predicates of the form “$|X|\equiv p\mod q$” are allowed, with the
largest modulus $q$ constant. Szeider [38] introduced MSO with local
cardinality constraints (MSO -LCC) and gave an XP algorithm deciding it on
graphs of bounded treewidth. MSO -LCC can express various problems, such as
General Factor, Equitable $r$-Coloring or Minimum Maximum Outdegree, which are
known to be W[1]-hard on graphs of bounded treewidth. Ganian and Obdržálek
[20] study CardMSO, which is incomparable with MSO -LCC in its expressive
power; they give an FPT algorithm on graphs of bounded neighborhood diversity.

###  1.2. Our contribution

The contribution of the paper is twofold. First, we survey and enrich the so
far studied extensions of MSO logic – fairMSO, CardMSO, and MSO -LCC. We do
this in Section 2.1. Second, we study the parameterized complexity of the
associated model checking problem for various combinations of these MSO
extensions. We completely settle the parameterized complexity landscape for
the model checking problems with respect to the parameters treewidth and
neighborhood diversity; for an overview of the complexity landscape refer to
Figures 1 and 2. We postpone formal definitions of logic extensions and
corresponding model checking to Subsection 2.1.

While both MSO -LCC and CardMSO express certain cardinality constraints, the
constraints of CardMSO are inherently global and linear, yet the constraints
of MSO -LCC are local and non-linear. This leads us to introduce two more
fragments and rename the aforementioned ones: CardMSO becomes ${\sf MSO}^{\sf
G}_{\sf lin}$, MSO -LCC becomes ${\sf MSO}^{\sf L}$ and we additionally have
${\sf MSO}^{\sf G}$, ${\sf MSO}^{\sf L}_{\sf lin}$, ${\sf MSO}^{\sf GL}_{\sf
lin}$ and ${\sf MSO}^{\sf GL}$. By this we give a complete landscape for all
possible combinations of types of constraints: global/local and linear/non-
linear.

In the following, we do not differentiate between the logics MSO1 (allowing
quantification over vertex sets) and MSO2 (additionally allowing
quantification over edge sets); see a detailed explanation in Subsection 2.1.
For now, it suffices to say that our positive result for graphs of bounded
treewidth holds for the appropriate extension of MSO2, while all remaining
results (positive for graphs of bounded neighborhood diversity and negative
for graphs of bounded vertex cover number) hold for the appropriate extensions
of MSO1.

For graphs of bounded treewidth we give an XP algorithm for the logic ${\sf
MSO}^{\sf GL}$, which is a composition ${\sf MSO}^{\sf G}$ and ${\sf MSO}^{\sf
L}$ and thus represents the most expressive fragment under our consideration.

###### Theorem 1

${\sf MSO}^{\sf GL}$ model checking is XP parameterized by
$\operatorname{tw}(G)$ and $|\varphi|$.

This result is also significant in its proof technique. We connect a recent
result of Kolman, Koutecký and Tiwary [29] about the polytope of satisfying
assignments with an old result of Freuder [17] about the solvability of
constraint satisfaction problem (CSP) of bounded treewidth. This allows us to
formulate the proof of Theorem 1 essentially as providing a CSP instance with
certain properties, surpassing the typical complexity of a dynamic programming
formulation. We also briefly discuss which problems can be modeled using ${\sf
MSO}^{\sf GL}$, deriving the following as a consequence:

###### Corollary 2

Let $G$ be a graph of treewidth $\tau$ and with $n=|V(G)|$.

The following problems have algorithms with runtime $n^{f(\tau)}$: General
Factor, Minimum Maximum Outdegree, Capacitated Dominating Set, Capacitated
Vertex Cover, Vector Dominating Set, Generalized Domination.

The following problems have algorithms with runtime $n^{f(\tau+k)}$:

  * •

Equitable $k$-Coloring, Equitable connected $k$-Partition, $k$-Balanced
Partitioning,

  * •

Graph Motif, where $k$ is the number of colors.

Theorem 1 is complemented from the negative side by the following hardness
result.

###### Theorem 3

${\sf MSO}^{\sf G}$ model checking is W[1]-hard parameterized by
$\operatorname{vc}(G)$ and $|\varphi|$, where $\operatorname{vc}(G)$ is the
vertex cover number of the input graph $G$.

For graphs of bounded neighborhood diversity we give two positive results; the
logic ${\sf MSO}^{\sf GL}_{\sf lin}$ is a composition of ${\sf MSO}^{\sf
L}_{\sf lin}$ and ${\sf MSO}^{\sf G}_{\sf lin}$.

###### Theorem 4

${\sf MSO}^{\sf GL}_{\sf lin}$ model checking is FPT parameterized by
$\operatorname{nd}(G)$ and $|\varphi|$.

###### Theorem 5

${\sf MSO}^{\sf GL}$ model checking is XP parameterized by
$\operatorname{nd}(G)$ and $|\varphi|$.

We complement the above results with another hardness result.

###### Theorem 6

${\sf MSO}^{\sf L}$ model checking is W[1]-hard parameterized by
$\operatorname{vc}{(G)}$.

MSO${\sf MSO}^{\sf L}_{\sf lin}$${\sf MSO}^{\sf G}_{\sf lin}$${\sf MSO}^{\sf
GL}_{\sf lin}$${\sf MSO}^{\sf L}$${\sf MSO}^{\sf G}$${\sf MSO}^{\sf GL}$

Figure 1. MSO extensions. A partial order of MSO extensions considered. An
arrow denotes generalizations; e.g., ${\sf MSO}^{\sf L}_{\sf lin}$ generalizes
MSO and is generalized by ${\sf MSO}^{\sf GL}_{\sf lin}$. Green (dashed) line
separates logics whose model checking is FPT parameterized by
$\operatorname{tw}(G)$ (Courcelle [9]) from those whose model checking is
W[1]-hard (both ${\sf MSO}^{\sf L}_{\sf lin}$ and ${\sf MSO}^{\sf G}_{\sf
lin}$ capture the W[1]-hard Equitable $r$-Coloring problem). Orange (dotted)
line separates logics whose model checking is FPT parameterized by
$\operatorname{nd}(G)$ (Theorem 4) from those whose model checking is
W[1]-hard (Theorems 3 and 6). The model checking of all logics below the red
(dashed-dotted) line is XP parameterized by both $\operatorname{tw}(G)$
(Theorem 1) and $\operatorname{nd}(G)$ (Theorem 5).

Interestingly, our finding about hardness being caused by nonlinearity carries
over to a generalization of the Set Cover problem.

Multidemand Set Multicover
Input: Universe $U=[k]$, set of multidemands $D_{1},\dots,D_{k}\subseteq[n]$,
a covering system $\mathcal{F}=\\{F_{1},\dots,F_{f}\\}\subseteq 2^{U}$, an
integer $r\in\mathbb{N}$ Task: Find integer multiplicities
$m_{1}+\dots+m_{f}=r$ such that for all $i\in[k]$, $(\sum_{j:u_{i}\in
F_{j}}m_{j})\in d_{i}$.

We show that the (non)linearity of the multidemands is crucial. On one hand,
we have the following hardness.

###### Theorem 7

Multidemand Set Multicover is W[1]-hard parameterized by $k$, already when
$|\mathcal{F}|=k$.

On the other hand, consider the Weighted Set Multicover problem. It is a
weighted variant of Multidemand Set Multicover where each multidemand $d_{i}$
is the interval $[0,\delta_{i}]$ for some $\delta_{i}\in\mathbb{N}$. Recently,
Bredereck et al. [7] showed that this variant is fixed-parameter tractable
when parameterized by $k$, which has applications in computational social
choice and elsewhere. Moreover, it is not difficult to see that even the more
general case when each $d_{i}$ is a discrete interval is in FPT, by a small
modification of the approach of Bredereck et al.

nd, vcMSO${\sf MSO}^{\sf G}_{\sf lin}$${\sf MSO}^{\sf G}$${\sf
MSO}$fairMSO${\sf MSO}^{\sf L}_{\sf lin}$${\sf MSO}^{\sf L}$FPT [31]FPT
[35]W[1]-h, Thm 6FPT [20]FPT, Thm 4W[1]-h, Thm 3XP, Thm 5

twMSO${\sf MSO}^{\sf G}_{\sf lin}$${\sf MSO}^{\sf G}$${\sf MSO}$fairMSO${\sf
MSO}^{\sf L}_{\sf lin}$${\sf MSO}^{\sf L}$FPT [9]W[1]-hard [35]XP
[38]W[1]-hard [20]XP, Thm 1

Figure 2. Complexity of various logic fragments generalizing MSO on graphs of
bounded vertex cover ($\operatorname{vc}$), neighborhood diversity
($\operatorname{nd}$) and treewidth ($\operatorname{tw}$). Positive results
(FPT, XP) spread to the left and up. W[1]-hardness spreads to the right and
down. Green background (lighter gray in b-w print) stands for FPT fragments,
while orange (darker gray) stands for W[1]-hard. A cell represents a union of
studied fragments, i.e., the cell indexed by ${\sf MSO}^{\sf G}$ and ${\sf
MSO}^{\sf L}$ corresponds to the ${\sf MSO}^{\sf GL}$ fragment.

##  2\. Preliminaries

For two integers $a,b$ we define a set $[a,b]=\\{x\in\mathbb{Z}\mid a\leq
x\leq b\\}$; we use $[b]$ to denote the set $[1,b]$. We write vectors in bold
font, i.e., $\mathbf{x}\in\mathbb{R}^{n}$, and denote by $x_{i}$, $i\in[n]$,
its $i$-th coordinate.

For a vertex $v\in V$ of a graph $G=(V,E)$, we denote by $N_{G}(v)$ the set of
neighbors of $v$ in $G$, that is, $N_{G}(v)=\left\\{u\in V\mid\\{u,v\\}\in
E\right\\}$; the subscript $G$ is omitted when clear from the context. For a
rooted tree $T$, $N_{T}(v)$ denotes the _down-neighborhood_ of $v$, i.e., the
set of descendants of $v$. For a graph $G=(V,E)$ a set $U\subseteq V$ is a
_vertex cover_ of $G$ (denoted $\operatorname{vc}(G)$) if for every edge $e\in
E$ it holds that $e\cap U\neq\emptyset$. For more graph theory notation cf.
the book of Matoušek and Nešetřil [36].

###  2.1. MSO and its Extensions

Let us shortly introduce MSO over graphs. In first-order logic (FO) we have
variables for the elements ($x,y,\ldots$), equality for variables, quantifiers
$\forall,\exists$ ranging over elements, and the standard Boolean connectives
$\neg,\land,\lor,\implies$. The _monadic second order logic_ (MSO) extends
first order logic using so called monadic variables. Graph MSO has the binary
relational symbol $\mathop{\mbox{\rm edge}}(x,y)$ encoding edges, and
traditionally comes in two flavors, MSO1 and MSO2, differing by the objects we
are allowed to quantify over: in MSO1 these are the vertices and vertex sets,
while in MSO2 we can additionally quantify over edges and edge sets. For
example, the $3$-colorability property can be expressed in MSO1 as follows:

$\displaystyle\exists X_{1},X_{2},X_{3}$ $\displaystyle\left[\,\forall
x\,(x\in X_{1}\vee x\in X_{2}\vee x\in X_{3})\wedge\right.$
$\displaystyle\bigwedge\nolimits_{i=1,2,3}\left.\\!\\!\forall
x,y\left(x\not\in X_{i}\vee y\not\in X_{i}\vee\neg\mathop{\mbox{\rm
edge}}(x,y)\right)\,\right]$

For a formula $\varphi$, we denote by $|\varphi|$ the _size_ of $\varphi$,
that is, the number of symbols in a chosen encoding of $\varphi$.

##### Regarding MSO1 and MSO2

Despite the fact that MSO2 is strictly stronger than MSO1 (hamiltonicity is
expressible in MSO2 but not in MSO1 [34]), it is known [28] that on graphs
with bounded treewidth their power is equal by an argument we shall review
below. We will show that only a small change makes the argument works even for
our extensions of MSO.

We use standard notation for relational structures (cf. Libkin [34]): a
_$\sigma$ -structure_ is a tuple
$\mathcal{A}=\bigl{(}A,\\{c_{i}\\},\\{P_{i}\\}\bigr{)}$, where the set $A$ is
the _universe_ , $\\{c_{i}\\}$ are _constant symbols_ ($c_{i}\in A$) and
$\\{P_{i}\\}$ are finitely many _relations_ , each of arity $r_{i}$
($P_{i}\subseteq A^{r_{i}}$). Then, a graph $G=(V,E)$ is typically modeled as
a $\sigma_{1}$-structure $\bigl{(}V,\emptyset,\\{E\\}\bigl{)}$. We can view
$G$ as a $\sigma_{2}$-structure ${\mathcal{A}=\bigl{(}V\cup
E,\emptyset,\\{I,L_{V},L_{E}\\}\bigr{)}}$, where $I=\\{\\{v,e\\}\mid{v\in
e},{e\in E}\\}$ is a binary relation representing incidence in $G$, and
$L_{V}$ and $L_{E}$ are unary predicates distinguishing vertices and edges;
then, every MSO2 formula about $G$ can be rewritten into an equivalent MSO1
formula about $\mathcal{A}$. The crucial observation is that the treewidth of
the structure $\mathcal{A}$ is equal to the original graph structure [28].

Let us examine this observation more closely. The structure $\mathcal{A}$ is
obtained from $G$ by subdividing every edge and labelling original vertices by
$L_{V}$ and new vertices by $L_{E}$. We shall introduce local cardinality
constraints, which require counting the number of both incident edges _and_
vertices – however, this is impossible in $\mathcal{A}$, since two vertices
$u,v$ incident in $G$ are no longer incident in $\mathcal{A}$; the global
cardinality constraints pose no problems. What we need is to reintroduce the
edge $uv$ into $\mathcal{A}$; let us call the resulting structure
$\mathcal{A}$′.

Fortunatelly, we will show this does not increase treewidth by more than one.
Observe that we can equivalently view the process obtaining $\mathcal{A}$′ as
copying each edge $e$ of $G$ and then subdividing one copy of $e$ and letting
the other as is. Then, if $(T,\mathcal{B})$ is an optimal tree decomposition
of $G$, there must exist a node $b$ with $e\subseteq B(b)$. We can subdivide
$(T,\mathcal{B})$ such that there is a distinct such node $b_{e}$ for each
edge $e$; then, for each edge $e$, we insert the vertex obtained by
subdividing $e$ into $B(b_{e})$. This increases the treewidth of
$(T,\mathcal{B})$ by one, and makes $(T,\mathcal{B})$ a tree decomposition of
$\mathcal{A}$′.

For this reason, when considering graphs of bounded treewidth, we will focus
on MSO1 formulae over $\sigma_{2}$-structures (i.e., graphs with labels
$L_{V}$ and $L_{E}$), rather than working with MSO2.

On bounded neighborhood diversity, MSO2 is strictly more powerful than MSO1;
however model checking of an MSO2 formula already over a _clique_ is not even
in XP unless $\mathsf{E}=\mathsf{NE}$ [10, 32]. Thus, here too we restrict our
attention to MSO1 and use MSO as a shortcut for MSO1 from now on.

We consider two orthogonal ways to extend MSO logic. In what follows $\varphi$
is a formula with $\ell$ free set-variables.

##### Global cardinality constraints.

We introduce a new type of atomic formulae called _global cardinality
constraints_ (_global constraints_ for short). An MSO formula with $c$ global
cardinality constraints contains $\ell$-ary predicates $R_{1},\ldots,R_{c}$
where each predicate takes as argument only the free variables of $\varphi$.
The input to the model checking problem is a graph $G=(V,E)$ on $n$ vertices
and an implicit representation (see below) of a tuple
$(R_{1}^{G},\ldots,R_{c}^{G})$, where $R_{i}^{G}\subseteq[n]^{\ell}$.

To define the semantics of the extension, it is enough to define the truth of
the newly introduced atomic formulae. A formula $R_{i}(X_{1},\ldots,X_{\ell})$
is true under an assignment $\mu\colon\\{X_{1},\ldots,X_{\ell}\\}\to 2^{V}$ if
and only if ${(|\mu(X_{1})|,\ldots,|\mu(X_{\ell})|)\in R_{i}^{G}}$. We allow a
relation $R_{i}^{G}$ to be represented either as a linear constraint
$a_{1}|X_{1}|+\cdots+a_{m}|X_{m}|\leq b$, where
$(a_{1},\dots,a_{m},b)\in\mathbb{R}^{m+1}$, or, much more generally, by an
arbitrary algorithm $\mathcal{A}(R_{i}^{G})$ such that
$\mathcal{A}(R_{i}^{G})$ decides whether $(|X_{1}|,\dots,|X_{\ell}|)\in
R_{i}^{G}$ in time $n^{\mathcal{O}(1)}$ for any tuple in $[0,n]^{\ell}$.

For example, suppose we want to satisfy a formula $\varphi(X_{1},X_{2})$ with
two sets for which $|X_{1}|\geq|X_{2}|^{2}$ holds. Then, we solve the ${\sf
MSO}^{\sf G}$ model checking problem with a formula
$\varphi^{\prime}:=\varphi\wedge[|X_{1}|\geq|X_{2}|^{2}]$, that is, we write
the relation as a part of the formula, as this is a more convenient way to
think of the problem. However, formally the relation is a part of the input,
represented by the obvious algorithm computing $|X_{2}|^{2}$, comparing it
with $|X_{1}|$, and returning the result.

##### Local cardinality constraints.

Local cardinality constraints are additional cardinality requirements such
that every variable assignment has to satisfy the cardinality constraint for
every vertex and for every free variable. Specifically, we want to control the
size of $\mu(X_{i})\cap N(v)$ for every $v$; we define a shorthand $S(v)=S\cap
N(v)$ for a subset $S\subseteq V$ and vertex $v$. _Local cardinality
constraints_ for a graph $G=(V,E)$ on $n$ vertices and a formula $\varphi$
with $\ell$ free variables are mappings $\alpha_{1},\ldots,\alpha_{\ell}$,
where each $\alpha_{i}$ is a mapping from $V$ to $2^{[n]}$.

We say that an assignment $\mu$ _obeys local cardinality constraints
$\alpha_{i},\ldots,\alpha_{\ell}$_ if for every $i\in[\ell]$ and every $v\in
V$ it holds that $|\mu(X_{i})(v)|\in\alpha_{i}(v)$.

The logic that incorporates both of these extensions is denoted ${\sf
MSO}^{\sf GL}$. Let $\varphi$ be an ${\sf MSO}^{\sf GL}$ formula with $c$
global cardinality constraints. Then the ${\sf MSO}^{\sf GL}$ model checking
problem has input:

  * •

graph $G=(V,E)$ on $n$ vertices,

  * •

relations $R_{1}^{G},\ldots,R_{c}^{G}\subseteq[n]^{\ell}$, and,

  * •

mappings $\alpha_{1},\ldots,\alpha_{\ell}$.

The task is to find an assignment $\mu$ that obeys local cardinality
constraints and such that $\varphi$ is true under $\mu$ by the semantics
defined above.

The ${\sf MSO}^{\sf GL}$ logic is very powerful and, as we later show, it does
not admit an FPT model checking algorithm neither for the parameterization by
neighborhood diversity, nor for the parameterization by treewidth. It is
therefore relevant to consider the following weakenings of the ${\sf MSO}^{\sf
GL}$ logic:

${\sf MSO}^{\sf G}$:

Only global cardinality constraints are allowed.

${\sf MSO}^{\sf L}$(originally MSO -LCC [38]):

Only local cardinality constraints are allowed.

${\sf MSO}^{\sf G}_{\sf lin}$(originally CardMSO [19]):

The cardinality constraints can only be linear; that is, we allow constraints
in the form $[e_{1}\geq e_{2}]$, where $e_{i}$ is linear expression over
$|X_{1}|,\ldots,|X_{\ell}|$.

${\sf MSO}^{\sf L}_{\sf lin}$:

Only local cardinality constraints are allowed; furthermore every local
cardinality constraint $\alpha_{i}$ must be of the form
$\alpha_{i}(v)=[l_{i}^{v},u_{i}^{v}]$, (i.e., an interval) where
$l_{i}^{v},u_{i}^{v}\in[n]$. Those constraints are referred to as _linear
local cardinality constraints_.

fairMSO:

Further restriction of ${\sf MSO}^{\sf L}_{\sf lin}$; now we only allow
$\alpha_{i}(v)=[u_{i}^{v}]$.

${\sf MSO}^{\sf GL}_{\sf lin}$:

A combination of ${\sf MSO}^{\sf L}_{\sf lin}$ and ${\sf MSO}^{\sf G}_{\sf
lin}$; both local and global constraints are allowed, but only in their linear
variants.

The model checking problem for the considered fragments is defined in a
natural way analogously to ${\sf MSO}^{\sf GL}$ model checking.

##### Pre-evaluations.

Many techniques used for designing MSO model checking algorithms fail when
applied to MSO extensions. A common workaround is first transforming the given
${\sf MSO}^{\sf GL}$ formula into an MSO formula by fixing the truth values of
all global constraints to either true or false. Once we determine which
variable assignments satisfy the transformed MSO formula, we can by other
means (e.g. integer linear programming or constraint satisfaction) ensure that
they obey the constraints imposed by fixing the values to true or false. This
approach was first used for CardMSO by Ganian and Obdržálek [20]. We formally
describe this technique as _pre-evaluations_ :

######  Definition 8 (Pre-evaluation).

Let $\varphi$ be an ${\sf MSO}^{\sf GL}$ formula. Denote by $C(\varphi)$ the
list of all global constraints. A mapping $\beta\colon
C(\varphi)\to\\{\mathtt{true},\mathtt{false}\\}$ is called a _pre-evaluation
function on $\varphi$_. The MSO formula obtained by replacing each global
constraint $c_{i}\in C(\varphi)$ by $\beta(c_{i})$ is denoted by
$\beta(\varphi)$ and is referred to as a _pre-evaluation of $\varphi$_.

######  Definition 9 (Assignment and Pre-evaluation Compliance).

A variable assignment $\mu$ of an ${\sf MSO}^{\sf GL}$ formula $\varphi$
_complies_ with a pre-evaluation function $\beta$ if every global constraint
$c_{i}\in C(\varphi)$ evaluates to $\beta(c_{i})$ under the assignment $\mu$.

###  2.2. Treewidth and Neighborhood Diversity

##### Treewidth.

For notions related to the treewidth of a graph and nice tree decompositions,
in most cases we stick to the standard terminology as given by Kloks [24]; the
only deviation is in the leaf nodes of the nice tree decomposition where we
assume that the bags are empty.

######  Definition 10 (Tree decomposition, Treewidth).

A _tree decomposition_ of a graph $G=(V,E)$ is a pair $(T,\mathcal{B})$, where
$T$ is a tree and $\mathcal{B}$ is a mapping $\mathcal{B}:V(T)\rightarrow
2^{V}$ satisfying

  * •

for any $\\{u,v\\}\in E$, there exists $a\in V(T)$ such that $u,v\in B(a)$,

  * •

if $v\in B(a)$ and $v\in B(b)$, then $v\in B(c)$ for all $c$ on the $a$-$b$
path in $T$.

We call the vertices of the tree _nodes_ and the sets $B(a)$ we call _bags_.

The treewidth $tw((T,\mathcal{B}))$ of a tree decomposition $(T,\mathcal{B})$
is the size of the largest bag of $(T,\mathcal{B})$ minus one. A graph $G$ has
treewidth $\tau$ ($\operatorname{tw}(G)=\tau$) if its smallest tree
decomposition has size $\tau$.

Observe that for every a graph $G$ we have
$\operatorname{tw}(G)\leq\operatorname{vc}(G)$, since it admits a tree
decomposition with $T$ being a path $P_{|G|-\operatorname{vc}(G)}$. In this
decomposition we have (in any order) bags of the form $U\cup\\{v\\}$ for each
vertex $v\in V\setminus U$, where $U$ is a vertex cover of $G$ with
$|U|=\operatorname{vc}(G)$. It is easy to verify that the constructed
decomposition is a tree decomposition of $G$. Thus, treewidth is a more
general structural graph parameter than vertex cover.

######  Definition 11 (Nice tree decomposition).

A _nice tree decomposition_ is a tree decomposition with $T$ rooted and
binary, where the root is denoted $r$ and each node is one of the following
types:

  * •

_Leaf node_ : a leaf $a$ of $T$ with $B(a)=\emptyset$.

  * •

_Introduce node_ : an internal node $a$ of $T$ with one child $b$ for which
$B(a)=B(b)\cup\\{v\\}$ for some $v\in B(a)$; for short we write $a=b*(v)$

  * •

_Forget node_ : an internal node $a$ of $T$ with one child $b$ for which
$B(a)=B(b)\setminus\\{v\\}$ for some $v\in B(b)$; for short $a=b\dagger(v)$

  * •

_Join node_ : an internal node $a$ with two children $b$ and $c$ with
$B(a)=B(b)=B(c)$; for short $a=\Lambda(b,c)$.

For a vertex $v\in V$, we denote by $top(v)$ the topmost node of a nice tree
decomposition that contains $v$ in its bag. For any graph $G$ on $n$ vertices,
a nice tree decomposition of $G$ with at most $8n$ nodes can be computed in
time $\mathcal{O}(n)$ [5, 24].

Given a graph $G=(V,E)$ and a subset of vertices
$V^{\prime}=\\{v_{1},\dots,v_{d}\\}\subseteq V$, we denote by $G[V^{\prime}]$
the subgraph of $G$ induced by $V^{\prime}$. Given a tree decomposition
$(T,\mathcal{B})$ and a node $a\in V(T)$, we denote by $T_{a}$ the subtree of
$T$ rooted in $a$, and by $G_{a}$ the subgraph of $G$ induced by all vertices
in bags of $T_{a}$, that is, $G_{a}=G[\bigcup_{b\in V(T_{a})}B(b)]$.

##### Neighborhood diversity.

We say that two (distinct) vertices $u,v$ are of the same neighborhood type if
they share their respective neighborhoods, that is when
${N(u)\setminus\\{v\\}=N(v)\setminus\\{u\\}}.$ Let $G=(V,E)$ be a graph. We
call a partition of vertices $\mathcal{T}=\\{T_{1},\dots,T_{\nu}\\}$ a
neighborhood decomposition if, for every $i\in[\nu]$, all vertices of $T_{i}$
are of one neighborhood type.

######  Definition 12 (Neighborhood diversity [31]).

A graph $G=(V,E)$ has neighborhood diversity $\nu$
($\operatorname{nd}(G)=\nu$) if its unique minimal neighborhood decomposition
is of size $\nu$. Moreover, this decomposition can be computed in linear time.

We call the sets $T_{1},\dots,T_{\nu}$ types. Note that every type induces
either a clique or an independent set in $G$ and two types are either joined
by a complete bipartite graph or no edge between vertices of the two types is
present in $G.$ Thus, we introduce the notion of a _type graph_
$T_{\mathcal{T}}(G)$. The vertices of $T_{\mathcal{T}}(G)$ are the types
$T_{1},\dots,T_{\nu}$ and two types $T_{i},T_{j}$ are joined by an edge if
$T_{i}$ and $T_{j}$ are joined by a complete bipartite graph in $G$. If the
decomposition $\mathcal{T}$ is clear from the context, we omit the subscript
$\mathcal{T}$.

Observe that for every a graph $G=(V,E)$ we have $\operatorname{nd}(G)\leq
2^{\operatorname{vc}(G)}+\operatorname{vc}$. Indeed, we can construct a
decomposition $\mathcal{T}$ witnessing this as follows. Let $U$ be the vertex
cover of $G$ with $|U|=\operatorname{vc}(G)$. We put singleton $\\{u\\}$ to
$\mathcal{T}$ for every $u\in U$ and then we add sets $\\{v\in V\setminus
U\mid N_{G}(v)=X\\}$ to $\mathcal{T}$ for every $X\subseteq U$. It is easy to
verify that $\mathcal{T}$ is a neighborhood decomposition of $G$. Thus,
neighborhood diversity is a more general structural graph parameter than
vertex cover, since the class of cliques has neighborhood diversity 1 while
unbounded size vertex cover.

##  3\. Graphs of Bounded Neighborhood Diversity

For graphs of bounded neighborhood diversity we prove two negative results
(Theorems 3 and 6) and two positive results (Theorems 4 and 5).

###  3.1. Theorems 3 and 6: W[1]-hardness of ${\sf MSO}^{\sf L}$ and ${\sf
MSO}^{\sf G}$

We begin with a definition of an auxiliary problem:

Local Cardinality Constrained Subset (LCC Subset) Input: Graph ${G=(V,E)}$
with $|V|=n$ and a function ${f\colon V\to 2^{[0,n-1]}}$. Task: Find a set
${U\subseteq V}$ such that ${|U(v)|\in f(v)}$ for each vertex ${v\in V}$.

Obviously LCC Subset is equivalent to ${\sf MSO}^{\sf L}$ with an empty
formula $\varphi$. We call an LCC Subset instance uniform if, on $G$ with
decomposition $\mathcal{T}$, the demand function $f$ can be written as
$f\colon\mathcal{T}\rightarrow 2^{[0,n-1]}$, that is, the vertices of the same
type have the same demand set. We show that already uniform LCC Subset is
W[1]-hard by a reduction from the W[1]-hard $k$-Multicolored Clique problem
[12].

$k$-Multicolored Clique Parameter: $k$ Input: $k$-partite graph
$G=(V_{1}\dot{\cup}\cdots\dot{\cup}V_{k},E)$, where $V_{a}$ is an independent
set for every $a\in[k]$. Task: Find a clique of size $k$.

We refer to a set $V_{a}$ as to a colorclass of $G$. Our proof is actually a
simplified proof of W[1]-hardness for the Target Set Selection problem [13].

###### Theorem 13

LCC Subset is W[1]-hard parameterized by the vertex cover number already in
the case when $f(v)=\\{0\\}$ for all $v$ not belonging to the vertex cover.

###### Proof.

Let $G=(V_{1}\cup\cdots\cup V_{k},E)$ the instance graph for $k$-Multicolored
Clique. We naturally split the set of edges $E$ into sets $E_{\\{a,b\\}}$ by
which we denote the edges between colorclasses $V_{a}$ and $V_{b}$. We may
assume that all of the colorclasses are of the same size which we denote $n$,
and similarly for the number of edges between any two colorclasses which we
denote $m$. Fix $N>n$, say $N=n^{2}$, and distinct $a,b\in[k]$.

##### Description of the reduction.

We numerate vertices in each color class $V_{a}$ for $a\in[k]$ using numbers
in $[n]$, that is, we fix a bijection $\mu_{a}\colon V_{a}\to[n]$ for each
$a\in[k]$. We also numerate the edges between color classes $a$ and $b$ by
numbers in $[m]$. Let $\varepsilon_{\\{a,b\\}}\colon E_{\\{a,b\\}}\to[m]$ be
the numeration function for distinct $a,b\in[k]$. We set

$I_{ab}=\bigl{\\{}\mu_{a}(v)+N\cdot\varepsilon_{\\{a,b\\}}(e)\mid v\in e,e\in
E_{\\{a,b\\}}\bigl{\\}}\,.$

We build the graph using the following groups of vertices (refer to Figure 3):

  * •

an independent set $S_{a}$ of size $n$ for each color class $V_{a}$ and set
$f(v)=\\{0\\}$ for every $v\in S_{a}$,

  * •

an independent set ${T_{\\{a,b\\}}}$ of size $mN$ for each edge set
${E_{\\{a,b\\}}}$, with $f(v)={\\{0\\}}$ for every $v\in{T_{\\{a,b\\}}}$,

  * •

a single vertex Mult{a,b} with $f(\textrm{Mult}_{\\{a,b\\}})={\\{tN\mid
t\in[m]\\}}$, and

  * •

a single vertex Incab with $f(\textrm{Inc}_{ab})={I_{ab}}$.

Finally, we add complete bipartite graphs between ${S_{a}}$ and Incab, between
Incab and ${T_{\\{a,b\\}}}$, and between ${T_{\\{a,b\\}}}$ and Mult{a,b}. Let
$H$ denote the resulting graph. It is straightforward to check that the
vertices Mult{a,b} together with vertices Inc${}_{{}_{ab}}$ form a vertex
cover of $H$. It follows that $\operatorname{vc}{(H)}=\binom{k}{2}+k(k-1)$.
For an overview of the reduction please refer to Figure 3.

Correctness of the reduction. Suppose there is a clique of size $k$ in $G$
with vertex set $\\{v_{1},\ldots,v_{k}\\}$. We assume that $v_{i}\in V_{i}$
for all $i\in[k]$. We select $\mu_{a}(v_{a})$ vertices in the set $S_{a}$ and
$N\cdot\varepsilon_{\\{a,b\\}}(\\{v_{a},v_{b}\\})$ vertices in the set
$T_{\\{a,b\\}}$ for all distinct $a,b\in[k]$. It is straightforward to check
that this is a solution respecting the demands in $H$.

Suppose there is a solution $U$ respecting demands in $H$. First note that
none of vertices Mult{a,b}, Incab is selected as their neighborhood demands
are set to $0$. Denote $s_{a}=|U\cap S_{a}|$ and
$t_{\\{a,b\\}}=|T_{\\{a,b\\}}\cap U|$. Now observe that since the demand of
vertex Mult{a,b} is fulfilled, there are $t_{\\{a,b\\}}=tN$ vertices for some
$t\in[m]$. Let $e_{ab}$ denote the edge in $E_{\\{a,b\\}}$ with numeration
$\varepsilon_{\\{a,b\\}}(e_{ab})=t$ for each distinct $a,b\in[k]$. Let $v_{a}$
denote the vertex in $V_{a}$ with numeration $\mu_{a}(v_{a})=s_{a}$ for every
$a\in[k]$. Since the demand of vertex Incab is fulfilled, it follows that the
vertex $v_{a}$ must be incident to the edge $e_{ab}$. Symmetrically, since the
demand for the vertex Incba is fulfilled, we get that the vertex $v_{b}$ is
incident to the edge $e_{ab}$. Combining all of these together we infer that
$\\{v_{1},\ldots,v_{k}\\}$ defined in this way form a clique in the graph $G$.
This concludes the proof. ∎

$n$$S_{a}$$0$$1$Incab$I_{ab}$$mN$$T_{\\{a,b\\}}$$0$$1$Mult{a,b}$\\{tN\mid
t\in[m]\\}$ Figure 3. An overview of the decomposition of a gadget used in the
proof of Theorem 13. Numbers inside nodes denote the number of vertices in the
independent set represented by the node. Below each node a description of the
respective set of admissible numbers is shown.

Note that Theorem 6 follows easily from Theorem 13 since the LCC Subset
problem is expressed by a an empty ${\sf MSO}^{\sf L}_{\sf lin}$ formula.

As we mentioned in the introduction, our hardness result has consequences for
the hardness of the Multideand Set Multicover problem.

###### Proof of Theorem 7.

Given a uniform instance of LCC Subset on a graph $G$ with
$\operatorname{nd}(G)=\nu$ with every type being an independent set, let
$U=[\nu]$, $\mathcal{F}=\\{N(v)\mid\forall v\in T(G)\\}$ and let $d_{i}=f(i)$.
Then if there exists an $r\in[n]$ such that
$(U,\mathcal{F},(d_{1},\dots,d_{\nu}),r)$ is a Yes instance of Multidemand Set
Multicover, the given LCC Subset instance is a Yes instance, and otherwise it
is a No instance. ∎

Having showed the hardness of ${\sf MSO}^{\sf L}$ parameterized by
$\operatorname{nd}(G)$, let us now turn our attention to the proof of Theorem
3, i.e., hardness of ${\sf MSO}^{\sf G}$ parameterized by
$\operatorname{nd}(G)$.

###### Proof of Theorem 3.

Let $(G=(V,E),f,k)$ be an instance of the LCC Subset problem parameterized by
the vertex cover number resulting from Theorem 13. Let $C\subseteq V$ be the
vertex cover in $G$. Note that it follows from the proof of Theorem 13 that we
may assume that the independent set $V\setminus C$ is divided into
$\mathcal{O}(k)$ groups, where each group shares the neighborhood in $C$.
Observe further that indeed the graph $G$ is bipartite (i.e., the set $C$ is
also an independent set), in particular, the largest clique subgraph of $G$ is
of size 2.

By Theorem 13 we know that it is W[1]-hard to find a subset $X\subseteq
V\setminus C$ such that $|X(v)|\in f(v)$ for all $v\in C$. Our goal now is to
build an ${\sf MSO}^{\sf G}$ formula expressing exactly this.

First we take $G$ and construct a graph $G^{\prime}$ by, for each $v\in C$,
attaching a $K_{2+\eta(v)}$ to $N(v)$, where $\eta\colon C\to[k]$ is a
bijective mapping. We will call the clique $K_{2+\eta(v)}$ a marker because it
will allow us to recognize exactly the vertices of $N(v)$. Note that markers
are the only cliques present in $G^{\prime}$ of size at least 3. Note further
that by this we have added $\mathcal{O}(k)$ cliques of size $\mathcal{O}(k)$
and thus the resulting graph has vertex cover of size $\mathcal{O}(k^{2})$.

Let us describe some auxiliary formulae which we then use to define the
desired formula $\varphi$. We reserve $X$ for the set that will represent the
set $X$ from the LCC Subset problem.

  * •

$Z$ is a clique:

$\displaystyle\qquad\qquad\texttt{clique}(Z):=(\forall x,y\in Z)(x\neq
y\implies xy\in E)$

  * •

$u$ and $v$ are of the same neighborhood type:

$\displaystyle\qquad\qquad\texttt{same}(u,v):=(\forall w\in V)(w=u\lor
w=v\lor(wu\in E\iff wv\in E))$

  * •

$Z$ is a type:

$\displaystyle\qquad\qquad\texttt{type}(Z):=(Z\neq\emptyset)\land(\forall
u,v\in Z)(\texttt{same}(u,v))\land(\forall u\in Z,v\notin
Z)(\lnot\texttt{same}(u,v))$

  * •

$Z$ is $\eta(v)$-th marker:

$\displaystyle\qquad\qquad\texttt{marker}_{v}(Z):=(|Z|=2+\eta(v))\land\texttt{clique}(Z)\land\texttt{type}(Z)$

  * •

$Z$ is $N(v)$:

$\displaystyle\qquad\qquad\texttt{neigh}_{v}(Z):=\texttt{type}(Z)\land(\exists
Q\subseteq V)(\texttt{marker}_{v}(Q)\land(\forall u\in Z,w\in Q)(uw\in E))$

  * •

$Z$ is exactly $X_{v}$:

$\displaystyle\qquad\qquad\texttt{sel-neigh}_{v}(Z,X):=(\exists
Z_{v})(\texttt{neigh}_{v}(Z_{v})\land Z=Z_{v}\cap X)$

Now $\varphi(X,(X_{v})_{v\in C}):=\bigwedge_{v\in C}\bigl{(}\texttt{sel-
neigh}_{v}(X_{v},X)\land|X_{v}|\in f(v)\bigr{)}.$ ∎

###  3.2. Theorem 4: FPT algorithm for ${\sf MSO}^{\sf GL}_{\sf lin}$ on
neighborhood diversity

Essentially, we are modifying the algorithm of Ganian and Obdržálek [20] for
${\sf MSO}^{\sf G}_{\sf lin}$ model checking so that it can deal with the
additional constraints introduced by ${\sf MSO}^{\sf L}_{\sf lin}$. We use
integer linear programming (ILP). By the result of Lenstra [33] ILP can be
solved in FPT-time parameterized by the number of integral variables.

####  3.2.1. Signatures and Shapes

Before we move on to proving Theorem 4 we first need to introduce some
notation.

######  Definition 14.

Let $\varphi$ be an ${\sf MSO}^{\sf G}_{\sf lin}$ formula with free set
variables $X_{1},\ldots,X_{\ell}$, let $G=(V,E)$ be a graph with
$\operatorname{nd}(G)=\nu$ and types $T_{1},\ldots,T_{\nu}$, and let
$\mu\colon\\{X_{1},\ldots,X_{\ell}\\}\to 2^{V}$ be a variable assignment. The
_signature of $\mu$_ is a mapping from $S_{\mu}\colon[\nu]\times
2^{[\ell]}\to\mathbb{N}$ defined by

$S_{\mu}(j,I)=\left|\bigcap_{i\in I}\mu(X_{i})\cap T_{j}\right|.$

Clearly, if we have two variable assignments $\mu,\mu^{\prime}$ with the same
signature, then $G,\mu\models\varphi$ if and only if
$G,\mu^{\prime}\models\varphi$.

However, for MSO formulae and graphs of bounded neighborhood diversity, much
more is true. Informally speaking, the formula cannot distinguish between two
cardinalities if both of them are large. This is formally stated in the next
lemma, which is a direct consequence of [31, Lemma 5]:

###### Lemma 15

Let $\varphi$ be an ${\sf MSO}$ formula with free set variables
$X_{1},\ldots,X_{\ell}$ that has $q_{S}$ set quantifiers and $q_{e}$ element
quantifiers. Let $G$ be a graph with $\operatorname{nd}(G)=\nu$. Denote by $t$
the number $2^{q_{S}}\cdot q_{e}$. Suppose that $\mu,\mu^{\prime}$ are two
variable assignments such that for every $I\subseteq[\ell]$, $j\in[\nu]$ we
have either

  * •

$S_{\mu}(j,I)=S_{\mu^{\prime}}(j,I)$, or

  * •

both $S_{\mu}(j,I),S_{\mu^{\prime}}(j,I)>t$.

Then $G,\mu\models\varphi$ if and only if $G,\mu^{\prime}\models\varphi$.

The last lemma leads to the following definition.

######  Definition 16 (Shape).

Let $\varphi$, $G$ and $t$ be as before. A _shape_ of a variable assignment
$\mu$ is a mapping $sh_{\mu}\colon[\nu]\times
2^{[\ell]}\to[0,t]\cup\\{\mathord{\uparrow}\\}$ defined by

$sh_{\mu}(j,I)=\begin{cases}S_{\mu}(j,I)&\text{ if $S_{\mu}(j,I)\leq t$}\\\
\mathord{\uparrow}&\text{ if $S_{\mu}(j,I)>t$}\\\ \end{cases}$

Since $t$ depends only on the formula $\varphi$, the total number of shapes
can be bounded by some function of $|\varphi|$ and $\operatorname{nd}(G)$.
Note that there are mappings from $[\nu]\times 2^{[\ell]}$ to
$[0,t]\cup\\{\mathord{\uparrow}\\}$ that do not correspond to shape of any
variable assignment $\mu$ for a particular graph $G$. For example, if
$sh(j,I)=\mathord{\uparrow}$ for some $j$ and $I$ but $|T_{j}|<t$, clearly
there is no assignment of shape $sh$.

However, Lemma 15 cannot be used directly, as the global linear constraints
allow us to distinguish small differences in cardinalities, even if the
cardinalities are large; consider for example the constraint
$\left[|X_{1}|=|X_{2}|+1\right]$. We use the approach outlined in Subsection
2.1, Pre-evaluations. This approach relies on Definitions 8 and 9. We simply
guess all possible outcomes of the cardinality constraints (the number of such
outcomes is clearly bounded by $2^{|\varphi|}$) and later ensure that our
assignment obeys those constraints by an Integer Linear Program.

######  Definition 17.

A shape $sh$ is _admissible_ with respect to a pre-evaluation $\beta$ if for
any variable assignment $\mu$ of the shape $sh$ we have
$G,\mu\models\beta(\varphi)$.

####  3.2.2. Unifying Local Linear Constraints

Here we show how to change the local linear constraints and the neighborhood
diversity decomposition in a way such that

  * •

the new instance is equivalent to the former one,

  * •

the size of the new decomposition is bounded in terms of
$\operatorname{nd}(G)$ and $|\varphi|$

  * •

vertices of the same type also have exactly the same local linear constraints.

This, in turn, allows us to prove the main theorem in a much simpler setting.

Let $G$ be a graph $G$ and $\mathcal{T}$ its neighborhood diversity
decomposition. A type $T\in\mathcal{T}$ is said to be _nonuniform_ with
respect to local linear cardinality constraints $\alpha$ if there exist
vertices $u,v\in T$ with $\alpha(u)\neq\alpha(v)$, otherwise $T$ is said to be
_uniform_. As already mentioned, the purpose of this section is to alter the
given instance into an equivalent uniform one. In order to to be able to do so
we have to change the neighborhood diversity decomposition (i.e., the type
graph). A neighborhood diversity decomposition $\hat{\mathcal{T}}$ is a
_refinement_ of $\mathcal{T}$ if for every $\hat{T}\in\hat{\mathcal{T}}$ there
exists a type $T\in\mathcal{T}$ such that $\hat{T}\subseteq T$. We define
$\nu_{\alpha}(\mathcal{T})$ as the number of nonuniform types in $\mathcal{T}$
with respect to $\alpha$.

###### Proposition 18

Let $G=(V,E)$ be a graph and let $\mathcal{T}$ be a neighborhood diversity
decomposition. For every $T\in\mathcal{T}$ and for every $X\subseteq V$ there
exists a nonnegative integer $z$ such that for every vertex $w\in T$

  * •

it holds that $|X(w)|=z$ if $T$ is an independent set and

  * •

it holds that $|X(w)|\in\\{z,z+1\\}$ if $T$ is a clique.

###### Proof.

First assume that $T$ is an independent set, then $N(v)=N(w)$ for all $v,w\in
T$.

For the second case assume that $T$ is a clique and let
$M=N(v)\setminus\\{w\\}$. Now $N(v)=M\cup\\{w\\}$ and $N(w)=M\cup\\{v\\}$ and
as the number $|M\cap X|$ contributes to both $v$ and $w$,
$\big{|}|X(v)|-|X(w)|\big{|}\leq 1$ must hold. ∎

Now we show how to refine the neighborhood diversity decomposition with
respect to one local linear cardinality constraint.

###### Lemma 19

Given a graph $G=(V,E)$, neighborhood diversity decomposition $\mathcal{T}$ of
$G$, and local linear cardinality constraints $\alpha$. Let $T\in\mathcal{T}$
be a nonuniform type of $G$. There exists partition $\mathcal{T}^{\prime}$ of
$T$ and local linear cardinality constraints $\alpha^{\prime}$ such that the
following holds

  1. (1)

$|\mathcal{T}^{\prime}|\leq 4$,

  2. (2)

$\nu_{\alpha^{\prime}}((\mathcal{T}\setminus\\{T\\})\cup\mathcal{T}^{\prime})<\nu_{\alpha}(\mathcal{T})$,
and

  3. (3)

for each $X\subseteq V$, $X$ satisfies $\alpha$ if and only if $X$ satisfies
$\alpha^{\prime}$.

###### Proof.

Let us first argue about an independent type $T$. In this case it suffices to
set $\alpha^{\prime}(u)=\bigcap_{v\in T}\alpha(v)$ for each $u\in T$. Now
$X\subseteq V$ satisfies $\alpha$ if and only if $X$ satisfies
$\alpha^{\prime}$ as the value $|N(T)\cap X|$ has to be the same for all
vertices of $T$ and thus has to be in $\alpha^{\prime}(v)$ for $v\in T$ by
Proposition 18.

Let $T$ be a clique type of $\mathcal{T}$. We define

l $\displaystyle=\max_{v\in T}\min\alpha(v)\,,\text{and}$ (1) u
$\displaystyle=\min_{v\in T}\max\alpha(v)\enspace.$ (2)

If $\texttt{u}\leq\texttt{l}-2$, then $\alpha$ cannot be satisfied by
Proposition 18. Denote the new local linear constraints
$\alpha^{\prime}(v)=\alpha(v)\cap[\texttt{l}-1,\texttt{u}+1]$ for $v\in T$ and
define $\alpha^{\prime}(v)=\alpha(v)$ for $v\in V\setminus T$. We get that:

  * •

$\alpha^{\prime}(v)\subseteq[\texttt{l}-1,\texttt{u}+1]$ for each $v\in T$ and

  * •

$[\texttt{l},\texttt{u}]\subseteq\alpha^{\prime}(v)$ for each $v\in T$.

This yields at most $4$ possibilities for $\alpha^{\prime}(v)$. We can refine
$T$ into at most $4$ subtypes such that all the vertices of a subtype of $T$
have the same $\alpha^{\prime}(v)$. As all newly introduced types are uniform
we have replaced a nonuniform type $T$ with at most $4$ uniform types. We have
proven (1) and (2); in order to prove (3) we use the following claim.

Clearly, all subtypes are uniform with respect to $\alpha^{\prime}$ and for
each $X\subseteq V$ it holds that if $X$ satisfies $\alpha^{\prime}$ than $X$
satisfies $\alpha$, since $\alpha^{\prime}(v)\subseteq\alpha(v)$ for every
vertex $v$.

###### Claim 20

Let $p\in[n]$ and let l be defined as in (1). If there exists $v\in T$ such
that the following conditions are fulfilled

  * •

$p\in\alpha(v)$ and

  * •

$p\leq\texttt{l}-2$.

For each $X$ satisfying $\alpha$ it holds that $p\neq|X(v)|$.

###### Proof.

Let $z$ be as in Proposition 18, that is, each $w\in T$ must have $z$ or $z+1$
in $\alpha(w)$. Suppose for contradiction that $|X(v)|=p$ and let $s$ be a
vertex with $\alpha(s)\subseteq\\{\texttt{l},\ldots\\}$ (such $s$ exists from
the definition of l). As $p\leq\texttt{l}-2$ it follows that $X$ cannot
satisfy $\alpha(s)$. There are two possible options $\\{p-1,p\\}$ and
$\\{p,p+1\\}$ from Proposition 18. Observe that
$\\{p-1,p,p+1\\}\cap\alpha(s)=\emptyset$. This finishes the proof of the
claim. ∎

Let $X\subseteq V$ satisfy $\alpha$ otherwise there is nothing to prove. By
the above claim and its symmetric version for $p\geq\texttt{u}+2$ it follows
that $\texttt{l}-1\leq X(v)\leq\texttt{u}+1$. By the definition of
$\alpha^{\prime}$ it follows that $X$ satisfies $\alpha^{\prime}$. ∎

We now apply the above lemma to all local cardinality constraints in the given
instance.

###### Lemma 21

Given a graph $G=(V,E)$ with $\operatorname{nd}(G)=\nu$ and with local linear
cardinality constraints $\alpha_{i}$ for each $i\in[\ell]$, there exists a
neighborhood decomposition $\mathcal{T}$ of $G$ of size at most $\nu 4^{\ell}$
and local linear cardinality constraints $\alpha^{\prime}_{i}$ for each
$i\in[\ell]$ such that:

  * •

the constraints $\alpha^{\prime}_{i}$, for all $i\in[\ell]$, are uniform with
respect to $\mathcal{T}$, and,

  * •

for each $(X_{1},\dots,X_{\ell})\subseteq V^{\ell}$, $X_{i}$ satisfies
$\alpha_{i}$ for all $i\in[\ell]$ if and only if $X_{i}$ satisfies
$\alpha^{\prime}_{i}$ for all $i\in[\ell]$.

###### Proof.

The proof goes by repeatedly applying Lemma 19. We start with the neighborhood
decomposition $\mathcal{T}$ of size $\nu$ that is guaranteed by
$\operatorname{nd}(G)=\nu$, and with the local linear cardinality constraints
$\alpha_{i}$.

First let $i=1$, and go sequentially over the types $T_{1},\dots,T_{\nu}$.
Apply Lemma 19 to the presently processed type $T_{j}$ and the local linear
cardinality constraint $\alpha^{\prime}_{1}$ and decomposition
$\mathcal{T}^{\prime}$ resulting from the previous application of the lemma,
using $\alpha_{1}$ and $\mathcal{T}$ in the beginning. Clearly, after we are
done we have a neighborhood decomposition $\mathcal{T}^{\prime}$ of size at
most $4\nu$ and local linear cardinality constraints $\alpha^{\prime}_{1}$
which are uniform with respect to $\mathcal{T}^{\prime}$.

Then, continuing with $i\in[2,\ell]$, we do the same, finally resulting in a
decomposition $\mathcal{T}^{\prime\prime}$ of size $\nu 4^{\ell}$ and local
linear cardinality constraints
$\alpha^{\prime\prime}_{1},\dots,\alpha^{\prime\prime}_{\ell}$ which are
uniform with respect to $\mathcal{T}^{\prime\prime}$, as desired. ∎

##### Uniform Instance

Let $G$ be a graph and let $\alpha_{i}$ for $i\in[\ell]$ be a collection of
local cardinality constraints. For a given neighborhood diversity
decomposition $\mathcal{T}$ we say that $\alpha_{i}$ are _uniform_ if
$\nu_{\alpha_{i}}(T)=0$ for all $T\in\mathcal{T}$ and $i\in[\ell]$.

####  3.2.3. Uniform Instance Theorem

###### Theorem 22

There exists an algorithm that, given an ${\sf MSO}^{\sf GL}_{\sf lin}$
formula $\varphi$ with free set variables $X_{1},\ldots,X_{\ell}$, a graph
$G=(V,E)$ with neighborhood diversity decomposition $\mathcal{T}$, and uniform
local linear constraints $\alpha_{i}(v)$, outputs an assignment $\mu$ such
that $G,\mu\models\varphi$ and $|\mu(X_{i})(v)|\in\alpha_{i}(v)$ for every
$v\in V$ and every $i\in[\ell]$. The algorithm terminates in time
$f(|\varphi|,\nu)n^{\mathcal{O}(1)}$ for some computable function $f$.

###### Proof.

Let $\nu$ denote the size of $\mathcal{T}$.

The algorithm runs as follows. For every pre-evaluation function $\beta$ and
every mapping $sh\colon[\nu]\times
2^{[\ell]}\to[0,t]\cup\\{\mathord{\uparrow}\\}$, we test whether $sh$ is
admissible. This can be done by picking an arbitrary variable assignment $\mu$
of shape $sh$ (if there exists such an assignment) and testing whether
$G,\mu\models\beta(\varphi)$ by an FPT model checking algorithm for MSO
formulae [31].

If the shape $sh$ is admissible with respect to $\beta$, we need to find a
variable assignment $\mu$ such that

  * •

$\mu$ complies with $\beta$,

  * •

$\mu$ has shape $sh$, and

  * •

$\mu$ satisfies the local linear constraints.

This is done by the following integer linear program. We begin the description
of the integer linear program with a description of all its variables:

  * •

for every $I\subseteq[\ell],j\in[\nu]$, we introduce an integer variable
$x_{I}^{j}$ (these correspond to $S_{\mu}(j,I)$ of the variable assignment
$\mu$ we are about to find),

  * •

for every $i\in[\ell]$, $j\in[\nu]$, we introduce an auxiliary variable
$y_{i}^{j}$ corresponding to $|\mu(X_{i})|\cap T_{j}|$, and

  * •

for every $i\in[\ell]$, we add an auxiliary variable $z_{i}$ corresponding to
$|\mu(X_{i})$ (technically variables $y_{i}^{j}$ and $z_{i}$ are redundant as
they are projections of the $x$ variables, but they will simplify the
presentation).

We note that all auxiliary variables can be assumed to be integral without
contributing to the number of integral variables. To ensure that $\mu$ has the
required properties, we add these constraints:

$\displaystyle\sum_{I\subseteq[\ell]}x_{I}^{j}$ $\displaystyle=|T_{j}|$ for
every $j\in[\nu]$ (0) $\displaystyle y_{i}^{j}$
$\displaystyle=\sum_{\scriptstyle{I\subseteq[\ell]:}\atop\scriptstyle{i\in
I}}x_{I}^{j}$ for every $j\in[\nu]$ and every $i\in[\ell]$ (a1) $\displaystyle
z_{i}$ $\displaystyle=\sum_{j=1}^{\nu}y_{i}^{j}$ for every $i\in[\ell]$ (a2)
$\displaystyle x_{I}^{j}$ $\displaystyle=sh(I,j)$ for every
$j\in[\nu],I\subseteq[\ell]$ such that $sh(I,j)\neq\mathord{\uparrow}$ (sh1)
$\displaystyle x_{I}^{j}$ $\displaystyle>t$ for every
$j\in[\nu],I\subseteq[\ell]$ such that $sh(I,j)=\mathord{\uparrow}$ (sh2)

The constraints ( ‣ 3.2.3) ensure that variables $x_{I}^{j}$ encode a variable
assignment for the graph $G$. The constraints (a1) and (a2) set auxiliary
variables $y_{i}^{j}$ and $z_{i}$ to the desired values. The constraints (sh1)
and (sh2) guarantee that $\mu$ has the shape $sh$.

We for convenience denote the $i$-th linear cardinality constraint for type
$T_{j}$ by $\alpha_{i,j}$ and furthermore we set
$\mathrm{lb}^{i}_{j}:=\min\alpha_{i,j}$ and
$\mathrm{ub}^{i}_{j}:=\max\alpha_{i,j}$.

If $T_{j}$ is an independent type, we need to ensure that for every $v\in
T_{j}$ we have $|\mu(X_{i})(v)|\in\alpha_{i,j}(v)$. It is easy to see that the
quantity $|\mu(X_{i})(v)|$ is the same for every $v\in T_{j}$ and it can be
expressed as

$\sum_{j^{\prime}:\\{j^{\prime},j\\}\in E(T_{G})}\left|\mu(X_{i})\cap
T_{j^{\prime}}\right|\,.$

By the definition of auxiliary variables $y_{I}^{j}$, we have $|\mu(X_{i})\cap
T_{j^{\prime}}|=y_{i}^{j^{\prime}}$, so the local linear condition for the
variable $X_{i}$ can be rewritten as

$\mathrm{lb}^{i}_{j}\leq\sum_{j^{\prime}:\\{j^{\prime},j\\}\in
E(T_{G})}y_{i}^{j}\leq\mathrm{ub}^{i}_{j}\,.$ (lli)

If $T_{j}$ is a clique type, we have to be slightly more careful, since the
quantity $|\mu(X_{i})(v)|$ depends on whether $v$ lies in $\mu(X_{i})$ or not.
The set $N(v)$ does not include $v$ itself, so if
$|\mu(X_{i})(v^{\prime})|=|\mu(X_{i})(v)|+1$ for every $v\in
T_{j}\cap\mu(X_{i})$, then $v^{\prime}\in T_{j}\setminus\mu(X_{i})$. Similarly
as before, we have equations

$|\mu(X_{i})(v)|=\left(\sum_{j^{\prime}:\\{j^{\prime},j\\}\in
E(T_{G})}\left|\mu(X_{i})\cap T_{j^{\prime}}\right|\right)-1$

for $v\in T_{j}\cap\mu(X_{i})$, and

$\left|\mu(X_{i})(v)\right|=\sum_{j^{\prime}:\\{j^{\prime},j\\}\in
E(T_{G})}\left|\mu(X_{i})\cap T_{j^{\prime}}\right|$

for $v\in T_{j}\setminus\mu(X_{i})$.

This means that we need to add the constraint

$\mathrm{lb}^{i}_{j}\leq\sum_{j^{\prime}:\\{j^{\prime},j\\}\in
E(T_{G})}y_{i}^{j^{\prime}}\leq\mathrm{ub}^{i}_{j}\\\ $ (llc1)

if $|\mu(X_{i})\cap T_{j}|\geq 1$ and add the constraint

$\mathrm{lb}^{i}_{j}\leq\sum_{j^{\prime}:\\{j^{\prime},j\\}\in
E(T_{G})}y_{i}^{j^{\prime}}-1\leq\mathrm{ub}^{i}_{j}\\\ $ (llc2)

if $|T_{j}\setminus\mu(X_{i})|\geq 1$.

Fortunately, we can deduce whether the conditions $|\mu(X_{i})\cap T_{j}|\geq
1$ or $|T_{j}\setminus\mu(X_{i})|\geq 1$ hold from the shape $sh$. If we have

$\sum_{I\,:\,I\ni i}sh(I,j)>0,\qquad\qquad\qquad\qquad\left(\forall
i\in[\ell]\right)$ (sh1)

then $\mu(X_{i})$ necessarily intersect $T_{j}$, whereas if we have

$\sum_{I\,:\,I\not\ni i}sh(I,j)>0,\qquad\qquad\qquad\qquad\left(\forall
i\in[\ell]\right)$ (sh2)

then there exists vertex in $T_{j}\setminus X_{i}$.

This means that the local linear constraints for type $T_{j}$ and variable
$X_{i}$ can be enforced by adding constraint (llc1) if (sh1) holds, and by
adding constraint (llc2) if (sh2) holds.

Let us turn our attention to the analysis of the running time of the
algorithm. There are at most

  * •

$(t+2)^{\nu}$ different shapes and

  * •

$2^{|\varphi|}$ pre-evaluation functions.

Since $t$ depends only on the number of quantifiers in the formula $\varphi$,
both numbers can be bounded by a function of $|\varphi|$ and $\nu$. For each
such combination of a shape and a pre-evaluation, we construct an ILP with
$\nu 2^{\ell}$ integer variables, so this ILP can be solved in time FPT time
with respect to $|\varphi|$ and $\nu$ by the aforementioned result of Lenstra
[33]. ∎

###### Proof of Theorem 4.

The theorem is a simple consequence of Theorem 22 and Lemma 21. ∎

###  3.3. Theorem 5: XP algorithm for ${\sf MSO}^{\sf GL}$

The main idea behind the proof of Theorem 5 is as follows. We use the
advantage of XP time to guess all sizes $b_{I}^{T}$ of the sets
$T\cap\bigcap_{i\in I}X_{i}$ for every type $T\in\mathcal{T}$ and every
$I\subseteq[\ell]$. Clearly, the number of possible assignments of $b_{I}^{T}$
can be upper-bounded by $n^{\nu 2^{\ell}}$. This immediately allows us to
verify global constraints and in particular $\varphi$. Note that at this point
this is possible since the vertices in $T$ are equivalent with respect to MSO
logic and thus the MSO-model-checking algorithm of Lampis [32] can be used to
verify $\varphi$ on the (now labeled) graph $G$. If $\varphi$ is satisfied, we
proceed in a similar way as in the proof of Theorem 4. Now, we have to check
whether there exists an assignment $\mu$ that obeys all local cardinality
constraints for each vertex in $G$. Observe that this can be done locally, as
the only thing that matters in the neighboring types is the number of vertices
in the sets $X_{1},\ldots,X_{\ell}$ (especially it is independent of the
actually selected vertices). This however, results in a computation of lower-
and upper-bounds on $b_{I}^{T}$ in a similar but simpler way to Lemma 19.
Finally, if all $b_{I}^{T}$ fulfill both lower- and upper-bounds, we have
found an assignment $\mu$ that on the one hand satisfies $\varphi$ (and thus
the global constraints) and on the other hand satisfies all the local
cardinality constraints. If such $b_{I}^{T}$’s do not exist it is impossible
to simultaneously satisfy the local and the global cardinality constraints.

####  3.3.1. Extended Numerical Assignments

Fix a formula $\varphi$ with $\ell$ free variables $X_{1},\ldots,X_{\ell}$.
Let $G=(V,E)$ be a graph and let $\mathcal{T}$ be its neighborhood diversity
decomposition. The _extended numerical assignment_ is a function $\sigma\colon
2^{\\{X_{1},\ldots,X_{\ell}\\}}\times\mathcal{T}\to\left[|G|\right]$. We say
that $\sigma$ is _valid for $G$ and $\mathcal{T}$_ if

$\sum_{I\in 2^{\\{X_{1},\ldots,X_{\ell}\\}}}\sigma(I,T)\leq|T|$

for each type $T\in\mathcal{T}$. The crucial thing is that extended numerical
assignment plays the same role for the purpose of a design of the XP algorithm
as pre-evaluations for the FPT algorithm presented in Section 3.2. We
formalize this by showing that knowing $\sigma$ it is possible to decide
whether $\varphi$ holds for $G$ or not. Before we do so, we have to introduce
one more formalism. We say that an assignment
$\mu\colon\left\\{X_{1},\ldots,X_{\ell}\right\\}\to 2^{V}$ is a _realisation_
of a valid extended numerical assignment $\sigma$ if

$\left|\left(\bigcap_{i\in I}X_{i}\right)\cap T\right|=\sigma(I,T)$

for every $I\subseteq\left\\{X_{1},\ldots,X_{\ell}\right\\}$ and every type
$T\in\mathcal{T}$.

###### Lemma 23

Fix a formula $\varphi$ with $\ell$ free variables $X_{1},\ldots,X_{\ell}$.
Let $G$ be a graph, let $\mathcal{T}$ be its neighborhood diversity
decomposition, and let $\sigma$ be a valid extended numerical assignment. Then
either each realization $\mu$ of $\sigma$ satisfies $\varphi$ or no
realization of $\sigma$ satisfies $\varphi$.

###### Proof.

Let assignment $\mu,\mu^{\prime}$ be realizations of $\sigma$. We will show
that $G,\mu\models\varphi$ if and only if $G,\mu^{\prime}\models\varphi$. This
is not hard to see. Note that the global cardinality constraints
$R_{1},\ldots,R_{c}$ contained in $\varphi$ depend solely on the number of
vertices contained in some $X_{i}$’s and some types of $\mathcal{T}$ which is,
however, prescribed by $\sigma$ and thus both $\mu,\mu^{\prime}$ have to agree
on this. Now, it is possible to evaluate the validity of all of the
constraints $R_{1},\ldots,R_{c}$ and (as in the case of pre-evaluations)
replace them by the constants true or false in $\varphi$ yielding a simplified
formula $\tilde{\varphi}$. The lemma now follows from the fact that
$\tilde{\varphi}$ is a MSO formula and both $\mu,\mu^{\prime}$ yield the same
labeled graph. ∎

By this we have shown that it makes sense to write $G,\sigma\models\varphi$.
Observe that there are at most $|G|^{|\mathcal{T}|\cdot 2^{\ell}}$ (valid)
extended numerical assignments for $G$.

####  3.3.2. Satisfying Local Cardinality Constraints

Fix a valid extended numerical assignment $\sigma$ with
$G,\sigma\models\varphi$. It follows from Lemma 23 that if
$G,\sigma\models\varphi$, then there is at least one assignment $\mu$
realising $\sigma$. Now, we would like to resolve whether among all of the
possible realizations of $\sigma$ there is at least one realization that obeys
the local cardinality constraints $\alpha_{1},\ldots,\alpha_{\ell}$.

Fix a type $T\in\mathcal{T}$ and define the function
$s\colon\\{1,\ldots,\ell\\}\to\mathbb{N}$ by

$s(i)=\left|\bigcup_{S\in\mathcal{T}:\\{S,T\\}\in E(T_{G})}(S\cap
X_{i})\right|.$

Recall that if $T$ is a clique in $G$, it has a loop in the corresponding
typegraph $T_{G}$. Now, following Proposition 18 we say that
$\alpha_{1},\ldots,\alpha_{\ell}$ are _possibly satisfied by $\sigma$_ if

  * •

$s(i)\in\alpha_{i}(v)$ for all $i\in[\ell]$ and $v\in T$, where $T$ is an
independent set in $G$ and

  * •

$\\{s(i)-1,s(i)\\}\cap\alpha_{i}(v)=\emptyset$ for all $i\in[\ell]$ and $v\in
T$, where $T$ is a clique in $G$.

Observe that if $T$ is an independent set in $G$ and
$\alpha_{1},\ldots,\alpha_{\ell}$ are possibly satisfied by $\sigma$, then
every assignment $\mu$ realizing $\sigma$ fulfills
$\alpha_{1},\ldots,\alpha_{\ell}$ for every vertex in $T$. This is, however,
not true when $T$ is a clique in $G$. In this case we let $t^{+}_{i}$ be the
number of vertices in $T$ with
$\\{s(i)-1,s(i)\\}\cap\alpha_{i}(v)=\\{s(i)-1\\}$, we let $t^{-}_{i}$ be the
number of vertices in $T$ with
$\\{s(i)-1,s(i)\\}\cap\alpha_{i}(v)=\\{s(i)\\}$, and we let $t^{\pm}_{i}$ be
$|T|-(t^{+}_{i}+t^{-}_{i})$. Note that $t^{+}_{i}$ is the number of vertices
in $T$ that must belong to $X_{i}$, $t^{-}_{i}$ is the number of vertices in
$T$ that cannot belong to $X_{i}$, and $t^{\pm}_{i}$ is the number of vertices
in $T$ that may or may not belong to $X_{i}$ (again this directly follows from
Proposition 18). Thus, we arrive at the following claim.

###### Lemma 24

If $\alpha_{1},\ldots,\alpha_{\ell}$ are possibly satisfied by $\sigma$ and
for each type $T\in\mathcal{T}$ forming a clique in $G$ we have

$t^{+}_{i}\leq s(i)\leq t^{+}_{i}+t^{\pm}_{i}\,,$

then there is an assignment $\mu$ realizing $\sigma$ and fulfilling all of
$\alpha_{1},\ldots,\alpha_{\ell}$. ∎

###### Proof of Theorem 5.

There are $|G|^{\nu\cdot 2^{\ell}}$ possible (valid) extended numerical
assignments for $G$. We loop through all of them and for each such $\sigma$ we

  1. (1)

check if $G,\sigma\models\varphi$,

  2. (2)

check if $\sigma$ possibly satisfies $\alpha_{1},\ldots,\alpha_{\ell}$, and

  3. (3)

verify the conditions given in Lemma 24.

If all three of the above conditions are satisfied, we accept $\sigma$ and say
Yes, otherwise we reject $\sigma$ and proceed to next $\sigma$. If there is no
$\sigma$ left, we say No. It is not hard to see that the above procedure takes
$O(n\cdot n^{\nu\cdot 2^{\ell}})$ time and can be simply extended so that it
actually returns the sought assignment $\mu$ in the same time. ∎

##  4\. Theorem 1: XP algorithm for ${\sf MSO}^{\sf GL}$ on bounded treewidth

We believe that the merit of Theorem 1 lies not only in being a very general
tractability result, but also in showcasing a simplified way to prove a
metatheorem extending MSO. Our main tool is the constraint satisfaction
problem (CSP). The key technical result of this section is Theorem 30, which
relates MSO and CSP on graphs of bounded treewidth. Let us shortly describe
it.

Notice that in the ${\sf MSO}^{\sf GL}$ model checking problem, we wish to
find a satisfying assignment of some formula $\varphi$ which satisfies further
constraints. Simply put, Theorem 30 says that it is possible to restrict the
set of satisfying assignments of a formula $\varphi\in$ MSO1 with CSP
constraints under the condition that these additional constraints are
structured along the tree decomposition of $G$. This allows the proof of
Theorem 1 to simply be a CSP formulation satisfying this property.

We believe that the key advantage of our approach, when compared with prior
work, is that it is _declarative_ : it only states what a solution looks like,
but does not describe how it is computed. This makes the proof cleaner, and
possible extensions easier.

We consider a natural optimization version of ${\sf MSO}^{\sf GL}$:

Weighted ${\sf MSO}^{\sf GL}$
Input: An ${\sf MSO}^{\sf GL}$ model checking instance, weights
$\mathbf{w}^{1},\dots,\mathbf{w}^{\ell}\in\mathbb{Z}^{n}$. Task: Find an
assignment $X_{1},\dots,X_{\ell}$ satisfying the ${\sf MSO}^{\sf GL}$ model
checking instance and minimizing $\sum_{j=1}^{\ell}\sum_{v\in
X_{j}}w_{v}^{j}$.

###  4.1. CSP, MSO and treewidth

######  Definition 25 (CSP).

An instance $I=(V,\mathcal{D},\mathcal{H},\mathcal{S})$ of CSP consists of

  * •

a set of variables $z_{v}$, one for each $v\in V$; without loss of generality
we assume that $V=[|V|]$,

  * •

a set $\mathcal{D}$ of finite domains $D_{v}\subseteq\mathbb{Z}$, one for each
$v\in V$,

  * •

a set of hard constraints $\mathcal{H}\subseteq\\{C_{U}\mid U\subseteq V\\}$
where each hard constraint $C_{U}\in\mathcal{H}$ with a _scope_
$U=\\{i_{1},\dots,i_{k}\\}$ and $i_{1}<\cdots<i_{k}$, is a $|U|$-ary relation
$C_{U}\subseteq D_{i_{1}}\times\cdots\times D_{i_{k}}$,

  * •

a set of weighted soft constraints $\mathcal{S}\subseteq\\{w_{U}\mid
U\subseteq V\\}$ where each ${w_{U}\in\mathcal{S}}$ with a _scope_
$U=\\{i_{1},\dots,i_{k}\\}$ and ${i_{1}<\cdots<i_{k}}$ is a function
$w_{U}:D_{i_{1}}\times\cdots\times D_{i_{k}}\rightarrow\mathbb{R}$.

For a vector ${\mathbf{z}=(z_{1},\ldots,z_{|}V|)}$ and a set
$U=\\{i_{1},\dots,i_{k}\\}\subseteq V$ with ${i_{1}<\cdots<i_{k}}$, we define
the projection of $\mathbf{z}$ on $U$ as
$\mathbf{z}|_{U}=(z_{i_{1}},\ldots,z_{i_{k}})$. A vector
$\mathbf{z}\in\mathbb{Z}^{|V|}$ satisfies the hard constraint
$C_{U}\in\mathcal{H}$ if and only if $\mathbf{z}|_{U}\in C_{U}$. We say that a
vector ${\mathbf{z}^{\star}=(z^{\star}_{1},\ldots,z^{\star}_{|V|})}$ is a
feasible assignment for $I$ if ${\mathbf{z}^{\star}\in D_{1}\times\cdots\times
D_{|V|}}$ and $\mathbf{z}^{\star}$ satisfies every hard constraint
$C\in\mathcal{H}$, and write ${\rm
Feas}(I)={\\{\mathbf{z}^{\star}\mid\mathbf{z}^{\star}}\mbox{ is a
feasible}\allowbreak\mbox{ assignment for }I\\}$. The _weight_ of
$\mathbf{z}^{\star}$ is
$w(\mathbf{z}^{\star})=\sum_{w_{U}\in\mathcal{S}}w_{U}(\mathbf{z}^{\star}|_{U})$.
We denote by $D_{I}$ the maximum size of all domains, that is,
$D_{I}=\max_{u\in V}|D_{u}|$, and we omit the subscript $I$ if the instance is
clear from the context. We denote by $\|\mathcal{D}\|$, $\|\mathcal{H}\|$ and
$\|\mathcal{S}\|$ the _length_ of $\mathcal{D}$, $\mathcal{H}$ and
$\mathcal{S}$, respectively, and define it as $\|\mathcal{D}\|=\sum_{v\in
V}|D_{v}|$, $\|\mathcal{H}\|=\sum_{C_{U}\in\mathcal{H}}|C_{U}|$ and
$\|\mathcal{S}\|=\sum_{w_{U}}|w_{U}|$; here $|w_{U}|$ denotes the size of the
subset of $D_{i_{1}}\times\cdots\times D_{i_{k}}$ for which the function
$w_{U}$ is nonzero.

######  Definition 26 (Constraint graph, Treewidth of CSP).

For a CSP instance $I=(V,\mathcal{D},\mathcal{H},\mathcal{S})$ we define the
_constraint graph_ $G(I)$ of $I$ as $G=(V,E)$ where

$E=\left\\{\\{u,v\\}\mid(\exists C_{U}\in\mathcal{H})\vee(\exists
w_{U}\in\mathcal{S})\textrm{ s.t. }\\{u,v\\}\subseteq U\right\\}.$

The treewidth of a CSP instance $I$, $tw(I)$, is defined as
$\operatorname{tw}(G(I))$. When we talk about $G(I)$ we use the terms
“variable” and “vertex” interchangeably.

Freuder [17] proved that CSPs of bounded treewidth can be solved quickly. We
use a natural weighted version of this result.

######  Proposition 27 ([17])

For a CSP instance $I$ of treewidth $\tau$ and maximum domain size $D$, a
minimum weight solution can be found in time
${\mathcal{O}(D^{\tau}|V|+\|\mathcal{H}\|+\|\mathcal{S}\|)}$.

Modeling after the terminology regarding extended formulations of polytopes
[8], we introduce the notion of a _CSP extension_.

######  Definition 28 (CSP extension).

Let $I=(V_{I},\mathcal{D}_{I},\mathcal{H}_{I},\mathcal{S}_{I})$ be a CSP
instance. We say that
$J=(V_{J},\mathcal{D}_{J},\mathcal{H}_{J},\mathcal{S}_{J})$ is an _extension
of $I$_ (or that _$J$ extends $I$_) if $V_{I}\subseteq V_{J}$ and ${\rm
Feas}(I)=\\{\mathbf{z}^{\star}|_{V_{I}}\mid\mathbf{z}^{\star}\in{\rm
Feas}(J)\\}$.

By Proposition 27, we can solve CSP instances of small treewidth efficiently.
Our motivation for introducing CSP extensions is that we are able to formulate
a CSP instance $I$ expressing what we need, but having large treewidth.
However, if an extension $J$ of $I$ exists with small treewidth, solving $J$
instead suffices.

Let $\varphi$ be an MSO1 formula with $\ell$ free variables and let $G$ be a
graph on $n$ vertices. We say that a binary vector
$\mathbf{y}\in\\{0,1\\}^{n\ell}$ _satisfies $\varphi$_
($G,\mathbf{y}\models\varphi$) if it is a characteristic vector of a
satisfying assignment, that is, if $v\in X_{i}\Leftrightarrow y_{v}^{i}=1$ and
$G\models\varphi(X_{1},\dots,X_{\ell})$. For a vector $\mathbf{s}$, let the
_support of $\mathbf{s}$_ be $\textrm{supp}(\mathbf{s})=\\{i\mid s_{i}\neq
0\\}$, that is, the set of its nonzero indices. The following definition
characterizes sets which are structured along a given tree decomposition of a
graph. The subsequent theorem then shows that, provided a CSP model whose
constraints are structured in this way along a tree decomposition of $G$,
there exists a compact and tree-structured CSP extension.

######  Definition 29 (Local scope property).

Let $m,\ell\in\mathbb{N}$, $G$ be a $\sigma_{2}$-structure representing a
graph, $(T,\mathcal{B})$ be its nice tree decomposition, and $S$ be a set of
vectors of elements indexed by $V(G)\times[m]$ and $V(T)\times[\ell]$. We say
that $S$ has the _local scope property_ if

$\displaystyle\forall\mathbf{s}\in S~{}\exists a\in
V(T):~{}\textrm{supp}(\mathbf{s})\subseteq\big{(}$ $\displaystyle\\{(v,i)\mid
v\in B(a),i\in[m]\\}~{}\cup$ $\displaystyle\\{(b,j)\mid b\in
N_{T}(a),j\in[\ell]\\}\big{)}.$

The heart of our proof of Theorem 1 is the following theorem.

###### Theorem 30

Let $I=(V,\mathcal{D},\mathcal{H},\mathcal{S})$ be a CSP instance such that
there exists a $\sigma_{2}$-structure $G$ representing a graph, an ${\sf
MSO}_{1}$ formula $\varphi$ with $\ell$ free variables, a nice tree
decomposition $(T,\mathcal{B})$ of $G$ of width $\tau$, and an integer
$k\in\mathbb{N}$, so that $V$ and $\mathcal{H}$ satisfy

$V=\\{y_{v}^{i}\mid v\in V(G),i\in[\ell]\\}\cup\\{x_{a}^{j}\mid a\in
V(T),j\in[k]\\}\text{ and }\mathcal{H}=\\{\mathbf{y}\mid
G,\mathbf{y}\models\varphi\\}\cup\mathcal{H}^{\prime}.$

If $\mathcal{H}^{\prime}\cup\mathcal{S}$ have the local scope property, then
there exists a CSP instance
$J=(V_{J},\mathcal{D}_{J},\mathcal{H}_{J},\mathcal{S}_{J})$ which extends $I$,
and,

  * •

$\operatorname{tw}(J)\leq f(|\varphi|,\tau)+2k$,

  * •

$\|\mathcal{H}_{J}\|+\|\mathcal{S}_{J}\|\leq
f(|\varphi|,\tau)\cdot|V|+(\|\mathcal{H}^{\prime}\|+\|\mathcal{S}\|)$,

  * •

$D_{J}=D_{I}$.

Before giving the proof, we will show how it Theorem 30 implies Theorem 1.

###  4.2. CSP instance construction

###### Proof of Theorem 1.

As before, we first note that there are at most $2^{|\varphi|}$ different pre-
evaluations $\beta(\varphi)$ of $\varphi$, so we can try each and choose the
best result. Let a pre-evaluation $\beta(\varphi)$ be fixed from now on.

Let $(T,\mathcal{B})$ be a nice tree decomposition of $G$. We will now
construct a CSP instance $I$ satisfying the conditions of Theorem 30, which
will give us its extension $J$ with properties suitable for applying Freuder’s
algorithm (Proposition 27).

Let $y_{v}^{i}$ be the variables as described above in Theorem 30; we use the
constraint $G,\mathbf{y}\models\beta(\varphi)$ to enforce that each feasible
solution complies with the pre-evaluation $\beta(\varphi)$. Now we will
introduce additional CSP variables and constraints in two ways to assure that
the local and global cardinality constraints are satisfied. Observe that we
introduce the additional CSP variables and constraints in such a way that they
have the local scope property (Definition 29), that is, their scopes will
always be limited to the neighborhood of some node $a\in V(T)$.

##### Global cardinality constraints.

In addition to the original $\mathbf{y}$ variables, we introduce, for each
node $a\in T$ and each $j\in[\ell]$, a variable $s_{a}^{j}$ with domain $[n]$.
We refer to the set of these variables as to $s$-variables. The meaning of
this variable is $s_{a}^{j}=|X_{j}\cap V(G_{a})|$. Thus, in the root node $r$,
$s_{r}^{j}$ is exactly $|X_{j}|$. To enforce the desired meaning of the
variables $\mathbf{s}$, we add the following hard constraints:

$\displaystyle s_{a}^{j}$ $\displaystyle=0$ $\displaystyle\forall\textrm{
leaves }a$ $\displaystyle s_{a}^{j}$ $\displaystyle=s_{b}^{j}+y_{v}^{j}$
$\displaystyle\forall a=b*(v)$ $\displaystyle s_{a}^{j}$
$\displaystyle=s_{b}^{j}$ $\displaystyle\forall a=b\dagger(v)$ $\displaystyle
s_{a}^{j}$ $\displaystyle=s_{b}^{j}+s_{b^{\prime}}^{j}-\sum_{v\in
B(a)}y_{v}^{j}$ $\displaystyle\forall a=\Lambda(b,b^{\prime})$

To enforce the cardinality constraints themselves, we add:

$\displaystyle(s_{r}^{1},\dots,s_{r}^{\ell})$ $\displaystyle\in R$
$\displaystyle\forall R:\beta(R)=\texttt{true}$
$\displaystyle(s_{r}^{1},\dots,s_{r}^{\ell})$
$\displaystyle\in([n]^{\ell}\setminus R)$ $\displaystyle\forall
R:\beta(R)=\texttt{false}$

##### Local cardinality constraints.

For every node $a\in V(T)$, every $j\in[\ell]$ and every vertex $v\in B(a)$,
introduce a variable $\lambda_{a}^{vj}$ with domain $[n]$, with the meaning
$\lambda_{a}^{vj}=|N_{G_{a}}(v)\cap X_{j}|$. We refer to these as to
$\lambda$-variables. Their meaning is enforced by setting:

$\displaystyle\lambda_{a}^{vj}$ $\displaystyle=\sum_{\begin{subarray}{c}u\in
B(a):u\neq v\\\ uv\in E\end{subarray}}y_{u}^{j}$ $\displaystyle\forall
a=b*(v)$ $\displaystyle\lambda_{a}^{uj}$
$\displaystyle=\lambda_{b}^{uj}+y_{v}^{j}$ $\displaystyle\forall a=b*(v),u\in
B(a),uv\in E$ $\displaystyle\lambda_{a}^{vj}$ $\displaystyle=\lambda_{b}^{vj}$
$\displaystyle\forall a=b\dagger(u),u\neq v,v\in B(a)$
$\displaystyle\lambda_{a}^{vj}$
$\displaystyle=\lambda_{b}^{vj}+\lambda_{b^{\prime}}^{vj}-\sum_{\begin{subarray}{c}u\in
B(a):u\neq v\\\ uv\in E\end{subarray}}y_{u}^{j}$ $\displaystyle\forall
a=\Lambda(b,b^{\prime})$

Now the local constraints themselves are enforced by setting:

$\displaystyle\lambda_{\textrm{top}(v)}^{vj}$ $\displaystyle\in\alpha^{j}(v)$
$\displaystyle\forall v\in V,\quad j\in[\ell]\enspace.$

##### Objective function.

In order to express the objective function we add soft constraints
$\mathcal{S}=\\{C_{\\{y_{v}^{j}\\}}\mid v\in V,j\in[\ell]\\}$ where
$C_{\\{y_{v}^{j}\\}}=w_{v}^{j}$ if $y_{v}^{j}=1$ and is $0$ otherwise.

In order to apply Theorem 30, let us determine the parameters of the CSP
instance $I$ we have constructed, namely the number of extra variables per
node $k$, the maximum domain size $D_{I}$, and the lengths of the additional
constraints $\|\mathcal{H}^{\prime}\|$ and $\|\mathcal{S}\|$.

We have introduced $\ell$ $s$-variables per node, and $\ell\tau$
$\lambda$-variables per node. Thus, $k=(\tau+1)\ell$. Since each $s$\- and
$\lambda$-variable corresponds to a size of some vertex subset, its value us
upper bounded by $n$, and thus $D_{I}=n$. Let

$N=\sum_{j=1}^{c}|R_{j}^{G}|+\sum_{j=1}^{\ell}\sum_{v\in V(G)}|\alpha_{j}(v)|$

be the input length of the global and local cardinality constraints.

Then, Theorem 30 implies that there exists a CSP instance $J$ which is an
extension of $I$ and has

  * •

$\operatorname{tw}(J)\leq f(|\varphi|,\tau)+2k\leq
f(|\varphi|,\tau)+(\tau+1)\ell\leq f^{\prime}(|\varphi|,\tau)$ for some
computable function $f^{\prime}$,

  * •

$\|\mathcal{H}_{J}\|+\|\mathcal{S}_{J}\|\leq
f(|\varphi|,\tau)\cdot|V|+(\|\mathcal{H}^{\prime}\|+\|\mathcal{S}\|)\leq
f(|\varphi|,\tau)\cdot n+N$, and

  * •

$D_{J}=D_{I}=n$.

Finally, applying Proposition 27 to $J$ solves it in time
$n^{f^{\prime}(|\varphi|,\tau)}+N$, finishing the proof of Theorem 1. ∎

##### Conditional cardinality constraints

As Szeider [38] points out, it is easy to extend his XP result for ${\sf
MSO}^{\sf L}$ in such a way that the local cardinality constraint
$|X(v)|\in\alpha(v)$ is conditioned on the fact that $v\in X$. Observe that
our approach can be extended in such a way as well. Moreover, in our setting
with multiple set variables, we can even condition on an arbitrary predicate
$\psi(v,X_{1},\dots,X_{m})$ describing how vertex $v$ relates to the set
variables.

###  4.3. Applications (Corollary 2)

Let us briefly sketch some consequences of Theorem 1. We focus on showing how
to encode various W[1]-hard (w.r.t. treewidth) problems using the notions we
have provided. The parameterized complexity statements which follow are not
very surprising and in many cases were known. Still, we believe that our
approach captures and summarizes them nicely.

##### Local constraints

While introducing ${\sf MSO}^{\sf L}$, Szeider [38] points out that the
problems General Factor, Equitable $k$-Coloring and Minimum Maximum Outdegree
are expressible in ${\sf MSO}^{\sf L}$. Let us now observe that using the
extension to conditional local constraints, we can also express the problems
Capacitated Dominating Set, Capacitated Vertex Cover, Vector Dominating Set
and Generalized Domination.

Take for example the Capacitated Dominating Set problem. There, we are given a
graph $G=(V,E)$ together with a capacity function $c:V\to\mathbb{N}$, and our
goal is to find a subset $D\subseteq V$ and a mapping $f:V\setminus D\to D$
such that for each $v\in D$, $|f^{-1}(v)|\leq c(v)$. Essentially, $f(w)=v$
means that the vertex $w$ is dominated by the vertex $v$, and the condition
$|f^{-1}(v)|\leq c(v)$ ensures that the mapping $f$ respects the capacities.
To encode this problem using ${\sf MSO}^{\sf L}$, we need to view $G$ as its
incidence graph $I(G)$ whose vertex set is $V_{I}=V\cup E$. Then, we let
$\varphi(D,F)$ and $\alpha$ be a formula and local cardinality constraints,
respectively, enforcing that:

  * •

$D\subseteq V$,

  * •

$F\subseteq E$,

  * •

each $v\in V$ is either in $D$ or has a neighbor in $F$,

  * •

each $e\in F$ has a neighbor in $D$, and,

  * •

if $v\in D$, then $|N(v)\cap F|\in\alpha_{F}(v)=[0,c(v)]$.

Then $D$ encodes a dominating set and $F$ can be used to construct the mapping
$f$ since for each edge $e\in F$, at most one of its endpoints is not in $D$,
and each $v\in D$ sees at most $c(v)$ edges from $F$.

Let us define the remaining problems; their ${\sf MSO}^{\sf L}$ formulations
are analogous to the one above. The Vector Dominating Set problem is similar
to Capacitated Dominating Set, except now each vertex $v$ has a _demand_
$d(v)$ and if $v\not\in D$, then it must have at least $d(v)$ neighbors in
$D$. In Generalized Domination, we are given two sets
$\sigma,\rho\subseteq\mathbb{N}$ and for each vertex $v$ in $D$ or in
$V\setminus D$, it must hold that $|N(v)\cap D|\in\sigma$ or $|N(v)\cap
D|\in\rho$, respectively. Finally, the Capacitated Vertex Cover problem is the
following. We are given a capacitated graph, and the task is to find a vertex
cover $C\subseteq V$ and an assignment $f:E\to C$ such that for each $v$,
$|f^{-1}(v)|\leq c(v)$.

##### Global constraints: $k$-Balanced Partitioning

Ganian and Obdržálek [20] introduce ${\sf MSO}^{\sf G}_{\sf lin}$ and show
that also this logic expresses Equitable $k$-Coloring, and moreover the
Equitable connected $k$-Partition problem. Interestingly, they also discuss
the complexity of the $k$-Balanced Partitioning problem, where the goal is to
find an equitable (all parts of size differing by at most one) $k$-partition
and, moreover, minimize the number of edges between partites. They provide an
FPT algorithm for graphs of bounded vertex cover, but are unable to express
the problem in ${\sf MSO}^{\sf G}_{\sf lin}$, and thus pose as an open problem
the task of finding a more expressive formalism which would capture this
problem. They also state that no parameterized algorithm exists for graphs of
bounded treewidth, but that is no longer true due to the results of van Bevern
et al. [39]. On the other hand, the question of capturing $k$-Balanced
Partitioning by some MSO extension stands. Here we show that it can be
expressed as an instance of weighted ${\sf MSO}^{\sf G}_{\sf lin}$ model
checking when we use edge set variables (thus this is not applicable to graphs
of bounded neighborhood diversity).

Let $\varphi$ be an ${\sf MSO}^{\sf G}$ formula with $k$ free vertex set
variables $X_{1},\dots,X_{k}$ and one free edge set variable $Y$. We use
$\varphi$ to express that $X_{1},\dots,X_{k}$ is an equitable $k$-partition;
this is easily done using the global constraints. Furthermore, we enforce that
$Y$ is the set of edges with one endpoint in $X_{i}$ and another in $X_{j}$
for any $i\neq j$. For a satisfying assignment $X_{1},\dots,X_{k},Y$, let
$(\mathbf{x},\mathbf{y})\in\\{0,1\\}^{k|V|}\times\\{0,1\\}^{|E|}$ be its
characteristic vector. To minimize the number of edges between partites, it
suffices to minimize $\mathbf{y}$. This also clearly extends to the case
studied in the literature when edges are assigned weights.

Moreover, it is not difficult to see that the CSP instance in the proof of
Theorem 1 could be extended to enforce constraints such as $\sum_{v\in
V}|X(v)|\in A$ for some set $A\subseteq\mathbb{N}$. With such constraints, it
is possible to directly express the set of minimal (by appropriate choice of
$A$) $k$-balanced partitions, which in turn provides a compact extended
formulation.

##### Global constraints: Graph Motif

Fellows et al. [15] study the Graph Motif problem from the perspective of
parameterized complexity, especially on graphs with bounded widths. In Graph
Motif, we are given a vertex-colored graph $G$ and a multiset of colors $M$,
and the task is to find a _motif_ , that is, a connected subset of vertices
$S\subseteq V$ such that the multiset of colors of $S$ is exactly $M$. This
problem is most naturally expressed when the vertex-colored graph $G$ is
encoded as a general relational structure over a finite vocabulary. Since we
have not explicitly phrased our results for such structures, Graph Motif does
not directly fit any of our notions; however, the extension of our results
(specifically, Theorem 1) to general structures is straightforward.

Then, let us consider the number of colors $\chi$ a parameter and introduce
additional unary relations (labels) $L_{1},\dots,L_{\chi}$. It is easy to see
that Graph Motif is encoded by the following ${\sf MSO}^{\sf G}_{\sf lin}$
formula $\varphi(S)$:

$\varphi(S)\equiv\text{connected}(S)\wedge\bigwedge_{i=1}^{\chi}[|S\cap
L_{i}|=\text{mult}(i,M)],$

where $\text{connected}(S)$ is a formula which holds if $S$ is connected, and
$\text{mult}(i,M)\in\mathbb{N}$ is the multiplicity of color $i$ in the motif
$M$.

###  4.4. Proof of Theorem 30

Fix objects and quantities as in the statement of Theorem 30, that is,
$I=(V,\mathcal{D},\mathcal{H},\mathcal{S})$ is a CSP instance for which there
exists a $\sigma_{2}$-structure $G$ representing a graph, $n:=|V(G)|$,
$\varphi$ is an MSO1 formula with $\ell$ free variables, $(T,\mathcal{B})$ is
a nice tree decomposition of $G$ of width $\tau$, $k\in\mathbb{N}$ is such
that $V$ has $\ell\cdot|V(G)|$ variables $y_{v}^{i}$ and $k\cdot|V(T)|$
variables $x_{a}^{j}$, $\mathcal{H}=\\{\mathbf{y}\mid
G,\mathbf{y}\models\varphi\\}\cup\mathcal{H}^{\prime}$ and $\mathcal{S}$ has
the local scope property.

We give a brief outline of the proof of Theorem 30, which proceeds in three
stages:

  1. (1)

Using a recent result of Kolman, Koutecký and Tiwary [29] we construct a
linear program (LP) of bounded treewidth whose integer solutions correspond to
feasible assignments of $\varphi$.

  2. (2)

We view this LP as an integer linear program (ILP) and construct an equivalent
CSP instance $J^{\prime}$ of bounded treewidth. Thus, $J^{\prime}$ is an
extension of
$I^{\prime}=([n\cdot\ell],\mathcal{D}_{I^{\prime}},\mathcal{H}_{I^{\prime}},\emptyset)$
where $\mathcal{D}_{I^{\prime}}=\\{D_{i}\mid
D_{i}=\\{0,1\\},\,i\in[n\cdot\ell]\\}$ and
$\mathcal{H}_{I^{\prime}}=\\{\mathbf{y}\mid G,\mathbf{y}\models\varphi\\}$.

  3. (3)

We show that if $\mathcal{H}^{\prime}$ and $\mathcal{S}$ have the local scope
property, it is possible to add new constraints derived from
$\mathcal{H}^{\prime}$ and $\mathcal{S}$ to the instance $J^{\prime}$ which
results in instance $J$ (with ${\rm Feas}(J)\subseteq{\rm Feas}(J^{\prime})$),
such that $J$ is an extension of $I$.

##### Stage 1: LP

We begin by extending our notion of treewidth to matrices.

######  Definition 31 (Treewidth of a matrix).

Given a matrix $\mathbf{A}\in\mathbb{Z}^{m\times n}$, we define its _Gaifman
graph_ $G=G(\mathbf{A})$ as follows. Let $V(G)=[n]$. Let $\\{i,j\\}\in E(G)$
if and only if there is an $r\in[n]$ with $\mathbf{A}[r,i]\neq 0$ and
$\mathbf{A}[r,j]\neq 0$. The _(primal or Gaifman) treewidth of a matrix
$\mathbf{A}$_ is then
$\operatorname{tw}(\mathbf{A}):=\operatorname{tw}(G(\mathbf{A}))$.

Let $P_{\varphi}(G)=\textrm{conv}\\{\mathbf{y}\mid
G,\mathbf{y}\models\varphi\\}$ be the polytope of satisfying assignments of
$\varphi$ on $G$, also called the _MSO 1 polytope_; $\textrm{conv}(X)$ denotes
the convex hull of a set $X$. A result of Kolman et al. [29] shows that there
exists an extended formulation of $P_{\varphi}(G)$ with many useful
properties:

######  Proposition 32 ([29, Theorem 4])

Let $G=(V,E)$ be a $\sigma_{2}$-structure representing a graph, let $n=|V|$,
$(T,\mathcal{B})$ be its nice tree decomposition of width $\tau$, and
$\varphi$ be an MSO1 formula with $\ell$ free variables.

Then there exists an LP
$\mathbf{A}\mathbf{y}+\mathbf{D}\mathbf{z}+\mathbf{C}\mathbf{w}=\mathbf{d},\,\mathbf{z},\mathbf{w}\geq
0$, a set $\mathcal{C}$, a function $\eta:\mathcal{C}\times V(T)\times
V\times[\ell]\rightarrow\\{0,1\\}$ and a tree decomposition
$(T,\mathcal{B}^{*})$ of the Gaifman graph
$G(\mathbf{A}~{}\mathbf{D}~{}\mathbf{C})$ such that the following claims hold:

  1. (1)

The polytope
$P=\\{(\mathbf{y},\mathbf{z},\mathbf{w})\mid\mathbf{A}\mathbf{y}+\mathbf{D}\mathbf{z}+\mathbf{C}\mathbf{w}=\mathbf{d},\,\mathbf{z},\mathbf{w}\geq\mathbf{0}\\}$
is a $0/1$-polytope and
$P_{\varphi}(G)=\\{\mathbf{y}\mid\exists\mathbf{z},\mathbf{w}:(\mathbf{y},\mathbf{z},\mathbf{w})\in
P\\}$.

  2. (2)

For any integer point $(\mathbf{y},\mathbf{z},\mathbf{w})\in P$, for any
$t\in\mathcal{C}$, $b\in V(T)$, $v\in B(b)$ and $i\in[\ell]$, equalities
$z_{b}^{t}=1$ and $\eta(t,b,v,i)=1$ imply that $y_{v}^{i}=1$.

  3. (3)

    1. (a)

The treewidth of $(T,\mathcal{B}^{*})$ is $\mathcal{O}(|\mathcal{C}|^{3})$,

    2. (b)

for every node $b\in V(T)$, $\bigcup_{t\in\mathcal{C}}\\{z_{b}^{t}\\}\subseteq
B^{*}(b)$.

  4. (4)

There is a computable function $f$ such that $|\mathcal{C}|\leq
f(\tau,|\varphi|)$ and $\mathbf{A},\mathbf{D},\mathbf{C},\mathbf{d},\eta$ can
be computed in time $\mathcal{O}(|\mathcal{C}|^{3}\cdot n)$.

##### Stage 2: Viewing ILP as CSP

By $\mathbf{a}_{j}$ we denote the $j$-th row of a matrix $\mathbf{A}$. Let us
connect ILP and CSP:

######  Definition 33.

A CSP instance $I$ is equivalent to an ILP
$\mathbf{A}\mathbf{x}\leq\mathbf{b}\,\mathbf{x}\in\mathbb{Z}^{n}$ if

$\\{\mathbf{x}\in\mathbb{Z}^{n}\mid\mathbf{A}\mathbf{x}\leq\mathbf{b}\\}={\rm
Feas}(I).$

###### Proposition 34

Let $\mathbf{A}\mathbf{x}\leq\mathbf{b},\,\mathbf{x}\in\mathbb{Z}^{n}$ be an
ILP with $\mathbf{A}\in\mathbb{Z}^{m\times n}$,
$\tau=\max_{j=1}^{m}|\textrm{supp}(\mathbf{a}_{j})|$ and
$D=\max_{i=1}^{n}|u_{i}-\ell_{i}|$, where $u_{i}$ and $\ell_{i}$ are an upper
and lower bound on $x_{i}$, that is,
$\mathbf{u}\leq\mathbf{x}\leq\mbox{\boldmath$\ell$}$ holds. Then, an
equivalent CSP instance $I$ can be constructed in time
$\mathcal{O}(D^{\tau}\cdot mn)$, and $G(\mathbf{A})=G(I)$.

###### Proof.

Let $V=\\{x_{1},\dots,x_{n}\\}$. For every $i\in[n]$, let
$D_{i}=[\ell_{i},u_{i}]$ and $\mathcal{D}=\\{D_{i}\mid i\in[n]\\}$. Observe
that $\max_{i}|D_{i}|=\|\mathbf{u}-\mbox{\boldmath$\ell$}\|_{\infty}=D$.
Regarding hard constraints $\mathcal{H}$, observe that every row
$\mathbf{a}_{j}$ of $\mathbf{A}$ contains at most $\tau$ non-zeros. Let
$U_{j}=\textrm{supp}(\mathbf{a}_{j})=\\{i_{1},\dots,i_{k}\\}$, where
$k\leq\tau$, and let $x_{c}=0$ for all $c\not\in U_{j}$. Let $C_{U_{j}}$ be
the set of assignments from $D_{i_{1}}\times\cdots\times D_{i_{k}}$ to
$x_{i_{1}},\ldots,x_{i_{k}}$ that satisfy $\mathbf{a}_{j}\mathbf{x}\leq
b_{j}$; obviously $|C_{U_{j}}|\leq D^{k}$ and it can be constructed in time
$\mathcal{O}(D^{k})$. Then, $\mathcal{H}=\\{C_{U_{j}}\mid j=1,\dots,m\\}$. It
is easy to verify that the feasible assignments of $I$ correspond to integer
solutions of $\mathbf{A}\mathbf{x}\leq\mathbf{b}$ and that
$G(\mathbf{A})=G(I)$. ∎

###### Proof of Theorem 30.

We apply Proposition 32 to obtain an ILP
$\mathbf{A}\mathbf{y}+\mathbf{D}\mathbf{z}+\mathbf{C}\mathbf{w}=\mathbf{d}$,
and use Proposition 34 to get an equivalent CSP instance $J^{\prime}$. Recall
that $(T,\mathcal{B})$ is a nice tree decomposition of $G$ and
$(T,\mathcal{B}^{*})$ is a tree decomposition of
$G(\mathbf{A}~{}\mathbf{D}~{}\mathbf{C})$ (and thus $G(J^{\prime})$) as
described in Proposition 32, part (3). Let $I^{\prime}$ be a CSP instance over
variables $\mathbf{y}$ with $\mathcal{H}=\\{\mathbf{y}\mid
G,\mathbf{y}\models\varphi\\}$. Clearly, $J^{\prime}$ is an extension of
$I^{\prime}$ by the fact that the polytope $P$ is an extension of
$P_{\varphi}(G)$.

Now we will add the variables $\mathbf{x}$ to $J^{\prime}$ and add constraints
in such a way that the resulting instance $J$ will be an extension of $I$, and
that it satisfies the claim of Theorem 30.

##### Stage 3: Adding variables and constraints

We introduce auxiliary binary variables $f_{v}^{i,a}$ for each $a\in V(T)$,
$i\in[\ell]$ and $v\in B(a)$, and we let Let
$f_{v}^{i,a}=\sum_{t\in\mathcal{C}}z_{a}^{t}\cdot\eta(t,a,v,i)$. For any
subset $U$ of variables of $I$, let $U_{a}$ be the set $U$ where each variable
$y_{v}^{i}$ is replaced by $f_{v}^{i,a}$. Then, for every constraint
$C_{U}\in\mathcal{H}^{\prime}$ and $w_{U}\in\mathcal{S}$ let $a\in V(T)$ be
the node such that the local scope property of $C_{U}$ and $w_{U}$,
respectively, is fulfilled by $a$, and add to $J^{\prime}$ a constraint
obtained by replacing the scope $U$ with $U_{a}$. Denote the resulting
instance $J$.

By property (2) of Proposition 32, $f_{v}^{i,a}=y_{v}^{i}$ for each $a\in
V(T)$ with $v\in B(a)$. Thus, for any constraint $C_{U}$ or $w_{U}$, replacing
its scope with $U_{a}$ does not change the set of feasible assignments, and
$J$ is an extension of $I$.

By the equivalence of
$\mathbf{A}\mathbf{y}+\mathbf{D}\mathbf{z}+\mathbf{C}\mathbf{w}=\mathbf{d}$
and $J^{\prime}$, we have that
$\|\mathcal{H}_{J^{\prime}}\|+\|\mathcal{S}_{J^{\prime}}\|\leq
f(|\varphi|,\tau)\cdot n$, and thus
$\|\mathcal{H}_{J}\|+\|\mathcal{S}_{J}\|\leq f(|\varphi|,\tau)\cdot
n+\|\mathcal{H}^{\prime}\|+\|\mathcal{S}\|$. The variables contained in $J$
and not $I$ are the $\mathbf{z},\mathbf{w}$ and $\mathbf{f}$ variables. Since
they are all binary we also have that $D_{J}=D_{I}$. It remains to show that
$\operatorname{tw}(J)\leq f(|\varphi|,\tau)+2k$. A lemma will help us see
that:

###### Lemma 35

Let $T=(I,F)$ be a rooted binary tree, let $(T,\mathcal{B})$ be a tree
decomposition of a graph $G=(V,E)$ of width $\kappa$, and let $H=(V\cup
W,E\cup Y)$ be a supergraph of $G$ such that:

  * •

$W=\bigcup_{a\in I}W_{a}$, $Y=\bigcup_{ab\in F}Y_{ab}$, all $W_{a}$ are pair-
wise disjoint, and all $Y_{ab}$ are pair-wise disjoint,

  * •

$|W_{a}|\leq\kappa^{\prime}$ for all $a\in I$,

  * •

if $a\in I$ has only child $b$, then $\bigcup Y_{ab}\subseteq(B(a)\cup
W_{a}\cup W_{b})$, and,

  * •

if $a$ has two children $b,b^{\prime}$, then $\bigcup(Y_{ab}\cup
Y_{ab^{\prime}})\subseteq(B(a)\cup W_{a}\cup W_{b}\cup W_{b^{\prime}})$.

Then there is a tree decomposition $(T,\mathcal{B}^{\prime})$ of $H$ of width
at most $\kappa+2\kappa^{\prime}$.

$W_{a}$$W_{b}$$a$$b$$W_{a}$$W_{b}$$W_{c}$$W_{d}$$W_{e}$$W_{f}$(b)(a) Figure 4.
The situation of Lemma 35. Part (a) depicts a single edge $ab\in F$ and the
requirement that edges from vertices in $W_{a}$ only connect to vertices in
$W_{a}$, $W_{b}$, $B(a)$ or $B(b)$. Part (b) depicts how $W$ and $Y$ relate to
the whole of $T$. Black points correspond to $I$, grey edges to $F$,
$W_{a},\dots,W_{f}$ are self-explanatory, and all remaining edges correspond
to sets of edges $Y_{ij}$.

###### Proof.

Let $\mathcal{B}^{\prime}$ be obtained from $\mathcal{B}$ by, for every edge
$ab\in F$, adding $W_{a}$ to the bags $B(a)$ and $B(b)$. We will verify that
$(T,\mathcal{B}^{\prime})$ is a tree decomposition of $H$ of width at most
$\kappa+2\kappa^{\prime}$; we shall denote by $B^{\prime}$ the bags of
$(T,\mathcal{B}^{\prime})$. The conditions of a tree decomposition obviously
hold for all vertices and edges of $G$, so we only check it for new vertices
and edges.

Edge condition. Let $uv\in Y_{ab}$ be an edge in $H\setminus G$ with $u\in
W_{a}$. Either $v\in B(a)$ and then $\\{u,v\\}\subseteq B(a)\cup
W_{a}\subseteq B^{\prime}(a)$, or $v\in W_{b}$ and then $\\{u,v\\}\subseteq
B(b)\cup W_{a}\subseteq B^{\prime}(b)$.

Connectedness condition. Let $v\in W_{a}$ and let $a$ have children
$b,b^{\prime}$, with possibly $b=b^{\prime}$. Notice that $v$ does not appear
in the bag of any node above $a$ and any node below $b$ and $b^{\prime}$.
Since we have added $W_{a}$ to all of $a,b$ and $b^{\prime}$, the
connectedness condition holds.

We have added to each node $b$ (except the root) two sets $W_{a}$, $W_{b}$
where $a$ is the parent of $b$, and because $|W_{a}|+|W_{b}|\leq
2\kappa^{\prime}$,
$\operatorname{tw}((T,\mathcal{B}^{\prime}))\leq\kappa+2\kappa^{\prime}$. ∎

Let us consider how the constraint graph $G(J)$ relates to $G(J^{\prime})$.
Since $J$ is obtained by adding new variables and constraints, this
corresponds to $G(J)$ being a supergraph of $G(J^{\prime})$. The vertices
$W=V(G(J))\setminus V(G(J^{\prime}))$ can be partitioned into sets $W_{a}$ for
every node $a\in V(T)$, and $|W_{a}|\leq k$. Moreover, the new edges
$Y=E(G(J))\setminus E(G(J^{\prime}))$ can also be partitioned into sets
$Y_{ab}$ for each $ab\in E(T)$, such that for each $uv\in Y_{ab}$ we have
$\\{u,v\\}\subseteq(W_{a}\cup W_{b})$, because, for each node $a\in V(T)$, the
new constraints only contain variables associated with node $a$ and its
neighbors. The tree decomposition $(T,\mathcal{B}^{*})$ of $G(J^{\prime})$ is
such that we are precisely in the situation of Lemma 35 with
$G:=G(J^{\prime})$, $H:=G(J)$,
$\kappa:=\operatorname{tw}(J^{\prime})=f^{\prime}(|\varphi|,\tau)$ and
$\kappa^{\prime}:=k+\ell\tau$, which then implies that $G(J)$ has a tree
decomposition $(T,\mathcal{B}^{\prime})$ of width
$f^{\prime}(|\varphi|,\tau))+2k+\ell\tau\leq f(|\varphi|,\tau))+2k$. ∎

##  5\. Conclusions

##### Limits of MSO extensions, other logics, and metatheorems.

We have defined extensions of MSO and extended positive and negative results
for them. There is still some unexplored space in MSO extensions: Szeider [38]
shows that ${\sf MSO}^{\sf L}$ where some of the sets of local cardinality
constraints are quantified is NP-hard already on graphs of treewidth 2. We are
not aware of a comparable result for ${\sf MSO}^{\sf G}$, and no results of
this kind are known for graphs of bounded neighborhood diversity. Also, we
have not explored other logics, as for example the modal logic considered by
Pilipczuk [37]. Also, one merit of algorithmic metatheorems is in generalizing
existing results. However, many problems [16, 19] are FPT on bounded
neighborhood diversity which are not expressible in any of the studied logics.
So we ask for a metatheorem generalizing as many such positive results as
possible.

##### Complementary Parameters and Problems.

Unlike for treewidth, taking the complement of a graph preserves its
neighborhood diversity. Thus our results apply also in the complementary
setting, where, given a graph $G$ and a parameter $p(G)$, we are interested in
the complexity (with respect to $p(G)$) of deciding a problem $P$ on the
_complement_ of $G$. While the complexity stays the same when parameterizing
by neighborhood diversity, it is unclear for sparse graph parameters such as
treewidth. It was shown very recently [14] that the Hamiltonian Path problem
admits an FPT algorithm with respect to the treewidth of the complement of the
graph. This suggest that at least sometimes this is the case and some
extension of Courcelle’s theorem deciding properties of the complement may
hold.

### Acknowledgements.

This research was supported by the project 338216 of GA UK and the grant
SVV–2017–260452. D. Knop acknowledges support by DFG, project “MaMu”, NI
369/19. M. Koutecký was partially supported by a postdoctoral fellowship at
the Technion funded by the Israel Science Foundation grant 308/18, by Charles
University project UNCE/SCI/004, and by the project 17-09142S of GA ČR. T.
Masařík was supported the project GA17-09142S of GA ČR.

## References

  * [1] Sancrey Rodrigues Alves, Konrad Kazimierz Dabrowski, Luérbio Faria, Sulamita Klein, Ignasi Sau, and Uéverton dos Santos Souza.  On the (parameterized) complexity of recognizing well-covered (r, l)-graphs.  In T.-H. Hubert Chan, Minming Li, and Lusheng Wang, editors, COCOA, volume 10043 of Lecture Notes in Computer Science, pages 423–437. Springer, 2016.
  * [2] NR Aravind, Subrahmanyam Kalyanasundaram, Anjeneya Swami Kare, and Juho Lauri.  Algorithms and hardness results for happy coloring problems.  arXiv preprint arXiv:1705.08282, 2017.
  * [3] Stefan Arnborg, Jens Lagergren, and Detlef Seese.  Easy problems for tree-decomposable graphs.  Journal of Algorithms, 12(2):308–340, June 1991.
  * [4] H. L. Bodlaender.  Treewidth: characterizations, applications, and computations.  In Proc. of WG, volume 4271 of LNCS, pages 1–14. Springer, 2006.
  * [5] Hans L. Bodlaender.  A linear time algorithm for finding tree-decompositions of small treewidth.  In Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16-18, 1993, San Diego, CA, USA, pages 226–234, 1993\.
  * [6] Édouard Bonnet and Florian Sikora.  The graph motif problem parameterized by the structure of the input graph.  Discrete Applied Mathematics, 2016.
  * [7] Robert Bredereck, Piotr Faliszewski, Rolf Niedermeier, Piotr Skowron, and Nimrod Talmon.  Elections with few candidates: Prices, weights, and covering problems.  In Proc. ADT 2015, volume 9346 of Lecture Notes Comput. Sci., pages 414–431, 2015.
  * [8] Michele Conforti, Gérard Cornuéjols, and Giacomo Zambelli.  Extended formulations in combinatorial optimization.  Annals OR, 204(1):97–143, 2013.
  * [9] Bruno Courcelle.  The monadic second-order logic of graphs I: Recognizable sets of finite graphs.  Information and Computation, 85:12–75, 1990.
  * [10] Bruno Courcelle, Johann A. Makowsky, and Udi Rotics.  Linear time solvable optimization problems on graphs of bounded clique-width.  Theory of Computing Systems, 33(2):125–150, 2000.
  * [11] Bruno Courcelle and Mohamed Mosbah.  Monadic second-order evaluations on tree-decomposable graphs.  Theoretical Computer Science, 109(1–2):49–82, 1 March 1993.
  * [12] Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh.  Parameterized Algorithms.  Springer, 2015.
  * [13] Pavel Dvořák, Dušan Knop, and Tomáš Toufar.  Target Set Selection in Dense Graph Classes.  CoRR, 1610.07530, October 2016.
  * [14] Pavel Dvořák, Dušan Knop, and Tomáš Masařík.  Anti-path cover on sparse graph classes.  In Jan Bouda, Lukáš Holík, Jan Kofroň, Jan Strejček, and Adam Rambousek, editors, Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Telč, Czech Republic, 21st-23rd October 2016, volume 233 of Electronic Proceedings in Theoretical Computer Science, pages 82–86. Open Publishing Association, 2016.
  * [15] Michael R. Fellows, Guillaume Fertin, Danny Hermelin, and Stéphane Vialette.  Upper and lower bounds for finding connected motifs in vertex-colored graphs.  J. Comput. Syst. Sci, 77(4):799–811, 2011.
  * [16] Jirí Fiala, Tomáš Gavenčiak, Dušan Knop, Martin Koutecký, and Jan Kratochvíl.  Fixed parameter complexity of distance constrained labeling and uniform channel assignment problems - (extended abstract).  In Thang N. Dinh and My T. Thai, editors, COCOON, volume 9797 of Lecture Notes in Computer Science, pages 67–78. Springer, 2016.
  * [17] Eugene C. Freuder.  Complexity of $K$-tree structured constraint satisfaction problems.  In Proceedings of the Eighth National Conference on Artificial Intelligence - Volume 1, AAAI’90, pages 4–9. AAAI Press, 1990.
  * [18] Markus Frick and Martin Grohe.  The complexity of first-order and monadic second-order logic revisited.  Ann. Pure Appl. Logic, 130(1-3):3–31, 2004.
  * [19] Robert Ganian.  Using neighborhood diversity to solve hard problems.  CoRR, abs/1201.3091, 2012.
  * [20] Robert Ganian and Jan Obdržálek.  Expanding the expressive power of monadic second-order logic on restricted graph classes.  In Thierry Lecroq and Laurent Mouchard, editors, IWOCA, volume 8288 of Lecture Notes in Computer Science, pages 164–177. Springer, 2013\.
  * [21] Luisa Gargano and Adele A. Rescigno.  Complexity of conflict-free colorings of graphs.  Theoretical Computer Science, 566:39–49, February 2015.
  * [22] Georg Gottlob, Reinhard Pichler, and Fang Wei.  Monadic datalog over finite structures with bounded treewidth.  In Proc. of the 26th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS), pages 165–174, 2007.
  * [23] Martin Grohe and Stephan Kreutzer.  Methods for algorithmic meta theorems.  Model Theoretic Methods in Finite Combinatorics, 558:181–206, 2011\.
  * [24] Ton Kloks.  Treewidth: Computations and Approximations, volume 842 of Lecture Notes in Computer Science.  Springer, 1994.
  * [25] Joachim Kneis, Alexander Langer, and Peter Rossmanith.  Courcelle’s theorem - A game-theoretic approach.  Discrete Optimization, 8(4):568–594, 2011.
  * [26] Dušan Knop, Tomáš Masařík, and Tomáš Toufar.  Parameterized complexity of fair vertex evaluation problems.  arXiv preprint arXiv:1803.06878, 2018.
  * [27] Dušan Knop, Martin Koutecký, Tomáš Masařík, and Tomáš Toufar.  Simplified algorithmic metatheorems beyond MSO: treewidth and neighborhood diversity.  In Hans L. Bodlaender and Gerhard J. Woeginger, editors, Graph-Theoretic Concepts in Computer Science - 43rd International Workshop, WG 2017, Eindhoven, The Netherlands, June 21-23, 2017, Revised Selected Papers, volume 10520 of Lecture Notes in Computer Science, pages 344–357. Springer, 2017.
  * [28] Phokion G. Kolaitis and Moshe Y. Vardi.  Conjunctive-query containment and constraint satisfaction.  Journal of Computer and System Sciences, 61(2):302 – 332, 2000\.
  * [29] Petr Kolman, Martin Koutecký, and Hans R. Tiwary.  Extension complexity, MSO logic, and treewidth, July 12 2016.  Short version presented at SWAT 2016.
  * [30] Petr Kolman, Bernard Lidický, and Jean-Sébastien Sereni.  On Fair Edge Deletion Problems, 2009.
  * [31] Michael Lampis.  Algorithmic meta-theorems for restrictions of treewidth.  Algorithmica, 64(1):19–37, 2012.
  * [32] Michael Lampis.  Model checking lower bounds for simple graphs.  Logical Methods in Computer Science, 10(1), 2014.
  * [33] Hendrik W. Lenstra Jr.  Integer programming with a fixed number of variables.  Math. Oper. Res., 8(4):538–548, 1983.
  * [34] Leonid Libkin.  Elements of Finite Model Theory.  Springer-Verlag, Berlin, 2004.
  * [35] Tomáš Masařík and Tomáš Toufar.  Parameterized complexity of fair deletion problems.  In International Conference on Theory and Applications of Models of Computation, pages 628–642. Springer, 2017.
  * [36] Jiří Matoušek and Jaroslav Nešetřil.  Invitation to Discrete Mathematics (2. ed.).  Oxford University Press, 2009.
  * [37] Michal Pilipczuk.  Problems parameterized by treewidth tractable in single exponential time: A logical approach.  In Filip Murlak and Piotr Sankowski, editors, MFCS, volume 6907 of Lecture Notes in Computer Science, pages 520–531. Springer, 2011.
  * [38] Stefan Szeider.  Monadic second order logic on graphs with local cardinality constraints.  ACM Trans. Comput. Log, 12(2):12, 2011.
  * [39] René van Bevern, Andreas Emil Feldmann, Manuel Sorge, and Ondřej Suchý.  On the parameterized complexity of computing balanced partitions in graphs.  Theory Comput. Syst, 57(1):1–35, 2015.