14
$\begingroup$

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!

Improve this question
$\endgroup$
4
  • $\begingroup$ 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? $\endgroup$
    – Hsien-Chih Chang 張顯之
    Jan 24, 2011 at 14:48
  • $\begingroup$ 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$). $\endgroup$
    – Bart Jansen
    Jan 24, 2011 at 16:52
  • 4
    $\begingroup$ 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". $\endgroup$
    – András Salamon
    Jan 24, 2011 at 19:42
  • 2
    $\begingroup$ 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. $\endgroup$
    – Bart Jansen
    Jan 25, 2011 at 13:48

2 Answers 2

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
4
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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! $\endgroup$
    – Bart Jansen
    Feb 8, 2011 at 9:33
  • $\begingroup$ 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.) $\endgroup$
    – Martin Lackner
    Feb 8, 2011 at 12:46

Your Answer

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

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