Resumen Técnico: Codificaciones SAT para la Coloración de Ancho de Banda

Definición del Problema

El Problema de Coloración de Ancho de Banda (BCP) es una generalización del Problema de Coloración de Grafos (GCP) donde las aristas portan pesos enteros positivos $d(u, v)$. El objetivo es asignar un color $c(v) \in \mathbb{N}$ a cada vértice $v$ de tal manera que se satisfaga la restricción de distancia $|c(u) - c(v)| \ge d(u, v)$ para cada arista $\{u, v\} \in E$. El objetivo es minimizar el ancho de banda (span), definido como el color máximo asignado a cualquier vértice.

El BCP surge naturalmente en los problemas de asignación de frecuencias (FAP) para redes inalámbricas y celulares, donde los vértices representan transmisores y los pesos de las aristas representan las separaciones mínimas de frecuencia requeridas para evitar la interferencia electromagnética. Aunque existen métodos metaheurísticos, estos carecen de garantías de optimalidad. Se han estudiado métodos exactos basados en Programación Lineal Entera (ILP) y Programación de Restricciones (CP), pero las formulaciones de ILP a menudo sufren de un recuento de restricciones que crece con los pesos de las aristas. Recientemente, han surgido enfoques basados en SAT como el estado del arte para la resolución exacta, aunque el espacio de diseño para las codificaciones SAT específicamente adaptadas al BCP permanece en gran medida inexplorado.

Metodología

El artículo presenta un estudio de diseño sistemático de codificaciones SAT para el BCP, proponiendo un marco unificado que explora seis métodos de codificación distintos organizados en tres categorías. El marco evalúa el impacto de tres características configurables: resolución incremental, ruptura de simetría y estrategias de ancho de bloque.

1. Categorías de Codificación

El marco implementa y compara los siguientes métodos de codificación:

• Codificaciones de Una Variable (1G, 1L): Estas utilizan variables de ordenamiento para definir implícitamente las asignaciones de color.
  • 1G (Greater-than / Mayor que): Utiliza variables $y_{u,j}$ donde $y_{u,j} = \text{true} \iff c(u) \ge j$.
  • 1L (Less-than / Menor que): Utiliza variables $y_{u,j}$ donde $y_{u,j} = \text{true} \iff c(u) \le j$.
  • Estos métodos tienen un recuento de cláusulas asintótico de $O(k(n+m))$, independiente de los pesos de las aristas.
• Codificaciones de Dos Variables (2G, 2L): Estas mantienen explícitamente tanto las variables de asignación ($x_{u,j}$) como las variables de ordenamiento ($y_{u,j}$) para permitir restricciones de distancia más directas.
  • 2G/2L: Semántica similar a 1G/1L pero incluye restricciones de canalización que vinculan las variables $x$ e $y$.
• Codificaciones de Bloque (X, Xa): Estas particionan el rango de colores en bloques de ancho fijo y utilizan variables de rango auxiliares ($R_{u,a,b}$) para representar sumas de variables de asignación dentro de los bloques.
  • X: Codifica las operaciones de sustracción (requeridas para las sumas de rango dentro de los bloques) directamente sin variables auxiliares.
  • Xa: Introduce variables auxiliares para representar términos de sustracción, permitiendo la reutilización de cláusulas.
  • Las codificaciones de bloque buscan reducir el número de cláusulas para las restricciones de distancia, particularmente cuando los pesos de las aritas son grandes.

2. Características Configurables

• Resolución Incremental: El marco prueba si la reutilización de cláusulas aprendidas a través de las iteraciones (mientras el límite superior del ancho de banda disminuye) mejora el rendimiento. Esto se implementa mediante supuestos (assumptions) de SAT.
• Ruptura de Simetría: Se aplica una técnica basada en reflexión al vértice de mayor grado, restringiendo su color a la mitad inferior del rango del ancho de banda ($c(h) \le \lfloor k/2 \rfloor$). Esto aprovecha la propiedad de que si $c$ es una coloración válida, $c'(v) = k+1-c(v)$ también lo es.
• Estrategias de Ancho de Bloque: Para las codificaciones de bloque, el marco compara bloques de ancho fijo (ancho predeterminado $w=8$) contra bloques de ancho variable (donde el ancho está determinado por el peso de la arista incidente máxima de un vértice).

3. Configuración Experimental

El estudio evalúa 36 configuraciones distintas (combinaciones de los 6 métodos y características) en 51 instancias de referencia:

• Conjunto GEOM: 33 grafos aleatorios geométricos (GEOM20 a GEOM120).
• Conjunto MS-CAP: 18 instancias derivadas de problemas de asignación de frecuencias de redes celulares.
• Solver: CaDiCaL 1.9.5 con un límite de tiempo de 3600 segundos por instancia.
• Línea Base: Las comparaciones se realizan contra las codificaciones SAT de última generación POP-S-B y POPH-S-B (Faber et al., 2024).

Resultados Clave

Rendimiento General

El marco propuesto logra un rendimiento de estado del arte. La mejor configuración, Codificación de Bloque Xa (con ancho fijo, resolución incremental y ruptura de simetría), resolvió todas las 51 instancias con un tiempo total de 2721.3 segundos. Esto representa una reducción del 6.3% en el tiempo total comparado con el estado del arte anterior POPH-S-B (2904.6s) y una reducción del 17.7% comparado con POP-S-B (3307.5s).

Rendimiento de Instancias Difíciles (GEOM120b)

Un hallazgo crítico concierne a la instancia más difícil, GEOM120b:

• Los métodos anteriores (POPH-S-B y POP-S-B) no lograron resolver GEOM120b hasta la optimalidad probada dentro del límite de una hora.
• Las Codificaciones de Bloque propuestas (X y Xa) resolvieron GEOM120b hasta la optimalidad en aproximadamente 1000 segundos (específicamente, la configuración base Xa la resolvió en 851.4s, y la Xa totalmente optimizada en 1011.6s).
• Esto demuestra un factor de aceleración de aproximadamente 2x sobre los mejores enfoques basados en SAT previos para esta instancia específica.

Efectos de Interacción

El estudio revela efectos de interacción significativos entre la elección de la codificación y la configuración del solver:

• Resolución Incremental: Proporciona aceleraciones sustanciales para las Codificaciones de Bloque (por ejemplo, una mejora del 24.4% para Xa) porque la estructura de escalera de los bloques permanece mayormente estable a medida que el ancho de banda disminuye. Por el contrario, no ofrece beneficios (o incluso causa degradación) para las Codificaciones de Una Variable (1G, 1L) debido a que las restricciones de ordenamiento se redefinen respecto al nuevo límite superior, invalidando las cláusulas aprendidas.
• Ruptura de Simetría: Su efectividad depende altamente de la codificación. Mejora significativamente el rendimiento para POP-S-B (aceleración del 24.5%) y 1L (aceleración del 13.2%), pero degrada el rendimiento para 2G (desaceleración del 11.9%) y POPH-S-B (desaceleración del 11.4%).
• Ancho de Bloque: La elección entre anchos de bloque fijos o variables tuvo un impacto mínimo (<1.2% de diferencia) en las 50 instancias estándar, lo que sugiere que el aprendizaje de cláusulas del solver se adapta bien a ambas estrategias.

Tamaño de la Codificación vs. Eficiencia

Contrario a la intuición de que menos variables y cláusulas producen una resolución más rápida, la codificación Xa (que genera 7 veces más variables y 5.5 veces más cláusulas que la codificación 1G más compacta) logró los tiempos de resolución más rápidos. Esto respalda el principio de que las variables auxiliares pueden fortalecer la propagación de unidades, creando "atajos" para que el solver derive implicaciones de manera más eficiente.

Significado y Reivindicaciones

El artículo afirma que su estudio de diseño sistemático llena un vacío en la literatura respecto a las codificaciones SAT para el BCP. Aunque la ruptura de simetría y la resolución incremental han sido estudiadas para el GCP, su aplicación e interacción con las codificaciones específicas de BCP no habían sido investigadas previamente.

Las contribuciones primarias son:

1. Resolver lo No Resuelto: El marco es el primero en resolver el benchmark GEOM120b hasta la optimalidad probada en un tiempo razonable, una tarea que los métodos exactos previos no pudieron completar en una hora.
2. Marco Unificado: Proporciona un estudio comparativo exhaustivo de seis métodos de codificación y sus características configurables, identificando que las Codificaciones de Bloque son superiores para las instancias más difíciles, mientras que las Codificaciones Basadas en Orden (como 2L y 1G) ofrecen un equilibrio favorable entre complejidad de implementación y rendimiento para casos generales.
3. Perspectivas de Interacción: El trabajo destaca que las características de codificación no operan de forma independiente. Específicamente, la resolución incremental y la ruptura de simetría deben seleccionarse cuidadosamente según el tipo de codificación específico, ya que pueden producir efectos sinérgicos o antagónicos.

Los autores concluyen que, si bien las codificaciones de bloque ofrecen el mejor rendimiento en las instancias más desafiantes, la exploración sistemática de las elecciones de diseño de codificación es esencial para avanzar en los solvers exactos de BCP. Se sugiere como trabajo futuro la extensión de este marco al Probleo de Multicoloreación de Ancho de Banda (BMCP) y el desarrollo de mecanismos de selección de configuración adaptativos.