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]}

Formulaciones

Conjuntos de vértices

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. ${\displaystyle R}$ ${\displaystyle G}$ ${\displaystyle B}$ $${\displaystyle {\begin{aligned}\exists R\ \exists G\ \exists B\ {\Bigl (}&\forall v\ (v\in R\vee v\in G\vee v\in B)\wedge {}\\&\forall u\ \forall v\ {\bigl (}(u\in R\wedge v\in R)\rightarrow \lnot \operatorname {adj} (u,v){\bigr )}\wedge {}\\&\forall u\ \forall v\ {\bigl (}(u\in G\wedge v\in G)\rightarrow \lnot \operatorname {adj} (u,v){\bigr )}\wedge {}\\&\forall u\ \forall v\ {\bigl (}(u\in B\wedge v\in B)\rightarrow \lnot \operatorname {adj} (u,v){\bigr )}{\Bigr )}\end{aligned}}}$$

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] ${\displaystyle \Pi }$ ${\displaystyle b}$ ${\displaystyle b}$ ${\displaystyle \Pi }$

Conjuntos de bordes

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]

Gráficos etiquetados

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]

Congruencias modulares

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 {card} _{q,r}(S)}$

Decisión versus optimización

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 camarilla acotado. ^{[8] [11]}

Complejidad espacial

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]

Estrategia de prueba y complejidad

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]

Teorema de Bojańczyk-Pilipczuk

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]

Satisfacción y teorema de Seese

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]

Aplicaciones

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]

Referencias

1. Eger, Steffen (2008), Lenguajes regulares, ancho de árbol y teorema de Courcelle: una introducción , VDM Publishing, ISBN 9783639076332.
2. Courcelle, Bruno ; Engelfriet, Joost (2012), Estructura gráfica y lógica monádica de segundo orden: un enfoque teórico del lenguaje (PDF) , Enciclopedia de matemáticas y sus aplicaciones, vol. 138, Cambridge University Press , ISBN 9781139644006, Zbl1257.68006 ​.
3. Downey, Rodney G. ; Fellows, Michael R. (2013), "Capítulo 13: Teorema de Courcelle", Fundamentos de la complejidad parametrizada , Textos en Ciencias de la Computación, Londres: Springer, pp. 265–278, CiteSeerX 10.1.1.456.2729 , doi :10.1007/978-1-4471-5559-1, ISBN  978-1-4471-5558-4, MR  3154461, S2CID  23517218.
4. Courcelle, Bruno (1990), "La lógica monádica de segundo orden de los grafos. I. Conjuntos reconocibles de grafos finitos", Información y Computación , 85 (1): 12–75, doi : 10.1016/0890-5401(90)90043-H , MR  1042649, Zbl  0722.03008
5. Borie, Richard B.; Parker, R. Gary; Tovey, Craig A. (1992), "Generación automática de algoritmos de tiempo lineal a partir de descripciones de cálculo de predicados de problemas en familias de grafos construidas recursivamente", Algorithmica , 7 (5–6): 555–581, doi :10.1007/BF01758777, MR  1154588, S2CID  22623740.
6. Kneis, Joachim; Langer, Alexander (2009), "Un enfoque práctico del teorema de Courcelle", Electronic Notes in Theoretical Computer Science , 251 : 65–81, doi : 10.1016/j.entcs.2009.08.028.
7. Lampis, Michael (2010), "Meta-teoremas algorítmicos para restricciones de ancho de árbol", en de Berg, Mark; Meyer, Ulrich (eds.), Proc. 18th Annual European Symposium on Algorithms , Lecture Notes in Computer Science, vol. 6346, Springer, págs. 549–560, doi :10.1007/978-3-642-15775-2_47, ISBN 978-3-642-15774-5, Zbl1287.68078 ​.
8. Courcelle, B.; Makowsky, JA; Rotics, U. (2000), "Problemas de optimización resolubles en tiempo lineal en gráficos de ancho de camarilla acotado", Theory of Computing Systems , 33 (2): 125–150, CiteSeerX 10.1.1.414.1845 , doi :10.1007/s002249910009, MR  1739644, S2CID  15402031, Zbl  1009.68102 .
9. Oum, Sang-il ; Seymour, Paul (2006), "Aproximación del ancho de camarilla y del ancho de rama", Journal of Combinatorial Theory , Serie B, 96 (4): 514–528, doi : 10.1016/j.jctb.2005.10.006 , MR  2232389.
10. Courcelle y Engelfriet (2012), Proposición 5.13, p. 338.
11. Arnborg, Stefan; Lagergren, Jens; Seese, Detlef (1991), "Problemas sencillos para grafos descomponibles en árboles", Journal of Algorithms , 12 (2): 308–340, CiteSeerX 10.1.1.12.2544 , doi :10.1016/0196-6774(91)90006-K, MR  1105479 .
12. Elberfeld, Michael; Jakoby, Andreas; Tantau, Till (octubre de 2010), "Versiones en espacio logarítmico de los teoremas de Bodlaender y Courcelle" (PDF) , Proc. 51.º Simposio anual IEEE sobre fundamentos de la informática (FOCS 2010) , págs. 143-152, doi :10.1109/FOCS.2010.21, ISBN 978-1-4244-8525-3, S2CID1820251 ​.
13. Downey & Fellows (2013), Teorema 13.1.1, pág. 266.
14. Downey & Fellows (2013), Sección 10.5: Teorema de Bodlaender, págs. 195-203.
15. Downey & Fellows (2013), Sección 12.6: Autómatas de árbol, págs. 237–247.
16. Frick, Markus; Grohe, Martin (2004), "Revisión de la complejidad de la lógica de primer orden y de segundo orden monádica", Annals of Pure and Applied Logic , 130 (1–3): 3–31, CiteSeerX 10.1.1.104.8429 , doi : 10.1016/j.apal.2004.01.007 , MR  2092847 .
17. Lapoire, Denis (1998), "Recognizability equals monadic second-order definability for sets of graphs of bounded tree-width", STACS 98: 15th Annual Symposium on Theoretical Aspects of Computer Science París, Francia, 27 de febrero de 1998, Actas , Lecture Notes in Computer Science, vol. 1373, págs. 618–628, Bibcode :1998LNCS.1373..618L, CiteSeerX 10.1.1.22.7805 , doi :10.1007/bfb0028596, ISBN  978-3-540-64230-5.
18. Courcelle, B.; Engelfriet., J. (2012), "Estructura de grafos y lógica monádica de segundo orden: un enfoque teórico del lenguaje", Enciclopedia de matemáticas y sus aplicaciones , vol. 138, Cambridge University Press.
19. Jaffke, Lars; Bodlaender, Hans L. (2015), La definibilidad de MSOL es igual a la reconocibilidad de los gráficos de Halin y los gráficos k -outerplanares de grado acotado , arXiv : 1503.01604 , Bibcode :2015arXiv150301604J.
20. Kaller, D. (2000), "La definibilidad equivale a la reconocibilidad de árboles 3 parciales y árboles k parciales con conexión k ", Algorithmica , 27 (3): 348–381, doi :10.1007/s004530010024, S2CID  39798483.
21. Bojańczyk, Mikołaj; Pilipczuk, Michał (2016), "La definibilidad es igual a la reconocibilidad de los gráficos de ancho de árbol acotado", Actas del 31.º Simposio anual ACM/IEEE sobre lógica en informática (LICS 2016) , págs. 407–416, arXiv : 1605.03045 , doi : 10.1145/2933575.2934508, ISBN 978-1-4503-4391-6, Número de identificación del sujeto  1213054.
22. Seese, D. (1991), "La estructura de los modelos de teorías monádicas decidibles de grafos", Annals of Pure and Applied Logic , 53 (2): 169–195, doi :10.1016/0168-0072(91)90054-P, MR  1114848.
23. Courcelle, Bruno; Oum, Sang-il (2007), "Vertex-menors, lógica monádica de segundo orden y una conjetura de Seese" (PDF) , Journal of Combinatorial Theory , Serie B, 97 (1): 91–126, doi : 10.1016/j.jctb.2006.04.003 , MR  2278126.
24. Grohe, Martin (2001), "Cálculo de números cruzados en tiempo cuadrático", Actas del trigésimo tercer simposio anual de la ACM sobre teoría de la computación (STOC '01) , págs. 231-236, arXiv : cs/0009010 , doi : 10.1145/380752.380805, ISBN 1-58113-349-9, S2CID  724544.
25. Kawarabayashi, Ken-ichi ; Reed, Bruce (2007), "Cálculo de números cruzados en tiempo lineal", Actas del Trigésimo Noveno Simposio Anual de la ACM sobre Teoría de la Computación (STOC '07) , págs. 382–390, doi :10.1145/1250790.1250848, ISBN 978-1-59593-631-8, Número de identificación del sujeto  13000831.
26. Gottlob, Georg; Lee, Stephanie Tien (2007), "Un enfoque lógico para problemas de múltiples cortes", Information Processing Letters , 103 (4): 136–141, doi :10.1016/j.ipl.2007.03.005, MR  2330167.
27. Burton, Benjamin A.; Downey, Rodney G. (2014), Teorema de Courcelle para triangulaciones , arXiv : 1403.2926 , Bibcode :2014arXiv1403.2926B. Comunicación corta, Congreso Internacional de Matemáticos , 2014.
28. Grohe, Martin; Mariño, Julian (1999), "Definibilidad y complejidad descriptiva en bases de datos de ancho de árbol acotado", Teoría de bases de datos — ICDT'99: 7.ª Conferencia internacional Jerusalén, Israel, 10-12 de enero de 1999, Actas , Lecture Notes in Computer Science, vol. 1540, págs. 70-82, CiteSeerX 10.1.1.52.2984 , doi :10.1007/3-540-49257-7_6, ISBN  978-3-540-65452-0.
29. Gottlob, Georg; Pichler, Reinhard; Wei, Fang (enero de 2010), "El ancho de árbol limitado como clave para la manejabilidad de la representación y el razonamiento del conocimiento", Inteligencia artificial , 174 (1): 105–132, doi : 10.1016/j.artint.2009.10.003.
30. Madhusudan, P.; Parlato, Gennaro (2011), "El ancho de árbol del almacenamiento auxiliar", Actas del 38.º Simposio anual ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación (POPL '11) (PDF) , SIGPLAN Notices, vol. 46, págs. 283-294, doi :10.1145/1926385.1926419, ISBN 978-1-4503-0490-0, Número de identificación del sujeto  6976816
31. Obdržálek, Jan (2003), "Fast mu-calculus model checking when tree-width is bounded", Verificación asistida por computadora: 15.ª conferencia internacional, CAV 2003, Boulder, CO, EE. UU., 8-12 de julio de 2003, Actas , Lecture Notes in Computer Science, vol. 2725, págs. 80-92, CiteSeerX 10.1.1.2.4843 , doi :10.1007/978-3-540-45069-6_7, ISBN  978-3-540-40524-5.