A SAT-Based Exact Approach for Radio k-Labeling

Resumo Técnico: Uma Abordagem Exata Baseada em SAT para o Radio $k$-Labeling

Definição do Problema
O artigo aborda o problema do radio $k$-labeling (também conhecido como radio $k$-coloração), um problema de otimização combinatória derivado do problema de atribuição de canais. Dado um grafo conexo $G=(V, E)$ com diâmetro $k = \text{diam}(G)$, o objetivo é atribuir rótulos inteiros não negativos $f(v)$ aos vértices de modo que, para cada par de vértices distintos $u, v$, a condição $|f(u) - f(v)| \ge k + 1 - d(u, v)$ seja satisfeita, onde $d(u, v)$ é a distância do caminho mais curto. O objetivo é minimizar o span (amplitude) da rotulagem, definido como $\max_{v \in V} f(v)$. O menor span possível é o número de rádio, denotado por $rn(G)$.

Embora existam construções teóricas para famílias específicas de grafos (ex: caminhos, ciclos, árvores) e algoritmos heurísticos forneçam soluções viáveis para grafos gerais, soluções exatas para classes amplas de grafos permanecem escassas. As formulações existentes de Programação Linear Inteira (ILP) sofrem de problemas de escalabilidade devido ao crescimento rápido do espaço de busca e à falta de reutilização de informações entre as iterações de otimização.

Metodologia
Os autores propõem uma estrutura incremental baseada em SAT (satisfatibilidade de Booleanos) que combina uma codificação de ordem compacta com uma estratégia de otimização iterativa.

1. Codificações SAT:
   O artigo desenvolve duas codificações de satisfatibilidade booleana baseadas no domínio de rótulos $\{1, \dots, UB\}$, onde $UB$ é um limite superior pré-computado:

   • Codificação Direta (Direct Encoding): Utiliza variáveis de atribuição $x_{v,l}$ (verdadeiro se o vértice $v$ possui o rótulo $l$). Ela impõe restrições via cláusulas de conflito pareadas. Embora logicamente equivalente ao modelo ILP, requer $O(n^2 UB k)$ cláusulas para as restrições de rádio, o que leva a uma propagação fraca sob resolução de unidade.
   • Codificação de Ordem (Order Encoding): Introduz variáveis de limiar $g_{v,l}$ (verdadeiro se $f(v) \ge l$) juntamente com as variáveis de atribuição. Esta codificação representa a restrição de rádio $|f(u) - f(v)| \ge \Delta_{uv}$ de forma mais compacta. Ela reduz o número de cláusulas de restrição de rádio de $O(n^2 UB k)$ para $O(n^2 UB)$, eliminando a dependência de $k$ na contagem de cláusulas. A codificação de ordem também permite uma propagação mais forte, pois desigualdades como $f(v) \ge c$ mapeiam para literais únicos.

2. Estratégia de Resolução Incremental:
   A estrutura emprega um paradigma de resolução SAT incremental. Em vez de reconstruir a fórmula para cada iteração, uma única instância de solver é construída uma vez. O algoritmo procede da seguinte forma:

   • Fase 1: Computar todas as distâncias entre pares e definir $k = \text{diam}(G)$.
   • Fase 2: Construir o modelo SAT com um limite superior inicial $UB$.
   • Fase 3: Resolver a fórmula iterativamente. Se uma atribuição satisfatória for encontrada com span $\beta$, o solver é instruído a proibir qualquer span $\ge \beta$ (estreitando o limite) e resolver novamente. Crucialmente, as cláusulas aprendidas das iterações anteriores são preservadas, evitando o esforço de busca redundante. O loop termina quando o solver retorna UNSAT (certificando a otimalidade) ou atinge um limite de tempo.

3. Quebra de Simetria:
   Para grafos ciclo ($C_n$), que exibem simetria rotacional, os autores introduzem uma restrição de quebra de simetria fixando o rótulo do primeiro vértice em 1 ($f(0)=1$). Isso reduz o espaço de busca e acelera significativamente a prova de otimalidade sem descartar soluções ótimas.

Principais Contribuições

• Estrutura Inovadora: A primeira estrutura de otimização exata baseada em SAT para o problema de radio $k$-labeling, utilizando codificação de ordem e resolução incremental.
• Melhorias de Eficiência: A codificação de ordem reduz a complexidade de cláusulas e melicamente melhora a propagação em comparação com a codificação direta. A abordagem incremental reutiliza cláusulas aprendidas, reduzindo significativamente o overhead computacional em comparação com chamadas SAT independentes ou abordagens ILP padrão que descartam informações de busca anteriores.
• Tratamento de Simetria: A introdução de restrições específicas de quebra de simetria para grafos ciclo, demonstrando acelerações substanciais nos tempos de resolução e aumento no número de ótimos certificados.

Resultos Experimentais
A estrutura foi avaliada em 146 instâncias de benchmark através de nove famílias de grafos (caminhos, ciclos, cobras triangulares, cobras $kC_m$, escadas, livros, grafos de amizade e árvores binomiais) com um limite de tempo de 1.200 segundos.

• Desempenho vs. Heurísticas: O método Order-SAT estabeleceu 38 novos melhores números de rádio conhecidos entre as 98 instâncias sem um ótimo de forma fechada conhecido. Ele consistentemente produziu limites viáveis mais estreitos do que as heurísticas existentes (Ub1, Ub3) e a codificação direta SAT.
• Desempenho vs. ILP:
  • Grafos com Diâmetro Crescente: Para famílias onde o diâmetro cresce com o tamanho (ex: cobras, escadas, árvores binomiais), o Order-SAT superou os solvers ILP comerciais (CPLEX, Gurobi) tanto em qualidade de solução (limites mais estreitos) quanto no número de ótimos certificados. Os solvers ILP frequentemente esgotaram a memória ou retornaram limites superiores frouxos nessas instâncias.
  • Grafos com Diâmetro Limitado: Para famílias com diâmetro constante (ex: grafos livro, grafos amizade), os solvers ILP foram mais eficazes, certificando a otimalidade para todas as instâncias rapidamente.
• Abordagem Combinada: Ao combinar a estrutura SAT com modelos ILP, o estudo certificou soluções ótimas para 109 das 146 instâncias, expandindo substancialmente o conjunto de benchmarks de radio-labeling com otimalidade comprovada.
• Significância Estatística: Um teste de Friedman confirmou que o Order-SAT alcançou o melhor ranking geral (rank médio de 2,58) entre todos os métodos comparados, incluindo solvers comerciais e heurísticas.

Significância
O artigo afirma que a resolução incremental de SAT constitui um paradigma prático de otimização exata para problemas de rotulagem de grafos que tradicionalmente foram dominados por construções teóricas e algoritmos heurísticos. O trabalho demonstra que:

1. Os solvers SAT modernos, quando combinados com codificações compactas e estratégias incrementais, podem resolver problemas de otimização combinatória difíceis onde as formulações tradicionais de ILP lutam com a escalabilidade.
2. A abordagem proposta é complementar à ILP; ela é superior para grafos com diâmetros crescentes, enquanto a ILP permanece preferível para grafos de diâmetro limitado.
3. A estrutura faz a ponte com sucesso entre limites teóricos e soluções exatas certificadas, fornecendo uma ferramenta robusta para determinar números de rádio em estruturas de grafos complexas.

Os autores concluem que esta abordagem oferece uma alternativa altamente competitiva para solvers comerciais para classes específicas de grafos e destaca o potencial da resolução incremental de SAT para outros problemas de rotulagem de grafos e otimização combinatória.