Constant time testability of first-order logic with modulo counting on finitary graphs

Resumen Técnico: Testabilidad en Tiempo Constante de la Lógica de Primer Orden con Conteo Modular en Grafos Finitarios

Enunciado del Problema
El artículo aborda el desafío de la prueba de propiedades en el modelo de grafos de grado acotado, buscando específicamente metateoremas algorítmicos que garanticen un tiempo de ejecución constante (independiente del tamaño de la entrada $n$). Si bien trabajos anteriores de Adler y Harwath (2018) establecieron que la Lógica Monádica de Segundo Orden con conteo (CMSO) es testeable con tiempo de ejecución polilogarítmico en clases de grafos con grado acotado y ancho de árbol acotado ($C^w_d$), permaneció como una cuestión abierta si esto podía mejorarse a tiempo constante.

Este artículo investiga esta cuestión en clases de grafos finitarios ($C^c_d$), definidas como la clase de todos los grafos donde el grado máximo está acotado por $d$ y el tamaño de cada componente conexa está acotado por una constante $c$. Los autores buscan determinar si las propiedades expresables en Lógica de Primer Orden con conteo modular (FOMOD), y consecuentemente CMSO, son testeables con tiempo de ejecución constante en estas clases.

Metodología
Los autores emplean una combinación de formas normales lógicas, muestreo probabilístico y técnicas teóricas de números para construir probadores de tiempo constante.

1. Forma Normal de Hanf Adaptada:
   La prueba se basa en una versión específica de la forma normal de Hanf para fórmulas FOMOD. Los autores adaptan el Teorema de Localidad de Hanf al contexto de grafos finitarios. Demuestran que cualquier sentencia FOMOD $\phi$ en $C^c_d$ puede transformarse en una Forma Normal Disyuntiva (DNF) donde las fórmulas atómicas describen la existencia de tipos específicos de componentes conexas (tipos de isomorfismo de tamaño $\le c$) con conteos específicos.

   • Crucialmente, los cuantificadores se unifican a un solo radio ($c-1$) y un "tope" uniforme $k$.
   • La satisfacción de la fórmula se reduce a verificar si el vector de histograma de componentes del grafo satisface restricciones específicas.

2. Vectores de Histograma de Componentes con Tope (k-CCHV):
   Los autores definen un vector de histograma de componentes con tope $k$ ($a$) indexado por los tipos de isomorfismo de componentes conexas. Para cada tipo $t$, la entrada $a[t]$ especifica una restricción sobre el número de ocurrencias de $t$ en el grafo:

   • Tipos raros: El conteo es exactamente un entero entre $0$y$k-1$.
   • Tipos frecuentes: El conteo es al menos $k$ y satisface una condición de congruencia específica ($\equiv j \pmod m$).
     El resultado lógico principal (Lema 14) establece que un grafo en $C^c_d$ satisface una sentencia FOMOD si y solo si su vector de histograma de componentes satisface al menos un vector de un conjunto finito $X$ derivado de la sentencia.

3. Estrategia Algorítmica:
   El probador propuesto opera en dos fases:

   • Muestreo: El algoritmo muestrea una cantidad constante de vértices (determinada por $\epsilon, c, d$) y explora sus componentes conexas para estimar la frecuencia de los tipos de componentes.
   • Verificación:
     • Si se detecta algún tipo de componente "raro" (que debe estar ausente o presente en números pequeños) en la muestra, el algoritmo rechaza.
     • Si no se detectan tipos raros, el algoritmo realiza una verificación aritmética. Verifica si el número total de vértices $n$ permite la construcción de un grafo que satisfaga las restricciones del histograma. Esto implica verificar condiciones de divisibilidad derivadas del Teorema de la Moneda de Frobenius. Específicamente, verifica si los vértices restantes (después de contabilizar los componentes raros requeridos y los componentes frecuentes mínimos) pueden llenarse mediante una combinación cónica de los tamaños de los tipos de componentes frecuentes.

4. "Parchabilidad" Teórico-Numérica:
   Una contribución técnica clave es el uso del Teorema de la Moneda de Frobenius. Para probar la corrección, los autores muestran que si un grafo está "lejos" de satisfacer la propiedad, se puede construir un grafo "parchado" $G'$ que satisface la propiedad y está $\epsilon$-cerca de la entrada. Esta construcción implica "plantar" los componentes raros requeridos y llenar el resto del grafo con copias de componentes frecuentes. El número de Frobenius asegura que, para $n$ suficientemente grande, el conteo de vértices restante siempre pueda expresarse como una suma de los tamaños de los componentes frecuentes, siempre que se cumplan las condiciones de aritmética modular necesarias.

Contribuciones y Resultados Clave

• Teorema Principal (Teorema 16): Toda propiedad definible en FOMOD es testeable con tiempo de ejecución constante en la clase $C^c_d$ (grafos con grado $\le d$ y tamaño de componente $\le c$).
• Corolario (Corolario 17): Dado que FOMOD y CMSO tienen el mismo poder expresivo en clases de grafos finitarios, toda propiedad definible en CMSO también es testeable con tiempo de ejecución constante en $C^c_d$.
• Extensión a Estructuras Relacionales (Teorema 18): El resultado se generaliza a estructuras relacionales de grado acotado con tamaño de componente acotado.

Significado y Afirmaciones
El artículo afirma que sus resultados representan un paso significativo hacia la resolución del problema abierto de si CMSO es testeable en tiempo constante en clases de grado acotado y ancho de árbol acotado.

• Paso Natural: Los autores señalan que las clases finitarias son exactamente la intersección de grado acotado y profundidad de árbol acotada (una condición más fuerte que el ancho de árbol). Por lo tanto, este trabajo proporciona un "paso natural" hacia el problema abierto más amplio.
• Fundamento para Grafos Hiperfinitos: Dado que los grafos finitarios son centrales en la definición de grafos hiperfinitos (cuya propiedad de ser testeables en tiempo constante es conocida), este trabajo sirve como una "piedra angular" para explorar la testabilidad en tiempo constante en clases de grafos más grandes y complejas.
• Independencia de la "Parchabilidad": Los autores destacan que la condición de "parchabilidad" teórico-numérica que exhiben, que permite inferencias globales a partir de muestras locales mediante verificaciones aritméticas, puede ser de interés independiente.
• Limitaciones: El artículo reconoce modestamente que la cuestión permanece abierta para clases generales de ancho de árbol acotado (donde los tamaños de los componentes no están uniformemente acotados). La dificultad surge específicamente cuando el número de vértices no puede modificarse para satisfacer la propiedad, una restricción inherente al modelo estándar de grado acotado.

El artículo no afirma resolver el caso general de ancho de árbol acotado, sino establece que la transición de tiempo polilogarítmico a tiempo constante es alcanzable cuando los tamaños de los componentes están uniformemente acotados, aprovechando la interacción entre el muestreo local y las restricciones aritméticas globales.