Lógica monádica de segundo orden (MSO) sobre grafos

Question

Dado un gráfico de conflicto $G = (V, E)$ un hombre tiene que transportar un conjunto $V$ de artículos/vértices a través del río. Dos elementos están conectados por un borde en $E$ Si son conflictivos y, por lo tanto, no pueden dejarse solos juntos sin supervisión humana. El barco disponible tiene capacidad $b\geq 1$ y por lo tanto puede llevar al hombre junto con cualquier subconjunto de como máximo $b$ artículos. Una programación factible es una secuencia finita de triples $(L_1, B_1, R_1),\dots, (L_s, B_s, R_s)$ de subconjuntos del conjunto de elementos V que satisfacen las siguientes condiciones (FS1)-(FS3). El entero impar $s$ se llama la longitud del horario.

(FS1) Para cada $k$ los conjuntos $L_k, B_k, R_k$ forman una partición de V . Los conjuntos $L_k$ y $R_k$ forman conjuntos estables en $G$ . El conjunto $B_k$ contiene como máximo $b$ elementos.

(FS2) La secuencia comienza con $L_1 \cup B_1 = V$ y $R_1 = \emptyset$ y la secuencia termina con $L_s = \emptyset$ y $B_s\cup R_s = V$ .

(FS3) Para incluso $k \geq 2$ tenemos $B_k\cup R_k = B_{k-1} \cup R_{k-1}$ y $L_k = L_{k-1}$ . Para impar $k \geq3$ tenemos $L_k\cup B_k= L_{k-1}\cup B_{k-1}$ y $R_k = R_{k-1}$ .

Resultado conocido: $VertexCover(G) \geq b \geq VertexCover(G)+1$ .

Por favor, ayude a formular este problema en MSO.

Answer 1

Tal vez haya una solución. Pero, para ello asumo que hay un límite superior en el número de rondas necesarias, digamos n, y que el valor b está fijado de antemano. Entonces, existe la siguiente fórmula EMSO,

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

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

Si i es incluso :
$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})$

Si i es impar (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})$

Así que si podemos demostrar que si hay una solución entonces hay una solución de máximo n rondas que depende del tamaño del gráfico entonces creo que tenemos una solución.

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

menosqueb(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

No estoy seguro de si es definitivamente expresable en MSO o no.

Answer 3

Puede encontrar artículos sobre el problema de la teoría de grafos buscando "grafo de número Alcuin".

Una referencia a una definición clara de la Lógica Monádica de Segundo Orden (y especialmente, algunos ejemplos de lo que puede expresar típicamente) sería útil para responder a la pregunta.

Answer 4

En MSOL tal y como yo lo conozco no se podría expresar esto por la aburrida razón de que no se puede decir en MSOL "el conjunto B_i contiene como máximo b elementos" (paramétricamente en b). ¿Quizás deberías decir con precisión en qué lenguaje quieres que se exprese esto? (¿Y qué es exactamente lo que quieres que se exprese: que una solución dada es factible?)