## 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 ≥ 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 (L1, B1, R1), (L2, B2, R2), . . . , (Ls, Bs, Rs) 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 Lk, Bk, Rk form a partition of V . The sets Lk and Rk form stable sets in G. The set Bk contains at most b elements.

(FS2) The sequence starts with L1 ∪ B1 = V and R1 = ∅, and the sequence ends with Ls = ∅ and Bs ∪ Rs = V .

(FS3) For even k ≥ 2, we have Bk ∪ Rk = Bk-1 ∪ Rk-1 and Lk = Lk-1. For odd k ≥ 3, we have Lk ∪ Bk = Lk-1 ∪ Bk-1 and Rk = Rk-1.

Known Result: VertexCover(G) ≤ b ≤ VertexCover(G)+1.

-
Sounds a bit like a homework problem. – supercooldave Jun 26 2010 at 9:14
Why do you believe this is expressible in MSO? – François G. Dorais Jun 26 2010 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 2010 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 2010 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 2010 at 20:51
Even CMSO is fine. – Esha Jul 17 2010 at 6:58

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”

-

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 2010 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 2010 at 8:07
Gerhard: You can always comment on your own post. – François G. Dorais Jun 29 2010 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 2010 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 2010 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 2010 at 6:30