MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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$.

Please help formulate this problem in MSO.

share|cite|improve this question
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
up vote 4 down vote accepted

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))$

share|cite|improve this answer
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.

share|cite|improve this answer
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.

share|cite|improve this answer
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 ( ). 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?)

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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