En el estudio de los algoritmos de gráficos , el teorema de Courcelle es la afirmación de que cada propiedad de 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 & Tovey (1992) . [5] Se considera el arquetipo de algorítmicas meta-teoremas . [6] [7]
Formulaciones
Conjuntos de vértices
En una variación de la lógica de gráficos monádicos de segundo orden conocida como MSO 1 , el gráfico 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 gráfico 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.
Como ejemplo, la propiedad de que un gráfico sea coloreable con tres colores (representado por tres conjuntos de vértices, , y ) puede definirse mediante la fórmula monádica de segundo orden
Para esta variación de la lógica del gráfico, el teorema de Courcelle se puede extender desde el ancho del árbol hasta el ancho de la camarilla : para cada propiedad fija de MSO 1, y cada límite fijo en el ancho de camarilla de un gráfico, hay un algoritmo de tiempo lineal para probar si un gráfico de ancho de camarilla como máximo tiene propiedad . [8] La formulación original de este resultado requería que el gráfico de entrada se presentara junto con una construcción que demostrara que tiene un ancho de camarilla acotado, pero los algoritmos de aproximación posteriores para el ancho de camarilla eliminaron este requisito. [9]
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 2 . 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 en tuplas de vértices o aristas.
Por ejemplo, la propiedad de tener un ciclo hamiltoniano puede expresarse en MSO 2 al describir el ciclo como un conjunto de aristas que incluye exactamente dos aristas incidentes a cada vértice, de modo que cada subconjunto de vértices propio no vacío tiene una arista en el ciclo putativo. con exactamente un punto final en el subconjunto. Sin embargo, la hamiltonicidad no se puede expresar en MSO 1 . [10]
Gráficos etiquetados
Es posible aplicar los mismos resultados a gráficos en los que los vértices o los bordes 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 conjuntos de vértices o conjuntos de bordes no cuantificados. . [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 1 y MSO 2 pueden extenderse a lógicas denominadas CMSO 1 y CMSO 2 , que incluyen por cada dos constantes de q y r un predicadoque comprueba 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]
Decisión versus optimización
Como se indicó anteriormente, el teorema de Courcelle se aplica principalmente a los problemas de decisión : ¿un gráfico 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 satisfaga una propiedad dada, 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 por encima y más allá del tamaño de la entrada en sí (que se supone que está representada de forma de solo lectura, de modo que sus requisitos de espacio no pueden destinarse a 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 usa solo espacio logarítmico . [12]
Prueba de estrategia 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 del árbol del gráfico dado. [6]
Más detalladamente, dos gráficos G 1 y G 2 , cada uno con un subconjunto específico T de vértices llamados terminales, pueden definirse como equivalentes con respecto a una fórmula F de MSO si, para todos los demás gráficos H cuya intersección con G 1 y G 2 consiste solamente de vértices en T , los dos gráficos G 1 ∪ H y G 2 ∪ H comportan de la misma con respecto a F : o bien que ambos modelo F o ambos no modelan F . Ésta 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 limitados) tiene un número finito de clases de equivalencia . [13]
Una descomposición de árbol de un gráfico G dado consta de un árbol y, para cada nodo de á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 borde uv de G , debe haber una bolsa que contenga tanto u como v . Los vértices de una bolsa se pueden considerar 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 limitado, tiene una descomposición de árbol en la que todas las bolsas tienen un tamaño limitado, 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 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. 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 es manejable con parámetros fijos con una dependencia elemental del parámetro. [dieciséis]
Teorema de Bojańczyk-Pilipczuk
Las demostraciones del teorema de Courcelle muestran un resultado más fuerte: no solo 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 puede ser reconocida por un autómata de árbol de estado finito . Courcelle conjeturó lo contrario: si un autómata de árbol reconoce una propiedad de las gráficas de ancho de árbol acotado, entonces puede definirse contando la lógica monádica de segundo orden. En 1998 Lapoire (1998) , reclamó una resolución de la conjetura. [17] Sin embargo, la prueba se considera en general insatisfactoria. [18] [19] Hasta 2016, solo se resolvieron algunos casos especiales: en particular, la conjetura ha sido probada para gráficos de ancho de árbol como máximo tres, [20] para gráficos conectados con k de ancho de árbol k, para gráficos de ancho de árbol constante y cordalidad, y para k grafos planos exteriores. La versión general de la conjetura fue finalmente probada por Mikołaj Bojańczyk y Michał Pilipczuk. [21]
Además, para los gráficos de Halin (un caso especial de tres gráficos de ancho de árbol) no es necesario contar: para estos gráficos, todas las propiedades que pueden ser reconocidas por un autómata de árbol también se pueden 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 la descomposición de un árbol se puede describir en MSOL. Sin embargo, no puede ser cierto para todas las gráficas de ancho de árbol acotado, porque en general el conteo 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 él. [19]
Satisfabilidad y teorema de Seese
El problema de satisfacibilidad para una fórmula de lógica monádica de segundo orden es el problema de determinar si existe al menos un gráfico (posiblemente dentro de una familia restringida de gráficos) para el que la fórmula es verdadera. Para familias de grafos arbitrarios y fórmulas arbitrarias, este problema es indecidible . Sin embargo, la satisfacibilidad de las fórmulas de MSO 2 es decidible para los gráficos de ancho de árbol acotado, y la satisfacibilidad de las fórmulas de MSO 1 es decidible para 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 un camino de aceptación.
Como recíproco parcial, Seese (1991) demostró que, siempre que una familia de gráficos tiene un problema de satisfacibilidad de MSO 2 decidible , la familia debe tener un ancho de árbol acotado. La demostración se basa en un teorema de Robertson y Seymour de que las familias de gráficos con un ancho de árbol ilimitado tienen menores de cuadrícula arbitrariamente grandes . [22] Seese también conjeturó que cada familia de gráficos con un problema de satisfacibilidad MSO 1 decidible debe tener un ancho de camarilla acotado; esto no ha sido probado, pero un debilitamiento de la conjetura que reemplaza a MSO 1 por CMSO 1 es cierto. [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 posterior adicional al tiempo lineal de Kawarabayashi y Reed (2007) sigue el mismo enfoque. Si el gráfico G dado 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 gran ancho de árbol, 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 pequeño ancho de árbol 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 direcciones en un gráfico, cuando la estructura formada por el gráfico y el conjunto de pares de cortes tiene un ancho de árbol limitado. Como resultado, obtienen un algoritmo manejable de parámetros fijos para estos problemas, parametrizado por un solo parámetro, treewidth, mejorando las 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 2 a una forma de lógica monádica de segundo orden en complejos simpliciales de dimensión acotada que permite la cuantificación sobre 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 de Morse discreta de manera eficiente, cuando la variedad tiene una triangulación (evitando simples degenerados) cuyo gráfico dual tiene un pequeño ancho de árbol. [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
- ^ Eger, Steffen (2008), Lenguajes regulares, ancho del árbol y teorema de Courcelle: una introducción , VDM Publishing, ISBN 9783639076332.
- ^ Courcelle, Bruno ; Engelfriet, Joost (2012), Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach (PDF) , Encyclopedia of Mathematics and its Applications, 138 , Cambridge University Press , ISBN 9781139644006, Zbl 1257.68006.
- ^ 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.
- ^ a b Courcelle, Bruno (1990), "La lógica monádica de segundo orden de los gráficos. I. Conjuntos reconocibles de gráficos finitos", Información y Computación , 85 (1): 12–75, doi : 10.1016 / 0890-5401 (90) 90043 -H , MR 1042649 , Zbl 0.722,03008
- ^ 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 , MR 1154588 , S2CID 22623740.
- ^ a b Kneis, Joachim; Langer, Alexander (2009), "Un enfoque práctico del teorema de Courcelle", Notas electrónicas en la informática teórica , 251 : 65–81, doi : 10.1016 / j.entcs.2009.08.028.
- ^ Lampis, Michael (2010), "Metateoremas algorítmicos para restricciones de ancho de árbol", en de Berg, Mark; Meyer, Ulrich (eds.), Proc. 18o Simposio Europeo Anual sobre Algoritmos , Lecture Notes in Computer Science, 6346 , Springer, págs. 549–560, doi : 10.1007 / 978-3-642-15775-2_47 , Zbl 1287.68078.
- ^ a b Courcelle, B .; Makowsky, JA; Rotics, U. (2000), "Problemas de optimización con solución de tiempo lineal en gráficos de ancho de camarilla acotado", Teoría de los 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.
- ^ Oum, Sang-il ; Seymour, Paul (2006), "Aproximación del ancho de la camarilla y el ancho de la rama", Journal of Combinatorial Theory , Serie B, 96 (4): 514-528, doi : 10.1016 / j.jctb.2005.10.006 , MR 2232389.
- ^ Courcelle y Engelfriet (2012) , Proposición 5.13, p. 338 .
- ^ a b Arnborg, Stefan; Lagergren, Jens; Seese, Detlef (1991), "Problemas fáciles 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 , MR 1105479.
- ^ Elberfeld, Michael; Jakoby, Andreas; Tantau, Till (octubre de 2010), "Versiones de espacio de registro de los teoremas de Bodlaender y Courcelle" (PDF) , Proc. 51 ° Simposio anual del IEEE sobre los fundamentos de la informática (FOCS 2010) , págs. 143-152, doi : 10.1109 / FOCS.2010.21 , S2CID 1820251.
- ^ Downey & Fellows (2013) , Teorema 13.1.1, p. 266.
- ^ Downey & Fellows (2013) , Sección 10.5: Teorema de Bodlaender, págs. 195-203.
- ^ Downey & Fellows (2013) , Sección 12.6: Autómatas de árboles, págs. 237–247.
- ^ Frick, Markus; Grohe, Martin (2004), "La complejidad de la lógica de primer orden y la lógica monádica de segundo orden revisitada", Annals of Pure and Applied Logic , 130 (1-3): 3-31, doi : 10.1016 / j.apal.2004.01 0.007 , MR 2092847.
- ^ 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 , págs. .618–628, Bibcode : 1998LNCS.1373..618L , CiteSeerX 10.1.1.22.7805 , doi : 10.1007 / bfb0028596.
- ^ Courcelle, B .; Engelfriet., J. (2012), "Estructura gráfica y lógica monádica de segundo orden: un enfoque teórico del lenguaje", Enciclopedia de las matemáticas y sus aplicaciones , 138 , Cambridge University Press.
- ^ a b Jaffke, Lars; Bodlaender, Hans L. (2015), MSOL-definibilidad es igual a la capacidad de reconocimiento de los gráficos de Halin y los gráficos de orugas planas de grado k delimitado , arXiv : 1503.01604 , Bibcode : 2015arXiv150301604J.
- ^ Kaller, D. (2000), "La definibilidad es igual a la reconocibilidad de 3 árboles parciales y árboles k parciales conectados por k ", Algorithmica , 27 (3): 348–381, doi : 10.1007 / s004530010024 , S2CID 39798483.
- ^ Bojańczyk, Mikołaj; Pilipczuk, Michał (2016), "Definibilidad es igual a reconocibilidad para gráficos de ancho de árbol acotado", Actas del 31 ° Simposio Anual ACM / IEEE sobre Lógica en Ciencias de la Computación (LICS 2016) , págs. 407–416, arXiv : 1605.03045 , doi : 10.1145 /2933575.2934508 , S2CID 1213054.
- ^ Seese, D. (1991), "La estructura de los modelos de teorías monádicas decidibles de gráficos", Annals of Pure and Applied Logic , 53 (2): 169-195, doi : 10.1016 / 0168-0072 (91) 90054- P , MR 1114848.
- ^ 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 , MR 2278126.
- ^ Grohe, Martin (2001), "Computación de números cruzados en tiempo cuadrático", Actas del trigésimo tercer Simposio Anual de ACM sobre Teoría de la Computación (STOC '01) , págs. 231-236, arXiv : cs / 0009010 , doi : 10.1145 /380752.380805 , S2CID 724544.
- ^ Kawarabayashi, Ken-ichi ; Reed, Bruce (2007), "Computación del número de cruce en tiempo lineal", Actas del trigésimo noveno Simposio Anual de ACM sobre Teoría de la Computación (STOC '07) , págs. 382–390, doi : 10.1145 / 1250790.1250848 , S2CID 13000831.
- ^ Gottlob, Georg; Lee, Stephanie Tien (2007), "Un enfoque lógico para problemas de corte múltiple ", Cartas de procesamiento de información , 103 (4): 136–141, doi : 10.1016 / j.ipl.2007.03.005 , MR 2330167.
- ^ Burton, Benjamin A .; Downey, Rodney G. (2014), Teorema de triangulaciones de Courcelle , arXiv : 1403.2926 , Bibcode : 2014arXiv1403.2926B. Comunicación corta, Congreso Internacional de Matemáticos , 2014.
- ^ 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: 7th International Conference Jerusalem, Israel, 10-12 de enero de 1999, Proceedings , Lecture Notes in Computer Science, 1540 , págs. 70–82, CiteSeerX 10.1.1.52.2984 , doi : 10.1007 / 3-540-49257-7_6.
- ^ Gottlob, Georg; Pichler, Reinhard; Wei, Fang (enero de 2010), "El ancho del árbol limitado como clave para la tractabilidad de la representación y el razonamiento del conocimiento", Inteligencia artificial , 174 (1): 105-132, doi : 10.1016 / j.artint.2009.10.003.
- ^ 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, 46 , págs. 283–294 , doi : 10.1145 / 1926385.1926419 , S2CID 6976816
- ^ Obdržálek, Jan (2003), "Comprobación rápida del modelo mu-cálculo cuando se limita el ancho del árbol", Verificación asistida por computadora: 15ª Conferencia Internacional, CAV 2003, Boulder, CO, EE. UU., 8-12 de julio de 2003, Actas , Notas de conferencias en Ciencias de la Computación, 2725 , págs. 80–92, CiteSeerX 10.1.1.2.4843 , doi : 10.1007 / 978-3-540-45069-6_7.