Consider the following problem.

Given a graph $G=(V,E)$, and two positive integers $k$ and $\gamma$, decide if there is a set of new edges to be added such that $|E'|\le k$, and any subset $V'\subseteq V$ of size $\gamma$ is not a vertex cover of $(V, E\cup E')$.

i.e., can we add at most $k$ edges to ensures that the minimum vertex cover has a size at least $\gamma+1$.

I am trying to write this problem in Graph-MSOL (monadic second-order logic).

$$C(V, E, \gamma) := \exists x_1 \exists x_2 \ldots \exists x_\gamma (uv \in E \implies (\lor_{i=1}^\gamma ((u=x_i \lor v=x_i))))$$ which defines a vertex cover of size $\gamma$.

$$ \exists e_1\exists e_2 \ldots \exists e_k (\lnot(C(V, E \cup \{e_1,\ldots,e_k\}, \gamma) )) $$ corresponds to adding $k$ edges so that there does not exist a vertex cover of size $\gamma$.

Substituting the definition of $C$ in the last line, we can write a single large MSOL as

$$ \exists e_1\exists e_2 \ldots \exists e_k \left ( \lnot \left (\vphantom{\int^A} \exists x_1 \exists x_2 \ldots \exists x_\gamma \left( \left (\vphantom{\bar{A^k}}(uv \in E) \lor \left (\lor_{j=1}^k (uv=e_j)\right) \right) \implies \left (\vphantom{\bar{A^k}}\lor_{i=1}^\gamma \left ((u=x_i) \lor (v=x_i)\right)\right) \right) \right ) \right ) $$.

Is the above a valid Graph MSOL? Consequently, does Courcelle's theorem now imply that the above problem is FPT for graphs with fixed treewidth?

  • $\begingroup$ Related question: cs.stackexchange.com/questions/168478/… $\endgroup$
    – Lisa E.
    Commented Jun 7 at 18:36
  • $\begingroup$ Are $k$ and $\gamma$ parameters, or fixed constants? In other words, is a hypothetical algorithm of time complexity $O(c^{\mathrm{tw}} n^{O(k+\gamma)})$ regarded as FPT? $\endgroup$
    – pcpthm
    Commented Jun 8 at 5:41
  • $\begingroup$ $k$ and $\gamma$ are parameters. $\endgroup$
    – Lisa E.
    Commented Jun 8 at 12:46
  • $\begingroup$ The idea looks good. I'm not sure you can use $\exists e_i$ for a non-edge $e_i$, and that you can use $uv = e_j$ (maybe it's ok, but to my knowledge these are not usually part of the specifications). To be sure, I'd suggest defining the pairs of vertices forming new edges explicitly, e.g. $\exists u_1 \exists v_1 \exists u_2 \exists v_2 \ldots$ and then require $u_j = x_i \vee v_j = x_i$ later on. $\endgroup$ Commented Jun 12 at 13:53
  • $\begingroup$ @ManuelLafond - I am not sure, I fully understand it. So, do you mean that the Courcelle's theorem now implies FPT of the above problem? Mind elaborating in an answer? $\endgroup$
    – Lisa E.
    Commented Jun 14 at 13:32

1 Answer 1


You can use CMSOL which allows cardinality predicates. See 5.2.6 in this report. This is authored by Courcelle himself. You can refer the original paper by Courcelle too, but it is a bit more terse.

In the form you have written above, the length of the formula increases with $k$ and $\gamma$. However, by using cardinality predicate, you can indeed decide all these in linear time, provided the tree width is fixed.

$$ \exists U \left( (\operatorname{card}(U) =k) \bigwedge \left( \neg \left( \exists X \left( (\operatorname{card}(X) = \gamma) \land (\beta(u, v, E, U, X)) \right)\vphantom{\sum^n} \right)\vphantom{\int} \right)\vphantom{\int_x^{x^2}} \right) $$ where $$ \alpha(u,v,E,U) = ((u,v) \in E )\lor ((u,v) \in U)\\ \beta(E,U, X) = \forall u\in V \;\forall v \in V \left( \vphantom{\int}\left( \alpha(u,v,E,U) \right) \to \left((u\in X ) \lor (v\in X) \right)\right) $$. Here,

  • $\alpha(u,v,E,U)$ means, $(u,v)$ is either an edge in $E$ or in $X$.
  • $\beta(E, U, X)$ means $X$ is a vertex cover of a graph with edge set $E\cup U$.
  • The part after the big AND in the main formula ensures that there does not exist a vertex cover of size $\gamma$.
  • The part before the big AND ensures that there is a set $U$ of edges which achieves that.

Because of the above representation, we have FPT w.r.t. tree width.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.