# Monadic Second Order (MSO) logic on graphs

Given a conflict graph $G = (V, E)$, a man has to transport a set $V$ of items/vertices across the river. Two items are connected by an edge in $E$, if they are conflicting and thus cannot be left alone together without human supervision. The available boat has capacity $b\geq 1$, and thus can carry the man together with any subset of at most $b$ items. A feasible schedule is a finite sequence of triples $(L_1, B_1, R_1),\dots, (L_s, B_s, R_s)$ of subsets of the item set V that satisfies the following conditions (FS1)–(FS3). The odd integer $s$ is called the length of the schedule.

(FS1) For every $k$, the sets $L_k, B_k, R_k$ form a partition of V . The sets $L_k$ and $R_k$ form stable sets in $G$. The set $B_k$ contains at most $b$ elements.

(FS2) The sequence starts with $L_1 \cup B_1 = V$ and $R_1 = \emptyset$, and the sequence ends with $L_s = \emptyset$ and $B_s\cup R_s = V$.

(FS3) For even $k \geq 2$, we have $B_k\cup R_k = B_{k-1} \cup R_{k-1}$ and $L_k = L_{k-1}$. For odd $k \geq3$, we have $L_k\cup B_k= L_{k-1}\cup B_{k-1}$ and $R_k = R_{k-1}$.

Known Result: $VertexCover(G) \geq b \geq VertexCover(G)+1$.

-
Sounds a bit like a homework problem. – supercooldave Jun 26 '10 at 9:14
This is not a homework problem.. This problem is NP-hard on general graphs. But has polynomial time solution for some special classes. Just like the classic Gupta-Vizing's theorem of Graph coloring, where number of colors required is either D (highest degree) or D+1, but still the problem is NP-Complete. This is in fact a generalization of the River crossing problem, which appeared in "Propositiones ad acuendos iuvenes” – Esha Jun 26 '10 at 14:44
Why do you believe this is expressible in MSO? – François G. Dorais Jun 26 '10 at 20:28
Even CMSO is fine as CMSO logic is provably a strict extension of MSO logic, since it is not definable in pure MSO for arbitrary structures. But nevertheless CMSO-problems for structures of bounded tree-width can be reduced to MSO-problems for binary trees since CMSO logic is definable in MSO logic for binary trees. – Esha Jul 17 '10 at 7:02

Maybe there is a solution. But, for that I assume there is an upper bound in the number of rounds needed, say n, and that the value b is fixed upfront. Then, there is the following EMSO formula,

$\exists L_{1} \exists B_{1} \exists R_{1} ... \exists L_{n} \exists B_{n} \exists R_{n} \phi(L_{1},B_{1},R_{1} ...,L_{n},B_{n},R_{n})$

where $\phi = Seq_{1} \wedge Seq_{2} ...\wedge Seq_{n}$

$Seq_{1}$=$\forall x (XOR(x\in L_{1},x \in B_{1})) \wedge empty(R_{1}) \wedge$ $lessthanb(B_1) \wedge IndSet(L_{1})$

If i is even :
$Seq_{i} = empty(L_{i-1}) \vee (equals(L_{i-1},L_{i})\wedge \forall x ((x \in B_{k-1} \vee x \in R_{k-1})$ $\Rightarrow XOR(x \in B_{k},x \in R_{k}))) \wedge lessthanb(B_i) \wedge IndSet(L_{i}) \wedge IndSet(R_{i})$

If i is odd (i $\geq$ 3):
$Seq_{i}$ = $empty(L_{i-1}) \vee (equals(R_{i-1},R_{i})\wedge \forall x ((x \in B_{k-1} \vee x \in L_{k-1})$ $\Rightarrow XOR(x \in L_{k},x \in B_{k}))) \wedge lessthanb(B_i) \wedge IndSet(L_{i}) \wedge IndSet(R_{i})$

$Seq_{n} = empty(L_{n-1})$

So if we can prove that if there is a solution then there is a solution of maximum n rounds which is dependent on the size of the graph then I think we have a solution.

empty(X) = $\forall x \neg(x\in X)$

lessthanb(X) = $\exists x_{1} ... \exists x_{b} (\wedge_{i \neq j}\neg(x_{i} = x_{j})) \forall x (x \in X) \rightarrow (x=x_{1} \vee... \vee x=x_{b})$

IndSet(X) = $\forall x,y \in X \neg(R(x,y))$

-
Thanks a lot. Yes, there is an upperbound on the number of rounds,n = stability number of the graph. – Esha Jun 29 '10 at 15:46
I don't think you need a bound on the number of rounds ($s$) at all. Monadic second-order logic can express the existence of (paths in a graph between two given vertices, and the same method should allow, for each $b$, expression of "there exists a solution with a boat of size $b$". The difficulty is that monadic logic can't count, so it is not possible to directly use $b$ as a variable. – T.. Jun 29 '10 at 20:51
Even CMSO is fine. – Esha Jul 17 '10 at 6:58

I am not sure whether it is definitely expressible in MSO or not.

-
This should be a comment instead of an answer. – François G. Dorais Jun 28 '10 at 14:05
Vote his question and answer up, and eventually Esha may get enough reputation to comment. Gerhard "Ask Me About System Design" Paseman, 2010.06.29 – Gerhard Paseman Jun 29 '10 at 8:07
Gerhard: You can always comment on your own post. – François G. Dorais Jun 29 '10 at 12:35

You can find papers on the graph theoretic problem by searching for "Alcuin number graph".

A reference to a clear definition of Monadic Second-Order Logic (and especially, some examples of what it can typically express) would be helpful for answering the question.

-
This is the generalized Alcuin Number problem.. – Esha Jun 29 '10 at 11:55
It is identical --- the problem statement in this question is a direct copy of a 150-word block of text from page 2 of the paper --- to the problem considered in "The Alcuin Number of a Graph" by Csorba, Hurken and Woeginger ( renyi.hu/~csp/alcuin.pdf ). They include references to the state of the art circa 2008. I think a lot of people who understand graph theory don't know monadic logic so it would help if you explained what other properties are typically expressible in MSO. The main one that I know is "vertices $v$ and $w$ are connected by a path". – T.. Jun 29 '10 at 18:07

In MSOL as I know it one could not express this for the boring reason that you can't say in MSOL "set B_i contains at most b elements" (parametrically in b). Maybe you should say precisely what language you want this expressed in? (And what exactly you want expressed: that a given solution is feasible?)

-
Yes, I precisely want to express that for any given graph there is a feasible schedule, either with b=VertexCover(G) or b=VertexCover(G)+1. – Esha Jul 16 '10 at 6:30