teorema de courcelle

En el estudio de los algoritmos de gráficos , el teorema de Courcelle es la afirmación de que cada propiedad del gráfico definible en la lógica monádica de segundo orden de los gráficos se puede decidir en tiempo lineal en gráficos de ancho de árbol acotado . ^{[1] [2] [3]} El resultado fue probado por primera vez por Bruno Courcelle en 1990 ^[4] y redescubierto de forma independiente 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 monádica de grafos 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 gráfico 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 que un gráfico se pueda colorear con tres colores (representados por tres conjuntos de vértices , y ) puede definirse mediante la fórmula monádica de segundo orden. ${\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}}}$$

convención de nomenclaturaconjunto independiente

Para esta variación de la lógica gráfica, el teorema de Courcelle se puede extender desde el ancho del árbol hasta el ancho de la camarilla : para cada propiedad MSO ₁ fija y cada límite fijo en el ancho de la camarilla de un gráfico, existe un algoritmo de tiempo lineal para probar si una El gráfico de ancho de camarilla como máximo tiene la propiedad . ^[8] La formulación original de este resultado requería que el gráfico de entrada se proporcionara junto con una construcción que demostrara que tiene un ancho de camarilla limitado, pero los algoritmos de aproximación posteriores para el ancho de camarilla eliminaron este requisito. ^[9] ${\displaystyle \Pi }$ ${\displaystyle b}$ ${\displaystyle b}$ ${\displaystyle \Pi }$

Conjuntos de bordes

El teorema de Courcelle también se puede utilizar con una variación más fuerte de la lógica monádica de segundo orden conocida como MSO ₂ . En esta formulación, un gráfico está representado por un conjunto V de vértices, un conjunto E de aristas y una relación de incidencia entre vértices y aristas. Esta variación 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 se puede expresar en MSO ₂ describiendo el ciclo como un conjunto de aristas que incluye exactamente dos aristas incidentes en cada vértice, de modo que cada subconjunto propio no vacío de vértices tenga una arista en el ciclo putativo. con exactamente un punto final en el subconjunto. Sin embargo, la hamiltonicidad no se puede expresar en MSO ₁ . ^[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 describen las etiquetas, o representando las etiquetas mediante variables de conjunto de vértices o conjuntos de aristas no cuantificadas. . ^[11]

Congruencias modulares

Otra dirección para ampliar el teorema de Courcelle se refiere a 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 puede extenderse a estas lógicas. ^[4] ${\displaystyle \operatorname {card} _{q,r}(S)}$

Decisión versus optimización

Como se indicó anteriormente, el teorema de Courcelle se aplica principalmente a problemas de decisión : ¿una gráfica 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 gráfico tienen pesos enteros, y se busca el conjunto de vértices de peso mínimo o máximo que satisface una propiedad determinada, expresada en lógica de segundo orden. Estos problemas de optimización se pueden resolver en tiempo lineal en gráficos 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 limitado, 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 propia entrada (que se supone que está representada en forma de sólo lectura para que sus requisitos de espacio no puedan destinarse a otros fines). En particular, es posible reconocer las gráficas de ancho de árbol acotado y cualquier propiedad MSO en estas gráficas mediante una máquina determinista de Turing 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 árbol autómata finito de abajo hacia arriba que actúa sobre las descomposiciones de los árboles del gráfico dado. ^[6]

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

Una descomposición en árbol de un gráfico G dado consta de 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 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 u como v . Los vértices de una bolsa pueden considerarse como las terminales de un subgrafo de G , representado por el subárbol de la descomposición del árbol que desciende de esa bolsa. Cuando G tiene un ancho de árbol acotado, tiene una descomposición de árbol en la que todas las bolsas tienen un tamaño acotado, y dicha descomposición se puede encontrar en un tiempo manejable de parámetros fijos. ^[14] Además, es posible elegir esta descomposición de árbol para que forme un árbol binario , con solo dos subárboles secundarios por bolsa. Por lo tanto, es posible realizar un cálculo ascendente en esta descomposición de á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 niños. ^[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 de MSO en árboles en un tiempo que sea manejable con parámetros fijos y con una dependencia elemental del parámetro. ^[dieciséis]

Teorema de Bojańczyk-Pilipczuk

Las pruebas del teorema de Courcelle muestran un resultado más sólido: no sólo se puede reconocer cada propiedad monádica de segundo orden (contando) en tiempo lineal para gráficos de ancho de árbol acotado, sino que también se puede reconocer mediante un autómata de árbol de estado finito . Courcelle conjeturó lo contrario: si un autómata de árbol reconoce una propiedad de los gráficos de ancho de árbol acotado, entonces se puede definir contando lógica monádica de segundo orden. En 1998, Lapoire (1998) afirmó una resolución de la conjetura. ^[17] Sin embargo, la prueba se considera en general insatisfactoria. ^{[18] [19]} Hasta 2016, solo se resolvieron unos pocos casos especiales: en particular, la conjetura se ha demostrado para gráficos de ancho de árbol como máximo tres, ^[20] para gráficos k-conexos de ancho de árbol k, para gráficos de ancho de árbol constante y cordalidad, y para gráficos k-planares exteriores. La versión general de la conjetura fue finalmente demostrada por Mikołaj Bojańczyk y Michał Pilipczuk. ^[21]

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

Satisfacibilidad 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 es verdadera. Para familias de gráficos arbitrarios y fórmulas arbitrarias, este problema es indecidible . Sin embargo, la satisfacibilidad de las fórmulas MSO ₂ es decidible para los gráficos de ancho de árbol acotado, y la satisfacibilidad de las fórmulas MSO ₁ es decidible para los gráficos de ancho de camarilla acotado. La prueba implica construir un árbol autómata para la fórmula y luego probar si el autómata tiene una ruta de aceptación.

Como recíproco parcial, Seese (1991) demostró que, siempre que una familia de grafos tiene un problema de satisfacibilidad de MSO ₂ decidible , la familia debe tener un ancho de árbol acotado. La prueba se basa en un teorema de Robertson y Seymour de que las familias de gráficos con ancho de árbol ilimitado tienen grillas menores arbitrariamente grandes . ^[22] Seese también conjeturó que cada familia de gráficos con un problema de satisfacibilidad MSO ₁ decidible debe tener un ancho de camarilla acotado; Esto no ha sido probado, pero es cierta una debilitación 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 cruce de un gráfico 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 adicional posterior al tiempo lineal realizada por Kawarabayashi y Reed (2007) sigue el mismo enfoque. Si el gráfico 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 una cuadrícula menor grande , dentro de la cual el gráfico se puede simplificar sin cambiar el número de cruce. El algoritmo de Grohe realiza estas simplificaciones hasta que el gráfico 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 encontrar cortes mínimos de múltiples vías en un gráfico, cuando la estructura formada por el gráfico y el conjunto de pares de cortes tiene un ancho de árbol acotado. Como resultado, obtienen un algoritmo manejable de parámetros fijos para estos problemas, parametrizado por un único parámetro, el ancho del árbol, mejorando soluciones anteriores que habían combinado 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 en complejos simpliciales de dimensión limitada que permite la cuantificación de simples de cualquier dimensión fija. Como consecuencia, muestran cómo calcular ciertos invariantes cuánticos de 3 variedades , así como cómo resolver ciertos problemas en la teoría Morse discreta de manera eficiente, cuando la variedad tiene una triangulación (evitando simples 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] representación y razonamiento del conocimiento , ^[29] teoría de autómatas , ^[30] y verificación de modelos . ^[31]

Referencias

1. Eger, Steffen (2008), Lenguajes regulares, ancho de árbol y teorema de Courcelle: 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 las matemáticas y sus aplicaciones, vol. 138, Prensa de la Universidad de Cambridge , ISBN 9781139644006, Zbl  1257.68006.
3. Downey, Rodney G .; Fellows, Michael R. (2013), "Capítulo 13: Teorema de Courcelle", Fundamentos de la complejidad parametrizada , Texts in Computer Science, Londres: Springer, págs. 265–278, CiteSeerX 10.1.1.456.2729 , doi :10.1007/978- 1-4471-5559-1, ISBN  978-1-4471-5558-4, SEÑOR  3154461, S2CID  23517218.
4. Courcelle, Bruno (1990), "La lógica monádica de gráficos de segundo orden. I. Conjuntos reconocibles de gráficos finitos", Información y Computación , 85 (1): 12–75, doi : 10.1016/0890-5401 (90 )90043-H , SEÑOR  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 problemas de cálculo de predicados en familias de gráficos construidas de forma recursiva", Algorithmica , 7 (5–6): 555–581, doi :10.1007/BF01758777, SEÑOR  1154588, S2CID  22623740.
6. Kneis, Joaquín; 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), "Metateoremas algorítmicos para restricciones de ancho de árbol", en de Berg, Mark; Meyer, Ulrich (eds.), Proc. 18.º Simposio europeo anual sobre algoritmos , Apuntes de conferencias sobre informática, vol. 6346, Springer, págs. 549–560, doi :10.1007/978-3-642-15775-2_47, Zbl  1287.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", Teoría de sistemas informáticos , 33 (2): 125–150, CiteSeerX 10.1.1.414.1845 , doi :10.1007/s002249910009, Señor  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 , SEÑOR  2232389.
10. Courcelle y Engelfriet (2012), Proposición 5.13, p. 338.
11. Arnborg, Stefan; Lagergren, Jens; Seese, Detlef (1991), "Problemas sencillos para gráficos descomponibles en árboles", Journal of Algorithms , 12 (2): 308–340, CiteSeerX 10.1.1.12.2544 , doi :10.1016/0196-6774(91)90006-K , señor  1105479 .
12. Elberfeld, Michael; Jakoby, Andreas; Tantau, Till (octubre de 2010), "Versiones en el espacio logarítmico de los teoremas de Bodlaender y Courcelle" (PDF) , Proc. 51.º Simposio anual del IEEE sobre fundamentos de la informática (FOCS 2010) , págs. 143–152, doi :10.1109/FOCS.2010.21, S2CID  1820251.
13. Downey & Fellows (2013), Teorema 13.1.1, p. 266.
14. Downey & Fellows (2013), Sección 10.5: Teorema de Bodlaender, págs.
15. Downey & Fellows (2013), Sección 12.6: Autómatas de árboles, págs.
16. Frick, Markus; Grohe, Martin (2004), "Revisión de la complejidad de la lógica monádica de primer orden y de segundo orden", 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 , SEÑOR  2092847 .
17. Lapoire, Denis (1998), "La reconocibilidad es igual a la definibilidad monádica de segundo orden para conjuntos de gráficos de ancho de árbol acotado", STACS 98: 15º Simposio anual sobre aspectos teóricos de la informática París, Francia, 27 de febrero de 1998, Actas , vol. 1373, págs. 618–628, Bibcode :1998LNCS.1373..618L, CiteSeerX 10.1.1.22.7805 , doi :10.1007/bfb0028596 .
18. Courcelle, B.; Engelfriet., J. (2012), "Estructura gráfica y lógica monádica de segundo orden: un enfoque teórico del lenguaje", Enciclopedia de matemáticas y sus aplicaciones , vol. 138, Prensa de la Universidad de Cambridge.
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 de grado acotado k -planares exteriores , arXiv : 1503.01604 , Bibcode : 2015arXiv150301604J.
20. Kaller, D. (2000), "La definibilidad equivale a la reconocibilidad de 3 árboles parciales y k -árboles parciales conectados " , 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 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, S2CID  1213054.
22. Seese, D. (1991), "La estructura de los modelos de teorías monádicas de grafos decidibles", Annals of Pure and Applied Logic , 53 (2): 169–195, doi :10.1016/0168-0072(91)90054 -P, SEÑOR  1114848.
23. Courcelle, Bruno; Oum, Sang-il (2007), "Vértices menores, 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 , SEÑOR  2278126.
24. Grohe, Martin (2001), "Cálculo de números cruzados en tiempo cuadrático", Actas del trigésimo tercer simposio anual ACM sobre teoría de la computación (STOC '01) , págs. 231-236, arXiv : cs/0009010 , doi : 10.1145/380752.380805, S2CID  724544.
25. Kawarabayashi, Ken-ichi ; Reed, Bruce (2007), "Cálculo del número de cruce en tiempo lineal", Actas del trigésimo noveno simposio anual ACM sobre teoría de la informática (STOC '07) , págs. 382–390, doi :10.1145/1250790.1250848, S2CID  13000831.
26. Gottlob, Georg; Lee, Stephanie Tien (2007), "Un enfoque lógico para problemas de cortes múltiples", Information Processing Letters , 103 (4): 136–141, doi :10.1016/j.ipl.2007.03.005, MR  2330167.
27. Burton, Benjamín A.; Downey, Rodney G. (2014), Teorema de Courcelle para triangulaciones , arXiv : 1403.2926 , Bibcode : 2014arXiv1403.2926B. Comunicación breve, Congreso Internacional de Matemáticos , 2014.
28. Grohe, Martín; 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: 7ma Conferencia Internacional Jerusalén, Israel, 10 al 12 de enero de 1999, Actas , Apuntes de conferencias en Ciencias de la Computación, vol. 1540, págs. 70–82, CiteSeerX 10.1.1.52.2984 , doi :10.1007/3-540-49257-7_6 .
29. Gottlob, Georg; Pichler, Reinhard; Wei, Fang (enero de 2010), "El ancho de árbol acotado como clave para la trazabilidad del razonamiento y la representación del conocimiento", Inteligencia artificial , 174 (1): 105–132, doi : 10.1016/j.artint.2009.10.003.
30. Madhusudan, P.; Parlato, Gennaro (2011), "The Tree Width of Auxiliary Storage", Actas del 38º Simposio anual ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación (POPL '11) (PDF) , Avisos SIGPLAN, vol. 46, págs. 283–294, doi :10.1145/1926385.1926419, S2CID  6976816
31. Obdržálek, Jan (2003), "Comprobación rápida del modelo de cálculo mu cuando el ancho del árbol está limitado", Verificación asistida por computadora: 15ª Conferencia Internacional, CAV 2003, Boulder, CO, EE. UU., 8 al 12 de julio de 2003, Actas , Conferencia Notas en Ciencias de la Computación, vol. 2725, págs. 80–92, CiteSeerX 10.1.1.2.4843 , doi :10.1007/978-3-540-45069-6_7 .