Question

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 (L₁, B₁, R₁), (L₂, B₂, R₂), . . . , (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₁ ∪ B₁ = V and R₁ = ∅, and the sequence ends with L_s = ∅ and B_s ∪ R_s = V .

(FS3) For even k ≥ 2, we have B_k ∪ R_k = B_k-1 ∪ R_k-1 and L_k = L_k-1. For odd k ≥ 3, we have L_k ∪ B_k = L_k-1 ∪ B_k-1 and R_k = R_k-1.

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

Please help formulate this problem in MSO.

Answer 1

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

Answer 2

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

Answer 3

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.

Answer 4

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

Answer 5

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”