A SAT-Based Exact Approach for Radio k-Labeling

Technische Samenvatting: Een SAT-gebaseerde exacte benadering voor Radio $k$-labeling

Probleemdefinitie
Het artikel behandelt het radio $k$-labeling probleem (ook bekend als radio $k$-kleuring), een combinatorisch optimalisatieprobleem afgeleid van het kanaaltoewijzingsprobleem. Gegeven een samenhangende graaf $G=(V, E)$ met diameter $k = \text{diam}(G)$, is het doel om niet-negatieve gehele labels $f(v)$ toe te wijzen aan knopen zodanig dat voor elk paar verschillende knopen $u, v$ de voorwaarde $|f(u) - f(v)| \ge k + 1 - d(u, v)$ geldt, waarbij $d(u, v)$ de kortste padafstand is. Het doel is om de span van de labeling te minimaliseren, gedefinieerd als $\max_{v \in V} f(v)$. De minimale mogelijke span is het radio getal, aangeduid als $rn(G)$.

Hoewel er theoretische constructies bestaan voor specifieke grafenfamilies (bijv. paden, cycli, bomen) en heuristische algoritmen werkbare oplossingen bieden voor algemene grafen, blijven exacte oplossingen voor brede grafenklassen schaars. Bestaande Integer Linear Programming (ILP) formuleringen lijden aan schaalbaarheidsproblemen door de snelle groei van de zoekruimte en het gebrek aan informatiehergebruik tussen optimalisatie-iteraties.

Methodologie
De auteurs stellen een exact, incrementeel SAT-gebaseerd framework voor dat een compacte order-encoding combineert met een iteratieve optimalisatiestrategie.

1. SAT-encodings:
   Het artikel ontwikkelt twee Boolean satisfiability (SAT) encodings gebaseerd op het labeldomein $\{1, \dots, UB\}$, waarbij $UB$ een vooraf berekende bovengrens is:

   • Direct Encoding: Gebruikt toewijzingsvariabelen $x_{v,l}$ (waar als knoop $v$ label $l$ heeft). Het handhaaft restricties via paren van conflictclausules. Hoewel logisch equivalent aan het ILP-model, vereist het $O(n^2 UB k)$ clausules voor radio-restricties, wat leidt tot zwakke propagatie onder unit resolution.
   • Order Encoding: Introduceert drempelvariabelen $g_{v,l}$ (waar $f(v) \ge l$) naast de toewijzingsvariabelen. Deze encoding representeert de radio-restrictie $|f(u) - f(v)| \ge \Delta_{uv}$ compacter. Het reduceert het aantal radio-restrictieclausules van $O(n^2 UB k)$ naar $O(n^2 UB)$ door de afhankelijkheid van $k$ in het aantal clausules te elimineren. De order encoding maakt ook sterkere propagatie mogelijk, aangezien ongelijkheden zoals $f(v) \ge c$ worden afgebeeld op enkele literalen.

2. Incrementele oplossingsstrategie:
   Het framework maakt gebruik van een incrementeel SAT-solving paradigma. In plaats van de formule voor elke iteratie opnieuw op te bouwen, wordt één enkele solver-instantie één keer geconstrueerd. Het algoritme verloopt als volgt:

   • Fase 1: Bereken alle-paren afstanden en stel $k = \text{diam}(G)$ in.
   • Fase 2: Bouw het SAT-model met een initiële bovengrens $UB$.
   • Fase 3: Los de formule iteratief op. Als er een bevredigende toewijzing wordt gevonden met span $\beta$, krijgt de solver de instructie om elke span $\ge \beta$ te verbieden (het aanscherpen van de bovengrens) en opnieuw op te lossen. Cruciaal is dat geleerde clausules uit vorige iteraties behouden blijven, waardoor redundante zoekinspanning wordt vermeden. De lus eindigt wanneer de solver UNSAT teruggeeft (wat optimaliteit certificeert) of wanneer een tijdslimiet is bereikt.

3. Symmetrie doorbreken:
   Voor cyclusgrafen ($C_n$), die rotationele symmetrie vertonen, introduceren de auteurs een symmetrie-doorbrekende restrictie die het label van de eerste knoop vastzet op 1 ($f(0)=1$). Dit vermindert de zoekruimte en versnelt het bewijs van optimaliteit aanzienlijk zonder optimale oplossingen weg te gooien.

Belangrijkste Bijdragen

• Nieuw Framework: Het eerste algemene exacte SAT-gebaseerde optimalisatieframework voor het radio $k$-labeling probleem, gebruikmakend van order encoding en incrementeel oplossen.
• Efficiëntieverbeteringen: De order encoding vermindert de clausulecomplexiteit en verbetert de propagatie vergeleken met direct encoding. De incrementele aanpak hergebruikt geleerde clausules, wat de computationele overhead aanzienlijk vermindert vergeleken met onafhankelijke SAT-aanroepen of standaard ILP-benaderingen die eerdere zoekinformatie weggooien.
• Symmetrie-afhandeling: De introductie van specifieke symmetrie-doorbrekende restricties voor cyclusgrafen, wat substantiële versnellingen in de oplostijden en een groter aantal gecertificeerde optima laat zien.

Experimentele Resultaten
Het framework werd geëvalueerd op 146 benchmark-instanties over negen grafenfamilies (paden, cycli, triangulaire slangen, $kC_m$-slangen, ladders, boeken, friendship-grafen en binomiale bomen) met een tijdslimiet van 1.200 seconden.

• Prestaties vs. Heuristieken: De voorgestelde Order-SAT methode vestigde 38 nieuwe best-bekende radio getallen onder de 98 instanties zonder een bekende gesloten vorm van het optimum. Het produceerde consistent nauwere werkbare grenzen dan bestaande heuristieken (Ub1, Ub3) en direct-encoding SAT.
• Prestaties vs. ILP:
  • Groeiende-diameter Grafen: Voor families waarbij de diameter meegroeit met de grootte (bijv. slangen, ladders, binomiale bomen), presteerde Order-SAT beter dan commerciële ILP-solvers (CPLEX, Gurobi) in zowel oplossingskwaliteit (nauwere grenzen) als in het aantal gecertificeerde optima. ILP-solvers raakten op deze instanties vaak het geheugen kwijt of gaven losse incumbent-oplossingen terug.
  • Constante-diameter Grafen: Voor families met een constante diameter (bijv. boek-grafen, friendship-grafen), waren ILP-solvers effectiever en certificeerden zij de optimaliteit voor alle instanties snel.
• Gecombineerde Aanpak: Door het SAT-framework te combineren met ILP-modellen, certificeerde de studie optimale oplossingen voor 109 van de 146 instanties, waarmee de set van radio-labeling benchmarks met bewezen optimaliteit aanzienlijk is uitgebreid.
• Statistische Significantie: Een Friedman-test bevestigde dat Order-SAT de beste algemene rangorde behaalde (gemiddelde rang 2,58) onder alle vergeleken methoden, inclusief commerciële solvers en heuristieken.

Betekenis
Het artikel stelt dat incrementeel SAT-solving een praktische exacte optimalisatieparadigma vormt voor grafen-labeling problemen die traditioneel werden gedomineerd door theoretische constructies en heuristische algoritmen. Het werk toont aan dat:

1. Moderne SAT-solvers, wanneer ze worden gecombineerd met compacte encodings en incrementele strategieën, moeilijke combinatorische optimalisatieproblemen kunnen oplossen waar traditionele ILP-formuleringen moeite hebben met schaalbaarheid.
2. De voorgestelde aanpak complementair is aan ILP; het is superieur voor grafen met groeiende diameters, terwijl ILP de voorkeur verdient voor grafen met een begrensde diameter.
3. Het framework succesvol de kloof overbrugt tussen theoretische grenzen en gecertificeerde exacte oplossingen, en biedt een robuust instrument voor het bepalen van radio getallen in complexe grafenstructuren.

De auteurs concluderen dat deze aanpak een zeer concurrerend alternatief biedt voor commerciële solvers voor specifieke grafenklassen en benadrukken het potentieel van incrementeel SAT-solving voor andere grafen-labeling en combinatorische optimalisatieproblemen.