Resumo Técnico: Codificações SAT para Coloração de Largura de Banda

Definição do Problema

O Problema de Coloração de Largura de Banda (BCP - Bandwidth Coloring Problem) é uma generalização do Problema de Coloração de Grafos (GCP), onde as arestas carregam pesos inteiros positivos $d(u, v)$. O objetivo é atribuir uma cor $c(v) \in \mathbb{N}$ a cada vértice $v$ de modo que a restrição de distância $|c(u) - c(v)| \ge d(u, v)$ seja satisfeita para cada aresta $\{u, v\} \in E$. O objetivo é minimizar o span (amplitude), definido como a cor máxima atribuída a qualquer vértice.

O BCP surge naturalmente em problemas de atribuição de frequência (FAP - Frequency Assignment Problems) para redes sem fio e celulares, onde os vértices representam transmissores e os pesos das arestas representam as separações mínimas de frequência necessárias para evitar interferência eletromagnética. Embora existam métodos metaheurísticos, eles carecem de garantias de otimalidade. Métodos exatos baseados em Programação Linear Inteira (ILP) e Programação de Restrições (CP) têm sido estudados, mas as formulações de ILP frequentemente sofrem com uma contagem de restrições que cresce com os pesos das arestas. Recentemente, abordagens baseadas em SAT emergiram como estado da arte para resolução exata, contudo, o espaço de design para codificações SAT especificamente adaptadas ao BCP permanece amplamente inexplorado.

Metodologia

O artigo apresenta um estudo de design sistemático de codificações SAT para o BCP, propondo um framework unificado que explora seis métodos de codificação distintos organizados em três categorias. O framework avalia o impacto de três recursos configuráveis: resolução incremental, quebra de simetria e estratégias de largura de bloco.

1. Categorias de Codificação

O framework implementa e compara os seguintes métodos de codificação:

• Codificações de Uma Variável (1G, 1L): Estas utilizam variáveis de ordenação para definir implicitamente as atribuições de cores.
  • 1G (Greater-than): Utiliza variáveis $y_{u,j}$ onde $y_{u,j} = \text{true} \iff c(u) \ge j$.
  • 1L (Less-than): Utiliza variáveis $y_{u,j}$ onde $y_{u,j} = \text{true} \iff c(u) \le j$.
  • Estes métodos possuem uma contagem assintótica de cláusulas de $O(k(n+m))$, independente dos pesos das arestas.
• Codificações de Duas Variáveis (2G, 2L): Estas mantêm explicitamente tanto as variáveis de atribuição ($x_{u,j}$) quanto as variáveis de ordenação ($y_{u,j}$) para permitir restrições de distância mais diretas.
  • 2G/2L: Semântica semelhante a 1G/1L, mas inclui restrições de canalização (channeling) que ligam as variáveis $x$ e $y$.
• Codificações de Bloco (X, Xa): Estas particionam o intervalo de cores em blocos de largura fixa e utilizam variáveis de intervalo auxiliares ($R_{u,a,b}$) para representar somas de variáveis de atribuição dentro dos blocos.
  • X: Codifica operações de subtração (necessárias para somas de intervalos dentro dos blocos) diretamente, sem variáveis auxiliares.
  • Xa: Introduz variáveis auxiliares para representar termos de subtração, permitindo o reuso de cláusulas.
  • As codificações de bloco visam reduzir o número de cláusulas para restrições de distância, particularmente quando os pesos das arestas são grandes.

2. Recursos Configuráveis

• Resolução Incremental: O framework testa se o reuso de cláusulas aprendidas entre iterações (conforme o limite superior do span diminui) melhora o desempenho. Isso é implementado usando suposições (assumptions) de SAT.
• Quebra de Simetria: Uma técnica baseada em reflexão é aplicada ao vértice de maior grau, restringindo sua cor à metade inferior do intervalo do span ($c(h) \le \lfloor k/2 \rfloor$). Isso explora a propriedade de que se $c$ é uma coloração válida, $c'(v) = k+1-c(v)$ também é válida.
• Estratégias de Largura de Bloco: Para codificações de bloco, o framework compara blocos de largura fixa (padrão $w=8$) contra blocos de largura variável (onde a largura é determinada pelo peso da aresta incidente máxima de um vértice).

3. Configuração Experimental

O estudo avalia 36 configurações distintas (combinações dos 6 métodos e recursos) em 51 instâncias de benchmark:

• Conjunto GEOM: 33 grafos aleatórios geométricos (GEOM20 a GEOM120).
• Conjunto MS-CAP: 18 instâncias derivadas de problemas de atribuição de frequência de redes celulares.
• Solver: CaDiCaL 1.9.5 com um limite de tempo de 3600 segundos por instância.
• Baseline: Comparações são feitas contra as codificações SAT de última geração POP-S-B e POPH-S-B (Faber et al., 2024).

Principais Resultados

Desempenho Geral

O framework proposto atinge o estado da arte em desempenho. A configuração de melhor desempenho, Codificação de Bloco Xa (com largura fixa, resolução incremental e quebra de simetria), resolveu todas as 51 instâncias com um tempo total de 2721,3 segundos. Isso representa uma redução de 6,3% no tempo total em comparação ao estado da arte anterior POPH-S-B (2904,6s) e uma redução de 17,7% em relação ao POP-S-B (3307,5s).

Desempenho de Instância Difícil (GEOM120b)

Uma descoberta crítica diz respeito à instância mais difícil, GEOM120b:

• Métodos anteriores (POPH-S-B e POP-S-B) não conseguiram resolver a GEOM120b até a otimalidade comprovada dentro do limite de uma hora.
• O proposto Codificações de Bloco (X e Xa) resolveu a GEOM120b para otimalidade em aproximadamente 1000 segundos (especificamente, a configuração base Xa resolveu-a em 851,4s, e a Xa totalmente otimizada em 1011,6s).
• Isso demonstra um fator de aceleração de aproximadamente 2x sobre as melhores abordagens baseadas em SAT anteriores para esta instância específica.

Efeitos de Interação

O estudo revela efeitos de interação significativos entre escolhas de codificação e configurações do solver:

• Resolução Incremental: Proporciona acelerações substanciais para Codificações de Bloco (ex: melhoria de 24,4% para Xa) porque a estrutura de escada do bloco permanece amplamente estável conforme o span diminui. Por outro lado, não oferece benefício (ou causa leve degradação) para Codificações de Uma Variável (1G, 1L) porque as restrições de ordem são redefinidas em relação ao novo limite superior, invalidando as cláusulas aprendidas.
• Quebra de Simetria: Sua eficácia é altamente dependente da codificação. Melhora significativamente o desempenho para POP-S-B (aceleração de 24,5%) e 1L (aceleração de 13,2%), mas degrada o desempenho para 2G (desaceleração de 11,9%) e POPH-S-B (desaceleração de 11,4%).
• Largura de Bloco: A escolha entre larguras de bloco fixas e variáveis teve impacto mínimo (<1,2% de diferença) nas 50 instâncias padrão, sugerindo que o aprendizado de cláusulas do solver se adapta bem a ambas as estratégias.

Tamanho da Codificação vs. Eficiência

Ao contrário da intuição de que menos variáveis e cláusulas geram uma resolução mais rápida, a codificação Xa (que gera 7x mais variáveis e 5,5x mais cláusulas que a codificação 1G mais compacta) alcançou os tempos de resolução mais rápidos. Isso apoia o princípio de que variáveis auxiliares podem fortalecer a propagação de unidade, criando "atalhos" para o solver derivar implicações de forma mais eficiente.

Significância e Alegações

O artigo afirma que seu estudo de design sistemático preenche uma lacuna na literatura em relação às codificações SAT para o BCP. Embora a quebra de simetria e a resolução incremental tenham sido estudadas para o GCP, sua aplicação e interação com codificações específicas do BCP não foram investigadas anteriormente.

As principais contribuições são:

1. Resolver o Irresolúvel: O framework é o primeiro a resolver o benchmark GEOM120b para otimalidade comprovada dentro de um tempo razoável, uma tarefa que métodos exatos anteriores não puderam completar em uma hora.
2. Framework Unificado: Fornece um estudo comparativo abrangente de seis métodos de codificação e seus recursos configuráveis, identificando que as Codificações de Bloco são superiores para as instâncias mais difíceis, enquanto as Codificações Baseadas em Ordem (como 2L e 1G) oferecem um compromisso favorável entre complexidade de implementação e desempenho para casos gerais.
3. Insights de Interação: O trabalho destaca que os recursos de codificação não operam de forma independente. Especificamente, a resolução incremental e a quebra de simetria devem ser selecionadas cuidadosamente com base no tipo específico de codificação, pois podem gerar efeitos sinérgicos ou antagônicos.

Os autores concluem que, embora as codificações de bloco ofereçam o melhor desempenho nas instâncias mais desafiadoras, a exploração sistemática das escolhas de design de codificação é essencial para o avanço dos solvers exatos de BCP. Sugere-se como trabalho futuro a extensão do framework para o Problema de Multicoloração de Largura de Banda (BMCP) e o desenvolvimento de mecanismos de seleção de configuração adaptativa.