What is the parameterized complexity of following model checking problem? Input: Graph $G$ and formula $\varphi_1(\vec x),\varphi_2(\vec x)$ 

Parameter: $tw(G)+|\varphi_1|+|\varphi_2|$

Problem: Decide if $|\varphi_1(G)|=|\varphi_2(G)|$



where $tw(G)$ is the treewidth of $G$ and $\varphi(G):=\{\vec a|(G,\vec a)\models\varphi\}$.

What is the parametrized complexity of this problem for $\varphi_i\in FO$ or $\varphi_i\in MSO$?
This problem is $\mathsf{FPT}$ for $\varphi_i \in MSO$ (and hence also for $\varphi_i \in FO$).

More precisely, Courcelle et al. prove in [1] the following:


  Theorem [1, Thm. 32]
  Let $\mathcal{C}$ be a class of graphs which is of bounded tree-width $k$.
  Then any $MSO_2$ definable counting problem, given by $\varphi$, can be solved in time $c_k \cdot \mathcal{O}(|V| + |E|)$, where $c_k$ is a constant which depends only on $\varphi$ and $k$.


$MSO_2$ stands for monadic second-order logic where the universe is $V \cup E$ (vertices and edges), and we are given a binary relation $R(v,e)$ for the incidence between a vertex $u$ and an edge $e$. This is a quite natural representation of graphs, sufficiently powerful to e.g. define Hamiltonicity.

[1]: B.Courcelle, J.A.Makowsky, U.Rotics. On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic. Discrete Applied Mathematics 108, pp. 23-52 (2001)