MSOL optimization problems on graphs of bounded cliquewidth, with cardinality predicates

CMSOL is Counting Monadic Second Order Logic, i.e. a logic of graphs where the domain is the set of vertices and edges, there are predicates for vertex-vertex adjacency and edge-vertex incidence, there is quantification over edges, vertices, edge sets and vertex sets, and there is a predicate $\textrm{Card}_{n,p}(S)$ which expresses whether the size of $S$ is $n$ modulo $p$.

Courcelle's famous theorem states that if $\Pi$ is a property of graphs expressible in CMSOL, then for every graph $G$ of treewidth at most $k$ it can be decided in linear time whether $\Pi$ holds, provided that a tree decomposition of $G$ is given in the input. Later versions of the theorem dropped the requirement that a tree decomposition is given in the input (because one can be computed with Bodlaender's algorithm), and also allowed optimization instead of merely decision; i.e. given a MSOL formula $\phi(S)$ we can also compute the largest or smallest set $S$ which satisfies $\phi(S)$.

My question concerns the adaptation of Courcelle's theorem to graphs of bounded cliquewidth. There is a similar theorem saying that if you have a MSOL1 which allows quantification over vertices, edges, vertex sets but not edge sets then given a graph $G$ of cliquewidth $k$ (with given clique-expression), for every fixed $k$ it can be decided in linear time whether graph $G$ satisfies some MSOL1 formula $\phi$; all references I have seen point to

Linear Time Solvable Optimization Problems on Graphs of Bounded Clique-Width by Courcelle, Makowsky and Rotics, Theory of Computing Systems, 2000.

I have tried to read the paper, but it is not self-contained with respect to the exact definition of MSOL1 and it is frankly hard to read. I have two questions with respect to what exactly is possible to optimize in FPT, parameterized by the cliquewidth of the graph, if a clique expression is given in the input.

• Does MSOL1 allow the $\textrm{Card}_{n,p}(S)$ predicate for testing the size of a set modulo some number?
• Is it possible to find a minimum / maximum size set $S$ which satisfies a MSOL1 formula $\phi(S)$ in FPT parameterized by cliquewidth, when the expression is given?

For both these questions I would also like to know what the correct references are to cite when claiming these results. Thanks in advance!

• I tried to modify some of your article, sorry about that. Because I'm pretty interested in your question, but still after the modification I'm not sure if I understand you ideas correctly. So, do you mean that you need the exact definition of MSOL1, and the existance of predicate and an FPT of an optimization problem? – Hsien-Chih Chang 張顯之 Jan 24 '11 at 14:48
• Ideally what I would like to hear is that for each fixed $MSOL_1$ formula $\phi(S)$, where $S$ is a vertex set variable and the formula $\phi$ involves Card$_{n,p}(S)$ predicates, there is an algorithm which given a graph G and a clique-expression of width k, computes a minimum-size set $S$ which satisfies $\phi(S)$ in $f(k) |V(G)|^{O(1)}$ for some arbitrary function $f$ (or outputs that no set $S$ satisfies $\phi$). – Bart Jansen Jan 24 '11 at 16:52
• Bruno Courcelle's draft book volumes might be useful: see labri.fr/perso/courcell/ActSci.html under "Graph structure and monadic second-order logic, a language theoretic approach". – András Salamon Jan 24 '11 at 19:42
• Thanks; this at least settles part 1) of the problem, since his Theorem 6.4 in the first part of the book says: For all finite sets K and L of vertex and edge labels, the model-checking problem of a Counting MSOL1 formula is fixed-parameter cubic with respect to the parameter cliquewidth(G) + size of the formula. – Bart Jansen Jan 25 '11 at 13:48

2 Answers

After asking around some more, it seems that the answers to 1) and 2) are both YES. Optimizing the cardinality of a set is possible in LinEMSOL (as mentioned by Martin Lackner); as I have been told, the existence of the cardinality predicates is no problem since they can be efficiently handled by finite-state tree automatons, which should follow (more explicitly than in the originally referenced paper) from On parse trees and Myhill-Nerode-type tools for handling graphs of bounded rank-width.

http://www.labri.fr/perso/courcell/Textes1/BC-Makowsky-Rotics(2000).pdf (which is the paper you mentioned but a better readable version) defines LinEMSOL (Definition 10). LinEMSOL allows for MSO1 optimization problems and Theorem 4 states that such problems are fixed-parameter tractable with regard to clique-width. So the answer to your second bullet/question should be yes.

Concerning the first bullet: In "Vertex-minors, monadic second-order logic, and a conjecture by Seese" by Bruno Courcelle and Sang-il Oum the authors write that "It can be proved that no MS formula φ(X) can express, in every structure, that a set X has even cardinality [10]" where [10]="Courcelle, The monadic second-order logic of graphs"

Hope that helps

• Thanks for the insight, but the fact that no MS formula (in general) can express whether a set has even cardinality is not really relevant here, since the question is about the Counting MSOL language which has special predicates added that explicitly allow testing the cardinality of a set modulo some fixed number; hence in the Counting MSOL language it is possible to express the even-ness of a set, and the question was whether we can efficiently find the smallest/biggest set satisfying a sentence in Counting MSOL parameterized by cliquewidth. Thanks anyway! – Bart Jansen Feb 8 '11 at 9:33
• You are of course right. I just wanted to make the point that the paper you mentioned does not cover CMSOL. (I do not know of a result that does that.) – Martin Lackner Feb 8 '11 at 12:46