A SAT-Based Exact Approach for Radio k-Labeling

Résumé Technique : Une approche exacte basée sur le SAT pour le $k$-étiquetage radio

Définition du Problème
L'article traite du problème du $k$-étiquetage radio (également connu sous le nom de $k$-coloration radio), un problème d'optimisation combinatoire dérivé du problème d'assignation de canaux. Étant donné un graphe connexe $G=(V, E)$ de diamètre $k = \text{diam}(G)$, l'objectif est d'assigner des étiquettes entières non négatives $f(v)$ aux sommets de telle sorte que pour chaque paire de sommets distincts $u, v$, la condition $|f(u) - f(v)| \ge k + 1 - d(u, v)$ soit respectée, où $d(u, v)$ est la distance du plus court chemin. Le but est de minimiser l'étendue (span) de l'étiquetage, définie par $\max_{v \in V} f(v)$. L'étendue minimale possible est le nombre radio, noté $rn(G)$.

Bien que des constructions théoriques existent pour des familles de graphes spécifiques (ex. : chemins, cycles, arbres) et que des algorithmes heuristiques fournissent des solutions réalisables pour des graphes généraux, les solutions exactes pour de larges classes de graphes restent rares. Les formulations existantes de programmation linéaire en nombres entiers (ILP) souffrent de problèmes d'évolutivité dus à la croissance rapide de l'espace de recherche et au manque de réutilisation d'informations entre les itérations d'optimisation.

Méthodologie
Les auteurs proposent un cadre exact et incrémental basé sur le SAT qui combine un codage d'ordre compact avec une stratégie d'optimisation itérative.

1. Codages SAT :
   L'article développe deux codages de satisfaisabilité booléenne (SAT) basés sur le domaine d'étiquetage $\{1, \dots, UB\}$, où $UB$ est une borne supérieure précalculée :

   • Codage Direct : Utilise des variables d'assignation $x_{v,l}$ (vraie si le sommet $v$ possède l'étiquette $l$). Il impose les contraintes via des clauses de conflit par paire. Bien qu'équivalent logiquement au modèle ILP, il nécessite $O(n^2 UB k)$ clauses pour les contraintes radio, ce qui entraîne une faible propagation sous résolution unitaire.
   • Codage d'Ordre (Order Encoding) : Introduit des variables de seuil $g_{v,l}$ (vraie si $f(v) \ge l$) aux côtés des variables d'assignation. Ce codage représente la contrainte radio $|f(u) - f(v)| \ge \Delta_{uv}$ de manière plus compacte. Il réduit le nombre de clauses de contrainte radio de $O(n^2 UB k)$ à $O(n^2 UB)$ en éliminant la dépendance vis-à-vis de $k$ dans le décompte des clauses. Le codage d'ordre permet également une propagation plus forte, car les inégalités de type $f(v) \ge c$ se traduisent par des littéraux uniques.

2. Stratégie de Résolution Incrémentale :
   Le cadre emploie un paradigme de résolution SAT incrémentale. Au lieu de reconstruire la formule pour chaque itération, une instance unique de solveur est construite une seule fois. L'algorithme procède comme suit :

   • Phase 1 : Calculer toutes les distances par paires et fixer $k = \text{diam}(G)$.
   • Phase 2 : Construire le modèle SAT avec une borne supérieure initiale $UB$.
   • Phase 3 : Résoudre la formule de manière itérative. Si une assignation satisfaisante est trouvée avec une étendue $\beta$, le solveur reçoit l'instruction d'interdire toute étendue $\ge \beta$ (resserrement de la borne) et de résoudre à nouveau. Crucialement, les clauses apprises des itérations précédentes sont préservées, évitant ainsi un effort de recherche redondant. La boucle se termine lorsque le solveur retourne UNSAT (certifiant l'optimalité) ou qu'une limite de temps est atteinte.

3. Rupture de Symétrie :
   Pour les graphes cycles ($C_n$), qui présentent une symétrie de rotation, les auteurs introduisent une contrainte de rupture de symétrie fixant l'étiquette du premier sommet à 1 ($f(0)=1$). Cela réduit l'espace de recherche et accélère considérablement la preuve d'optimalité sans rejeter de solutions optimales.

Contributions Clés

• Nouveau Cadre : Le premier cadre d'optimisation exact basé sur le SAT pour le problème de $k$-étiquetage radio, utilisant le codage d'ordre et la résolution incrémentale.
• Améliorations d'Efficacité : Le codage d'ordre réduit la complexité des clauses et améliore la propagation par rapport au codage direct. L'approche incrémentale réutilise les clauses apprises, réduisant considérablement la surcharge de calcul par rapport aux appels SAT indépendants ou aux approches ILP standards qui rejettent les informations de recherche précédentes.
• Gestion de la Symétrie : L'introduction de contraintes de rupture de symétrie spécifiques pour les graphes cycles, démontrant des accélérations substantielles des temps de résolution et une augmentation du nombre d'optima certifiés.

Résultats Expérimentaux
Le cadre a été évalué sur 146 instances de référence à travers neuf familles de graphes (chemins, cycles, serpents triangulaires, serpents $kC_m$, échelles, livres, graphes d'amitié et arbres binomiaux) avec une limite de temps de 1 200 secondes.

• Performance vs Heuristiques : La méthode Order-SAT proposée a établi 38 nouveaux meilleurs nombres radio connus parmi les 98 instances sans optimum à forme fermée connu. Elle a systématiquement produit des bornes réalisables plus serrées que les heuristiques existantes (Ub1, Ub3) et le SAT à codage direct.
• Performance vs ILP :
  • Graphes à Diamètre Croissant : Pour les familles où le diamètre croît avec la taille (ex. : serpents, échelles, arbres binomiaux), Order-SAT a surpassé les solveurs ILP commerciaux (CPLEX, Gurobi) tant en qualité de solution (bornes plus serrées) qu'en nombre d'optima certifiés. Les solveurs ILP ont souvent épuisé la mémoire ou renvoyé des solutions entrantes trop lâches sur ces instances.
  • Graphes à Diamètre Borné : Pour les familles à diamètre constant (ex. : graphes livres, graphes d'amitié), les solveurs ILP se sont montrés plus efficaces, certifiant l'optimalité pour toutes les instances rapidement.
• Approche Combinée : En combinant le cadre SAT avec des modèles ILP, l'étude a certifié des solutions optimales pour 109 des 146 instances, élargissant substantiellement l'ensemble des références de l'étiquetage radio avec une optimalité prouvée.
• Signification Statistique : Un test de Friedman a confirmé qu'Order-SAT a obtenu le meilleur classement global (rang moyen de 2,58) parmi toutes les méthodes comparées, y compris les solveurs commerciaux et les heuristiques.

Signification
L'article affirme que la résolution SAT incrémentale constitue un paradigme d'optimisation exacte pratique pour les problèmes d'étiquetage de graphes qui ont traditionnellement été dominés par des constructions théoriques et des algorithmes heuristiques. Le travail démontre que :

1. Les solveurs SAT modernes, lorsqu'ils sont combinés à des codages compacts et des stratégies incrémentales, peuvent résoudre des problèmes d'optimisation combinatoire difficiles là où les formulations ILP traditionnelles peinent en raison de leur évolutivité.
2. L'approche proposée est complémentaire à l'ILP ; elle est supérieure pour les graphes à diamètre croissant, tandis que l'ILP reste préférable pour les graphes à diamètre borné.
3. Le cadre comble avec succès le fossé entre les bornes théoriques et les solutions exactes certifiées, fournissant un outil robuste pour déterminer les nombres radio dans des structures de graphes complexes.

Les auteurs concluent que cette approche offre une alternative hautement compétitive aux solveurs commerciaux pour certaines classes de graphes et souligne le potentiel de la résolution SAT incrémentale pour d'autres problèmes d'étiquetage de graphes et d'optimisation combinatoire.