MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

3 added 8 characters in body

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

2 added 233 characters in body

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 B_{k-1} \vee x \in L_{k-1}) \Rightarrow XOR(x \in L_{k},x \in B_{k}))) \wedge lessthanb(B_i)$ $\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))$

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.