A SAT-Based Exact Approach for Radio k-Labeling

Resumen Técnico: Un enfoque exacto basado en SAT para el etiquetado de radio $k$

Definición del Problema
El artículo aborda el problema del etiquetado de radio $k$ (también conocido como coloración de radio $k$), un problema de optimización combinatoria derivado del problema de asignación de canales. Dado un grafo conexo $G=(V, E)$ con diámetro $k = \text{diam}(G)$, el objetivo es asignar etiquetas de enteros no negativos $f(v)$ a los vértices tales que para cada par de vértices distintos $u, v$, se cumpla la condición $|f(u) - f(v)| \ge k + 1 - d(u, v)$, donde $d(u, v)$ es la distancia del camino más corto. El objetivo es minimizar el alcance (span) del etiquetado, definido como $\max_{v \in V} f(v)$. El alcance mínimo posible es el número de radio, denotado como $rn(G)$.

Aunque existen construcciones teóricas para familias de grafos específicas (por ejemplo, caminos, ciclos, árboles) y algoritmos heurísticos proporcionan soluciones factibles para grafos generales, las soluciones exactas para clases amplias de grafos son escasas. Las formulaciones de Programación Lineal Entera (ILP) existentes sufren problemas de escalabilidad debido al rápido crecimiento del espacio de búsqueda y a la falta de reutilización de información entre las iteraciones de optimización.

Metodología
Los autores proponen un marco de trabajo exacto e incremental basado en SAT que combina una codificación de orden compacta con una estrategia de optimización iterativa.

1. Codificaciones SAT:
   El artículo desarrolla dos codificaciones de satisfacción de Booleanos (SAT) basadas en el dominio de etiquetas $\{1, \dots, UB\}$, donde $UB$ es un límite superior precalculado:

   • Codificación Directa: Utiliza variables de asignación $x_{v,l}$ (verdadero si el vértice $v$ tiene la etiqueta $l$). Impone restricciones mediante cláusulas de conflicto por pares. Aunque es lógicamente equivalente al modelo ILP, requiere $O(n^2 UB k)$ cláusulas para las restricciones de radio, lo que conduce a una propagación débil bajo resolución de unidad.
   • Codificación de Orden: Introduce variables de umbral $g_{v,l}$ (verdadero si $f(v) \ge l$) junto con las variables de asignación. Esta codificación representa la restricción de radio $|f(u) - f(v)| \ge \Delta_{uv}$ de forma más compacta. Reduce el número de cláusulas de restricción de radio de $O(n^2 UB k)$ a $O(n^2 UB)$ al eliminar la dependencia de $k$ en el recuento de cláusulas. La codificación de orden también permite una propagación más fuerte, ya que las desigualdades como $f(v) \ge c$ se mapean a literales únicos.

2. Estrategia de Resolución Incremental:
   El marco de trabajo emplea un paradigma de resolución SAT incremental. En lugar de reconstruir la fórmula para cada iteración, se construye una única instancia del solver. El algoritmo procede de la siguiente manera:

   • Fase 1: Calcular todas las distancias entre pares y establecer $k = \text{diam}(G)$.
   • Fase 2: Construir el modelo SAT con un límite superior inicial $UB$.
   • Fase 3: Resolver la fórmula iterativamente. Si se encuentra una asignación satisfactoria con un alcance $\beta$, se instruye al solver para prohibir cualquier alcance $\ge \beta$ (estrechando el límite) y resolver de nuevo. Crucialmente, las cláusulas aprendidas de las iteraciones anteriores se preservan, evitando el esfuerzo de búsqueda redundante. El bucle termina cuando el solver devuelve UNSAT (certificando la optimalidad) o se alcanza un límite de tiempo.

3. Ruptura de Simetría:
   Para los grafos ciclo ($C_n$), que exhiben simetría rotacional, los autores introducen una restricción de ruptura de simetría que fija la etiqueta del primer vértice en 1 ($f(0)=1$). Esto reduce el espacio de búsqueda y acelera significativamente la prueba de optimalidad sin descartar soluciones óptimas.

Contribuciones Clave

• Nuevo Marco de Trabajo: El primer marco de optimización exacto basado en SAT para el problema del etiquetado de radio $k$, utilizando codificación de orden y resolución incremental.
• Mejoras de Eficiencia: La codificación de orden reduce la complejidad de las cláusulas y mejora la propagación en comparación con la codificación directa. El enfoque incremental reutiliza las cláusulas aprendidas, reduciendo significativamente la sobrecarga computacional en comparación con las llamadas SAT independientes o los enfoques ILP estándar que descartan la información de búsqueda previa.
• Manejo de Simetría: La introducción de restricciones específicas de ruptura de simetría para grafos ciclo, demostrando aceleraciones sustanciales en los tiempos de resolución y un mayor número de óptimos certificados.

Resultados Experimentales
El marco de trabajo fue evaluado en 146 instancias de referencia a través de nueve familias de grafos (caminos, ciclos, serpientes triangulares, serpientes $kC_m$, escaleras, libros, grafos de amistad y árboles binomiales) con un límite de tiempo de 1,200 segundos.

• Rendimiento vs. Heurísticas: El método Order-SAT propuesto estableció 38 nuevos mejores números de radio conocidos entre las 98 instancias sin un óptimo de forma cerrada conocido. Produjo consistentemente límites factibles más ajustados que las heurísticas existentes (Ub1, Ub3) y el SAT de codificación directa.
• Rendimiento vs. ILP:
  • Grafos de Diámetro Creciente: Para familias donde el diámetro crece con el tamaño (por ejemplo, serpientes, escaleras, árboles binomiales), Order-SAT superó a los solvers ILP comerciales (CPLEX, Gurobi) tanto en calidad de solución (límites más ajustados) como en el número de óptimos certificados. Los solvers ILP a menudo agotaron la memoria o devolvieron incumbentes laxos en estas instancias.
  • Grafos de Diámetro Acotado: Para familias con diámetro constante (por ejemplo, grafos libro, grafos de amistad), los solvers ILP fueron más efectivos, certificando la optimalidad para todas las instancias rápidamente.
• Enfoque Combinado: Al combinar el marco de trabajo SAT con modelos ILP, el estudio certificó soluciones óptimas para 109 de las 146 instancias, expandiendo sustancialmente el conjunto de referencias de etiquetado de radio con optimalidad probada.
• Significancia Estadística: Una prueba de Friedman confirmó que Order-SAT logró el mejor rango general (rango medio 2.58) entre todos los métodos comparados, incluyendo solvers comerciales y heurísticas.

Significancia
El artículo afirma que la resolución incremental de SAT constituye un paradigma de optimización exacta práctico para problemas de etiquetado de grafos que tradicionalmente han estado dominados por construcciones teóricas y algoritmos heurísticos. El trabajo demuestra que:

1. Los solvers SAT modernos, cuando se combinan con codificaciones compactas y estrategias incrementales, pueden resolver problemas de optimización combinatoria difíciles donde las formulaciones ILP tradicionales luchan con la escalabilidad.
2. El enfoque propuesto es complementario al ILP; es superior para grafos con diámetros crecientes, mientras que el ILP sigue siendo preferible para grafos de diámetro acotado.
3. El marco de trabajo cierra con éxito la brecha entre los límites teóricos y las soluciones exactas certificadas, proporcionando una herramienta robusta para determinar los números de radio en estructuras de grafos complejas.

Los autores concluyen que este enfoque ofrece una alternativa altamente competitiva a los solvers comerciales para clases de grafos específicas y destaca el potencial de la resolución incremental de SAT para otros problemas de etiquetado de grafos y optimización combinatoria.