MSOL and Courcelle's theorem for maximum clique

Question

The Clique Problem is known to be NP-complete but is known to be fixed-parameter-tractable (FPT) if the treewidth of the underlying graph is fixed.

The traditional proof is by a dynamic programming algorithm given a tree decomposition. The tree decomposition itself can be found in poly-time if the treewidth is fixed.

In contrast, I am trying to show the FPTness of the problem by writing it as an MSOL and then appealing to Courcelle's theorem.

The decision version of the problem is: Given a graph $G=(V,E)$ and $k> 1$, decide if the graph has a clique of size $k$.

Here is my attempt at writing the MSOL.

$$ \exists v_1 \exists v_2 \ldots \exists v_k \left ( \bigwedge_{\substack{i,j\in \{1,...,k\} \\ i \neq j}} \operatorname{adj}(v_i, v_j) \right ) $$

However, this formula is not of length invariant with $k$. As $k$ grows, the formula becomes longer (the $\bigwedge_{\dots}$ is only an abbreviation). Is Courcelle's theorem still applicable, with the MSOL written as above, to show that the clique problem is FPT with treewidth?

If not, is there an alternative way of writing the MSOL, so that we can use the Courcelle's theorem to show that the clique problem is FPT with treewidth?

Answer 1

Essentially no.

Let $k$ be the size of the clique and $t$ a bound on the tree-width. Then, from Courcelle's theorem, one can derive an FPT algorithm with parameter $(k,t)$. In order to see, whether that can be improved to parameter just $t$, let us recap the details.

The question of clique can be formulated in MSO. For each $k$, there is a formula $\varphi_k$ such that the graph satisfies $\varphi_k$ if and only if it has a clique of size $k$. The formula from the question is perfectly fine for the purpose. The formula is not constant: It depends on $k$. As a consequence, for varying $k$, an infinite number of formulae is needed.

From $\varphi_k$ and $t$, one constructs a tree-automaton that works on tree-decompositions of width $\leq t$ and checks whether the so-decomposed graph satisfies $\varphi_k$. Another way to look at it is that one constructs a dynamic programming algorithm.

How large do the automata become? In general, i.e. is for general MSO formulae $\varphi$, no elementary function in $|\varphi|$ bounds the number of states of the corresponding automaton $\mathcal A$. So, we are very far from a polynomial bound.

On the other hand, the formulae $\varphi_k$ are not "general". In fact they have a quite simple structure: They are conjunctive queries. In their case, an exponential number of states suffices. This is a big improvement over "no elementary bound", but of course it is still too much.

What if we do not use automata? They might be a detour and some other approach for proving Courcelle's theorem might be more efficient, right? No. Model checking (that is checking whether a given graph satisfies a given formula) for conjunctive queries is essentially the same problem as CSP (constraint satisfaction) and as graph homomorphism. Let us view the question from the point of view of the latter. A graph $G$ has a clique of size $k$ if and only if there is a homomorphism $K_k\to G$. If there was some more efficient version of Courcelle's theorem, then the graph homomorphism problem would be in FPT when parameterized only by the tree-width of the right-hand side graph. On the other hand, fixing the right-hand side to $K_3$ (that is asking, for a given graph $G$, whether there is a homomorphism $G\to K_3$) is the problem of 3-colourability. Which is known to be NP-complete. Hence (unless P=NP), graph homomorphism is not in FPT when parameterized as above.

In summary: No, FPT-ness of clique when parameterized just by $t$ cannot be derived from Courcelle's theorem. Yet above I wrote "essentially no". Why is that? One can exploit the fact that a graph of tree-width $t$ cannot have a clique of size $>t+1$. Then, one would use $\varphi_k$ as above in case $k\leq t+1$ and the formula $\bot$ otherwise. Then, the formula in use is bounded by a function in $t$. Hence, FPT with parameter $t$.

Yet, if we allow use of that fact, then let us do it properly: For any clique in a graph, any tree decomposition must have a bag which covers the clique whole. So, given the tree decomposition, we do not need Courcelle's theorem, automata, or dynamic programming any more. We just iterate over the bags and check these bags for cliques.

EDIT

The answer becomes yes for a different meta-theorem, which builds upon the techniques sketched above. I don't think I have actually seen it in the literature, but from today's perspective it is so straightforward that I am certain somebody must have published it somewhere by now. It goes like this:

Let $\varphi(X)$ be an MSO formula in the language of graphs with a free monadic variable $X$. Then, the following problem is in FPT when parameterized by the tree-width of $G$:

Decide, given a graph $G$ and a natural number $n$, whether there is a set $S$ of vertices of $G$, such that

• $|S|=n$, and
• $(G,S)$ satisfies $\varphi$.

For the clique problem, one would use $\varphi = \forall x\forall y((Xx \wedge Xy \wedge \neg x=y) \to Exy)$, where $E$ is the edge predicate. $\varphi$ says that $X$ is a clique.

Proof sketch:

From $\varphi$, derive a tree automaton. The tree it works on would encode tree decompositions (as for Courcelle's theorem) plus the predicate $X$. That is, it encodes which vertices belong to $X$.

Using dynamic programming, compute for each bag $b$ of the tree decomposition the set of pairs $(s,m)$, for which there is a set $S$ of vertices, such that

• $s$ is a state of the automaton,
• $m=|S|$,
• all vertices of $S$ are covered in the subtree rooted at $b$, and
• when $S$ is used for $X$, the automaton can be in state $s$ for $b$.

Answer 2

The formula as stated in the question has to modified before Courcelle's theorem can be applied to prove FPT w.r.t. tree width.

Courcelle's theorem allows a cardinality predicate. i.e., you can quantify over sets, and necessitate that their cardinality is $k$. For example, you are allowed to write $\exists X(|X|=k)$, in the MSOL (strictly CMSOL) allowed. So, you can rewrite your formula as $$ \exists X \left( (|X| \ge k )\land \left( \bigwedge_{u,v\in X; u\neq v}\operatorname{adj}(u,v) \right ) \right). $$

Now, the length of this formula is fixed with respect to $k$. Courcelle's theorem gives you an FPT w.r.t. tree width.

P.S. The discussion here might be of interest.

Answer 3

Here, your formula size is $O(k^2)$, which will give you an upper bound on the existence of any FPT algorithms through Courcelle's theorem. See this reference (§4.2 on page 17) for more details.