Teorema de Courcelle

En el estudio de algoritmos de grafos , el teorema de Courcelle es la afirmación de que cada propiedad de grafo definible en la lógica monádica de segundo orden de grafos puede decidirse en tiempo lineal en grafos de ancho de árbol acotado . ^{[1] [2] [3]} El resultado fue demostrado por primera vez por Bruno Courcelle en 1990 ^[4] y redescubierto independientemente por Borie, Parker y Tovey (1992). ^[5] Se considera el arquetipo de los metateoremas algorítmicos . ^{[6] [7]}

En una variación de la lógica de grafos monádicos de segundo orden conocida como MSO ₁ , el grafo se describe mediante un conjunto de vértices y una relación de adyacencia binaria , y la restricción a la lógica monádica significa que la propiedad del grafo en cuestión puede definirse en términos de conjuntos de vértices del grafo dado, pero no en términos de conjuntos de aristas o conjuntos de tuplas de vértices.${\displaystyle \operatorname {adj} (.,.)}$

Como ejemplo, la propiedad de un grafo que es coloreable con tres colores (representados por tres conjuntos de vértices , , y ) puede definirse por la fórmula monádica de segundo orden con la convención de nomenclatura de que las variables en mayúsculas denotan conjuntos de vértices y las variables en minúsculas denotan vértices individuales (de modo que una declaración explícita de cuál es cuál puede omitirse de la fórmula). La primera parte de esta fórmula asegura que las tres clases de color cubran todos los vértices del grafo, y el resto asegura que cada una forme un conjunto independiente . (También sería posible agregar cláusulas a la fórmula para asegurar que las tres clases de color sean disjuntas, pero esto no hace ninguna diferencia en el resultado). Por lo tanto, por el teorema de Courcelle, la 3-colorabilidad de grafos de ancho de árbol acotado puede probarse en tiempo lineal.${\estilo de visualización R}$${\estilo de visualización G}$${\estilo de visualización B}$$${\displaystyle {\begin{aligned}\existe R\ \existe G\ \existe B\ {\Bigl (}&\para todos v\ (v\en R\vee v\en G\vee v\en B)\wedge {}\\&\para todos u\ \para todos v\ {\bigl (}(u\en R\wedge v\en R)\rightarrow \lnot \operatorname {adj} (u,v){\bigr )}\wedge {}\\&\para todos u\ \para todos v\ {\bigl (}(u\en G\wedge v\en G)\rightarrow \lnot \operatorname {adj} (u,v){\bigr )}\wedge {}\\&\para todos u\ \para todos v\ {\bigl (}(u\en B\wedge v\en B)\rightarrow \lnot \operatorname {adj} (u,v){\bigr )}{\Bigr )}\end{alineado}}}$$

Para esta variación de la lógica de grafos, el teorema de Courcelle se puede extender desde treewidth hasta clique-width : para cada propiedad fija MSO ₁ y cada límite fijo en el clique-width de un grafo, hay un algoritmo de tiempo lineal para probar si un grafo de clique-width como máximo tiene la propiedad . ^[8] La formulación original de este resultado requería que el grafo de entrada se diera junto con una construcción que probara que tiene un clique-width acotado, pero algoritmos de aproximación posteriores para clique-width eliminaron este requisito. ^[9]${\estilo de visualización \Pi}$${\estilo de visualización b}$${\estilo de visualización b}$${\estilo de visualización \Pi}$

El teorema de Courcelle también puede utilizarse con una variante más fuerte de la lógica monádica de segundo orden conocida como MSO ₂ . En esta formulación, un grafo se representa mediante un conjunto V de vértices, un conjunto E de aristas y una relación de incidencia entre vértices y aristas. Esta variante permite la cuantificación sobre conjuntos de vértices o aristas, pero no sobre relaciones más complejas sobre tuplas de vértices o aristas.

Por ejemplo, la propiedad de tener un ciclo hamiltoniano puede expresarse en MSO ₂ describiendo el ciclo como un conjunto de aristas que incluye exactamente dos aristas incidentes a cada vértice, de modo que cada subconjunto propio no vacío de vértices tiene una arista en el ciclo putativo con exactamente un punto final en el subconjunto . Sin embargo, la hamiltonicidad no puede expresarse en MSO _1. ^[10]

Es posible aplicar los mismos resultados a gráficos en los que los vértices o aristas tienen etiquetas de un conjunto finito fijo, ya sea aumentando la lógica del gráfico para incorporar predicados que describan las etiquetas o representando las etiquetas mediante variables no cuantificadas del conjunto de vértices o aristas. ^[11]

Otra dirección para extender el teorema de Courcelle se refiere a las fórmulas lógicas que incluyen predicados para contar el tamaño de la prueba. En este contexto, no es posible realizar operaciones aritméticas arbitrarias en tamaños de conjuntos, ni siquiera probar si dos conjuntos tienen el mismo tamaño. Sin embargo, MSO ₁ y MSO ₂ se pueden extender a lógicas llamadas CMSO ₁ y CMSO ₂ , que incluyen para cada dos constantes q y r un predicado que prueba si la cardinalidad del conjunto S es congruente con r módulo  q . El teorema de Courcelle se puede extender a estas lógicas. ^[4]${\displaystyle \operatorname {tarjeta} _{q,r}(S)}$

Como se ha indicado anteriormente, el teorema de Courcelle se aplica principalmente a problemas de decisión : ¿un grafo tiene una propiedad o no? Sin embargo, los mismos métodos también permiten la solución de problemas de optimización en los que los vértices o aristas de un grafo tienen pesos enteros, y se busca el conjunto de vértices con peso mínimo o máximo que satisface una propiedad dada, expresada en lógica de segundo orden. Estos problemas de optimización se pueden resolver en tiempo lineal en grafos de ancho de clique acotado. ^{[8] [11]}

En lugar de limitar la complejidad temporal de un algoritmo que reconoce una propiedad MSO en gráficos de ancho de árbol acotado, también es posible analizar la complejidad espacial de dicho algoritmo; es decir, la cantidad de memoria necesaria más allá del tamaño de la entrada misma (que se supone que se representa de forma de solo lectura para que sus requisitos de espacio no se puedan utilizar para otros fines). En particular, es posible reconocer los gráficos de ancho de árbol acotado y cualquier propiedad MSO en estos gráficos mediante una máquina de Turing determinista que utiliza solo espacio logarítmico . ^[12]

El enfoque típico para demostrar el teorema de Courcelle implica la construcción de un autómata de árbol finito de abajo hacia arriba que actúa sobre las descomposiciones de árbol del gráfico dado. ^[6]

En más detalle, dos grafos G ₁ y G ₂ , cada uno con un subconjunto especificado T de vértices llamados terminales, pueden definirse como equivalentes con respecto a una fórmula MSO F si, para todos los demás grafos H cuya intersección con G ₁ y G ₂ consiste solo en vértices en T , los dos grafos G ₁  ∪  H y G ₂  ∪  H se comportan de la misma manera con respecto a F : o ambos modelan F o ambos no modelan F . Esta es una relación de equivalencia , y puede demostrarse por inducción sobre la longitud de F que (cuando los tamaños de T y F están ambos acotados) tiene un número finito de clases de equivalencia . ^[13]

Una descomposición en árbol de un grafo G dado consiste en un árbol y, para cada nodo del árbol, un subconjunto de los vértices de G llamado bolsa. Debe satisfacer dos propiedades: para cada vértice v de G , las bolsas que contienen a v deben estar asociadas con un subárbol contiguo del árbol, y para cada arista uv de G , debe haber una bolsa que contenga tanto a u como a v . Los vértices en una bolsa pueden considerarse como los terminales de un subgrafo de G , representado por el subárbol de la descomposición en árbol que desciende de esa bolsa. Cuando G tiene un ancho de árbol acotado, tiene una descomposición en árbol en la que todas las bolsas tienen un tamaño acotado, y dicha descomposición se puede encontrar en un tiempo manejable con parámetros fijos. ^[14] Además, es posible elegir esta descomposición en árbol de modo que forme un árbol binario , con solo dos subárboles hijos por bolsa. Por lo tanto, es posible realizar un cálculo de abajo hacia arriba en esta descomposición del árbol, calculando un identificador para la clase de equivalencia del subárbol enraizado en cada bolsa combinando los bordes representados dentro de la bolsa con los dos identificadores para las clases de equivalencia de sus dos hijos. ^[15]

El tamaño del autómata construido de esta manera no es una función elemental del tamaño de la fórmula MSO de entrada. Esta complejidad no elemental es necesaria, en el sentido de que (a menos que P = NP ) no es posible probar las propiedades MSO en árboles en un tiempo que sea manejable con parámetros fijos y con una dependencia elemental del parámetro. ^[16]

Las pruebas del teorema de Courcelle muestran un resultado más fuerte: no sólo se puede reconocer cada propiedad monádica de segundo orden (contable) en tiempo lineal para grafos de ancho de árbol acotado, sino que también puede ser reconocida por un autómata de árbol de estados finitos . Courcelle conjeturó una inversa a esto: si una propiedad de grafos de ancho de árbol acotado es reconocida por un autómata de árbol, entonces se puede definir en lógica monádica de segundo orden contable. En 1998, Lapoire (1998), afirmó una resolución de la conjetura. ^[17] Sin embargo, la prueba es ampliamente considerada como insatisfactoria. ^{[18] [19]} Hasta 2016, solo se habían resuelto unos pocos casos especiales: en particular, la conjetura se había demostrado para grafos con un ancho de árbol de como máximo tres, ^[20] para grafos k-conexos con un ancho de árbol k, para grafos con un ancho de árbol y una cordalidad constantes, y para grafos k-externoplanares. La versión general de la conjetura fue finalmente demostrada por Mikołaj Bojańczyk y Michał Pilipczuk. ^[21]

Además, para los grafos de Halin (un caso especial de grafos con un ancho de árbol de tres) no es necesario contar: para estos grafos, cada propiedad que puede ser reconocida por un autómata de árbol también puede definirse en lógica monádica de segundo orden. Lo mismo es cierto de manera más general para ciertas clases de grafos en los que una descomposición de árbol puede describirse en sí misma en MSOL. Sin embargo, no puede ser cierto para todos los grafos de ancho de árbol acotado, porque en general el conteo agrega poder adicional sobre la lógica monádica de segundo orden sin conteo. Por ejemplo, los grafos con un número par de vértices pueden reconocerse usando el conteo, pero no sin él. ^[19]

El problema de satisfacibilidad de una fórmula de lógica monádica de segundo orden es el problema de determinar si existe al menos un grafo (posiblemente dentro de una familia restringida de grafos) para el cual la fórmula sea verdadera. Para familias de grafos arbitrarias y fórmulas arbitrarias, este problema es indecidible . Sin embargo, la satisfacibilidad de fórmulas MSO ₂ es decidible para los grafos de ancho de árbol acotado, y la satisfacibilidad de fórmulas MSO ₁ es decidible para grafos de ancho de camarilla acotado. La prueba implica construir un autómata de árbol para la fórmula y luego probar si el autómata tiene un camino de aceptación.

Como una recíproca parcial, Seese (1991) demostró que, siempre que una familia de grafos tiene un problema de satisfacibilidad MSO _{2 decidible, la familia debe tener un ancho de árbol acotado. La prueba se basa en un teorema de} Robertson y Seymour que dice que las familias de grafos con un ancho de árbol ilimitado tienen menores de cuadrícula arbitrariamente grandes . ^[22] Seese también conjeturó que cada familia de grafos con un problema de satisfacibilidad MSO ₁ decidible debe tener un ancho de clique acotado; esto no se ha demostrado, pero es cierto un debilitamiento de la conjetura que reemplaza MSO ₁ por CMSO _1. ^[23]

Grohe (2001) utilizó el teorema de Courcelle para demostrar que calcular el número de cruces de un grafo G es manejable con parámetros fijos con una dependencia cuadrática del tamaño de G , mejorando un algoritmo de tiempo cúbico basado en el teorema de Robertson-Seymour . Una mejora posterior adicional al tiempo lineal por Kawarabayashi y Reed (2007) sigue el mismo enfoque. Si el grafo dado G tiene un ancho de árbol pequeño, el teorema de Courcelle se puede aplicar directamente a este problema. Por otro lado, si G tiene un ancho de árbol grande, entonces contiene un menor de cuadrícula grande , dentro del cual el grafo se puede simplificar mientras se deja el número de cruces sin cambios. El algoritmo de Grohe realiza estas simplificaciones hasta que el grafo restante tiene un ancho de árbol pequeño, y luego aplica el teorema de Courcelle para resolver el subproblema reducido. ^{[24] [25]}

Gottlob y Lee (2007) observaron que el teorema de Courcelle se aplica a varios problemas de búsqueda de cortes mínimos multidireccionales en un grafo, cuando la estructura formada por el grafo y el conjunto de pares de cortes tiene un ancho de árbol acotado. Como resultado, obtuvieron un algoritmo manejable con parámetros fijos para estos problemas, parametrizado por un único parámetro, el ancho de árbol, mejorando las soluciones anteriores que combinaban múltiples parámetros. ^[26]

En topología computacional, Burton y Downey (2014) extienden el teorema de Courcelle de MSO ₂ a una forma de lógica monádica de segundo orden sobre complejos simpliciales de dimensión acotada que permite la cuantificación sobre símplices de cualquier dimensión fija. Como consecuencia, muestran cómo calcular ciertos invariantes cuánticos de variedades 3- , así como también cómo resolver ciertos problemas en la teoría de Morse discreta de manera eficiente, cuando la variedad tiene una triangulación (evitando símplices degenerados) cuyo gráfico dual tiene un ancho de árbol pequeño. ^[27]

Los métodos basados ​​en el teorema de Courcelle también se han aplicado a la teoría de bases de datos , ^[28] la representación y razonamiento del conocimiento , ^[29] la teoría de autómatas , ^[30] y la verificación de modelos . ^[31]