A SAT-Based Exact Approach for Radio k-Labeling

Sintesi Tecnica: Un approccio esatto basato su SAT per il radio $k$-labeling

Definizione del Problema
Il documento affronta il problema del radio $k$-labeling (noto anche come radio $k$-coloring), un problema di ottimizzazione combinatoria derivato dal problema dell'assegnazione dei canali. Dato un grafo connesso $G=(V, E)$ con diametro $k = \text{diam}(G)$, l'obiettivo è assegnare etichette intere non negative $f(v)$ ai vertici tali che per ogni coppia di vertici distinti $u, v$, la condizione $|f(u) - f(v)| \ge k + 1 - d(u, v)$ sia soddisfatta, dove $d(u, v)$ è la distanza del cammino minimo. L'obiettivo è minimizzare l'estensione (span) della etichettatura, definita come $\max_{v \in V} f(v)$. La minima estensione possibile è il numero radio, indicato con $rn(G)$.

Sebbene esistano costruzioni teoriche per specifiche famiglie di grafi (es. cammini, cicli, alberi) e algoritmi euristici forniscono soluzioni ammissibili per grafi generici, rimangono scarse le soluzioni esatte per classi di grafi ampie. Le formulazioni esistenti di Programmazione Lineare Intera (ILP) soffrono di problemi di scalabilità dovuti alla rapida crescita dello spazio di ricerca e alla mancanza di riutilizzo delle informazioni tra le iterazioni di ottimizzazione.

Metodologia
Gli autori propongono un framework incrementale esatto basato su SAT che combina una codifica d'ordine compatta con una strategia di ottimizzazione iterativa.

1. Codifiche SAT:
   Il documento sviluppa due codifiche di soddisfacibilità booleana (SAT) basate sul dominio delle etichette $\{1, \dots, UB\}$, dove $UB$ è un limite superiore precomputato:

   • Codifica Diretta (Direct Encoding): Utilizza variabili di assegnazione $x_{v,l}$ (vera se il vertice $v$ ha l'etichetta $l$). Essa impone i vincoli tramite clausole di conflitto a coppie. Sebbene logicamente equivalente al modello ILP, richiede $O(n^2 UB k)$ clausole per i vincoli radio, portando a una debole propagazione sotto la risoluzione unitaria.
   • Codifica d'Ordine (Order Encoding): Introduce variabili di soglia $g_{v,l}$ (vera se $f(v) \ge l$) insieme alle variabili di assegnazione. Questa codifica rappresenta il vincolo radio $|f(u) - f(v)| \ge \Delta_{uv}$ in modo più compatto. Riduce il numero di clausole dei vincoli radio da $O(n^2 UB k)$ a $O(n^2 UB)$ eliminando la dipendenza da $k$ nel conteggio delle clausole. La codifica d'ordine consente anche una propagazione più forte, poiché le disuguaglianze come $f(v) \ge c$ mappano in singoli letterali.

2. Strategia di Risoluzione Incrementale:
   Il framework impiega un paradigma di risoluzione SAT incrementale. Inve แทน di ricostruire la formula per ogni iterazione, viene costruito un unico istanza del solver. L'algoritmo procede come segue:

   • Fase 1: Calcolare tutte le distanze tra le coppie e impostare $k = \text{diam}(G)$.
   • Fase 2: Costruire il modello SAT con un limite superiore iniziale $UB$.
   • Fase 3: Risolvere iterativamente la formula. Se viene trovata un'assegnazione soddisfacente con estensione $\beta$, il solver riceve l'istruzione di proibire qualsiasi estensione $\ge \beta$ (restringendo il limite) e risolvere nuovamente. Fondamentalmente, le clausole apprese (learned clauses) dalle iterazioni precedenti vengono preservate, evitando sforzi di ricerca ridondanti. Il ciclo termina quando il solver restituisce UNSAT (certificando l'ottimalità) o raggiunge un limite di tempo.

3. Rottura della Simmetria (Symmetry Breaking):
   Per i grafi ciclo ($C_n$), che esibiscono simmetria rotazionale, gli autori introducono un vincolo di rottura della simmetria che fissa l'etichetta del primo vertice a 1 ($f(0)=1$). Ciò riduce lo spazio di ricerca e accelera significativamente la prova di ottimalità senza scartare soluzioni ottimali.

Contributi Chiave

• Framework Innovativo: Il primo framework di ottimizzazione esatta basato su SAT per il problema del radio $k$-labeling, che utilizza la codifica d'ordine e la risoluzione incrementale.
• Miglioramenti dell'Efficienza: La codifica d'ordine riduce la complessità delle clausole e migliora la propagazione rispetto alla codifica diretta. L'approccio incrementale riutilizza le clausole apprese, riducendo significativamente l'overhead computazionale rispetto alle chiamate SAT indipendenti o agli approcci ILP standard che scartano le informazioni di ricerca precedenti.
• Gestione della Simmetria: L'introduzione di vincoli specifici di rottura della simmetria per i grafi ciclo dimostra sostanziali accelerazioni nei tempi di risoluzione e un aumento del numero di ottimi certificati.

Risultati Sperimentali
Il framework è stato valutato su 146 istanze di benchmark attraverso nove famiglie di grafi (cammini, cicli, serpenti triangolari, serpenti $kC_m$, scale, libri, grafi amicizia e alberi binomiali) con un limite di tempo di 1.200 secondi.

• Performance vs Euristiche: Il metodo proposto Order-SAT ha stabilito 38 nuovi migliori numeri radio noti tra le 98 istanze senza un ottimo a forma chiusa noto. Ha prodotto costantemente limiti ammissibili più stretti rispetto alle euristiche esistenti (Ub1, Ub3) e alla SAT a codifica diretta.
• Performance vs ILP:
  • Grafi con Diametro Crescente: Per le famiglie in cui il diametro cresce con la dimensione (es. serpenti, scale, alberi binomiali), Order-SAT ha superato i solver ILP commerciali (CPLEX, Gurobi) sia in termini di qualità della soluzione (limiti più stretti) che nel numero di ottimi certificati. I solver ILP spesso esaurivano la memoria o restituivano incumbent meno stringenti su queste istanze.
  • Grafi a Diametro Limitato: Per le famiglie con diametro costante (es. grafi libro, grafi amicizia), i solver ILP sono stati più efficaci, certificando l'ottimalità per tutte le istanze rapidamente.
• Approccio Combinato: Combinando il framework SAT con i modelli ILP, lo studio ha certificato soluzioni ottime per 109 delle 146 istanze, espandendo sostanzialmente l'insieme dei benchmark del radio-labeling con ottimalità provata.
• Significatività Statistica: Un test di Friedman ha confermato che Order-SAT ha ottenuto il miglior ranking complessivo (rank medio 2.58) tra tutti i metodi confrontati, inclusi i solver commerciali ed euristici.

Significatività
Il documento afferma che la risoluzione SAT incrementale costituisce un paradigma di ottimizzazione esatta pratico per i problemi di etichettatura di grafi che sono stati tradizionalmente dominati da costruzioni teoriche e algoritmi euristici. Il lavoro dimostra che:

1. I moderni solver SAT, se combinati con codifiche compatte e strategie incrementali, possono risolvere difficili problemi di ottimizzazione combinatoria dove le formulazioni ILP tradizionali faticano con la scalabilità.
2. Il metodo proposto è complementare all'ILP; è superiore per grafi con diametri crescenti, mentre l'ILP rimane preferibile per grafi a diametro limitato.
3. Il framework colma con successo il divario tra i limiti teorici e le soluzioni esatte certificate, fornendo uno strumento robusto per determinare i numeri radio in strutture di grafi complesse.

Gli autori concludono che questo approccio offre un'alternativa altamente competitiva ai solver commerciali per specifiche classi di grafi e sottolinea il potenziale della risoluzione SAT incrementale per altri problemi di etichettatura di grafi e di ottimizzazione combinatoria.