Technische Samenvatting: SAT-encodings voor Bandbreedtekleuring

Probleemdefinitie

Het Bandbreedtekleuringsprobleem (Bandwidth Coloring Problem, BCP) is een generalisatie van het Grafiekkleuringsprobleem (Graph Coloring Problem, GCP), waarbij randen positieve gehele gewichten $d(u, v)$ dragen. Het doel is om aan elke vertex $v$ een kleur $c(v) \in \mathbb{N}$ toe te wijzen zodat de afstandsomstandigheid $|c(u) - c(v)| \ge d(u, v)$ wordt voldaan voor elke rand $\{u, v\} \in E$. Het doel is om de span te minimaliseren, gedefinieerd als de maximale kleur toegewezen aan een vertex.

Het BCP komt van nature voor in frequentietoewijzingsproblemen (Frequency Assignment Problems, FAP) voor draadloze en cellulaire netwerken, waarbij vertices zenders vertegenwoordigen en randgewichten de minimale frequentieseparatie vertegenwoordigen die vereist is om elektromagnetische interferentie te voorkomen. Hoewel metaheuristische methoden bestaan, ontbreken optimaliteitsgaranties. Exacte methoden gebaseerd op Integer Lineaire Programmering (ILP) en Constraint Programming (CP) zijn bestudeerd, maar ILP-formuleringen lijden vaak aan een aantal restricties dat meegroeit met de randgewichten. Recentelijk zijn SAT-gebaseerde benaderingen opgekomen als state-of-the-art voor exact oplossen, maar de ontwerpplek voor SAT-encodings die specifiek zijn afgestemd op BCP blijft grotendeels onverkend.

Methodologie

Het artikel presenteert een systematische designstudie van SAT-encodings voor het BCP, en stelt een verenigd framework voor dat zes verschillende encodingmethoden onderzoekt, georganiseerd in drie categorieën. Het framework evalueert de impact van drie configureerbare kenmerken: incrementeel oplossen, symmetriebreking en blokbreedtestrategieën.

1. Encodingcategorieën

Het framework implementeert en vergelijkt de volgende encodingmethoden:

• One-Variable Encodings (1G, 1L): Deze gebruiken ordeningsvariabelen om kleurtoewijzingen impliciet te definiiden.
  • 1G (Greater-than): Gebruikt variabelen $y_{u,j}$ waar $y_{u,j} = \text{true} \iff c(u) \ge j$.
  • 1L (Less-than): Gebruikt variabelen $y_{u,j}$ waar $y_{u,j} = \text{true} \iff c(u) \le j$.
  • Deze methoden hebben een asymptotisch aantal clausules van $O(k(n+m))$, onafhankelijk van de randgewichten.
• Two-Variable Encodings (2G, 2L): Deze onderhouden expliciet zowel toewijzingsvariabelen ($x_{u,j}$) als ordeningsvariabelen ($y_{u,j}$) om directere afstandrestricties mogelijk te maken.
  • 2G/2L: Vergelijkbare semantiek als 1G/1L maar bevat channeling-restricties die $x$- en $y$-variabelen koppelen.
• Block Encodings (X, Xa): Deze partitioneren het kleurbereik in blokken met een vaste breedte en gebruiken hulp-range-variabelen ($R_{u,a,b}$) om sommen van toewijzingsvariabelen binnen blokken te representeren.
  • X: Encodeert aftrekocties (vereist voor range-sommen binnen blokken) direct zonder hulpvariabelen.
  • Xa: Introduceert hulpvariabelen om aftrektermen te representeren, waardoor clausulehergebruik mogelijk is.
  • Block encodings beogen het aantal clausules voor afstandrestricties te verminderen, met name wanneer de randgewichten groot zijn.

2. Configureerbare Kenmerken

• Incrementeel Oplossen: Het framework test of het hergebruiken van geleerde clausules over iteraties heen (terwijl de bovengrens van de span afneemt) de prestaties verbetert. Dit is geïmplementeerd met behulp van SAT-aannames.
• Symmetriebreking: Een reflectiegebaseerde techniek wordt toegepast op de vertex met de hoogste graad, waarbij de kleur van deze vertex wordt beperkt tot de onderste helft van het span-bereik ($c(h) \le \lfloor k/2 \rfloor$). Dit maakt gebruik van de eigenschap dat als $c$ een geldige kleuring is, $c'(v) = k+1-c(v)$ ook geldig is.
• Blokbreedtestrategieën: Voor block encodings vergelijkt het framework fixed-width blokken (standaard $w=8$) met vary-width blokken (waarbij de breedte wordt bepaald door het maximale incident randgewicht van een vertex).

3. Experimentele Opzet

De studie evalueert 36 verschillende configuraties (combinaties van de 6 methoden en kenmerken) op 51 benchmark-instanties:

• GEOM Set: 33 geometrische random graphs (GEOM20 tot GEOM120).
• MS-CAP Set: 18 instanties afgeleid van cellulaire netwerkfrequentietoewijzingsproblemen.
• Solver: CaDiCaL 1.9.5 met een tijdlimiet van 3600 seconden per instantie.
• Baseline: Vergelijkingen worden gemaakt met de state-of-the-art SAT-encodings POP-S-B en POPH-S-B (Faber et al., 2024).

Belangrijkste Resultaten

Algemene Prestaties

Het voorgestelde framework bereikt state-of-the-art prestaties. De best presterende configuratie, Block Encoding Xa (met vaste breedte, incrementeel oplossen en symmetriebreking), loste alle 51 instanties op met een totale tijd van 2721,3 seconden. Dit vertegenwoordigt een reductie van 6,3% in totale tijd vergeleken met de vorige state-of-the-art POPH-S-B (2904,6s) en een reductie van 17,7% vergeleken met POP-S-B (3307,5s).

Prestaties bij Moeilijke Instanties (GEOM120b)

Een cruciale bevinding betreft de moeilijkste instantie, GEOM120b:

• Vorige methoden (POPH-S-B en POP-S-B) slaagden er niet in om GEOM120b tot bewezen optimaliteit op te lossen binnen de tijdlimiet van één uur.
• De voorgestelde Block Encodings (X en Xa) losten GEOM120b op tot optimaliteit in ongeveer 1000 seconden (specifiek loste de basis Xa-configuratie het op in 851,4s, en de volledig geoptimaliseerde Xa in 1011,6s).
• Dit demonstreert een versnellingsfactor van ongeveer 2x ten opzichte van de beste vorige SAT-gebaseerde benaderingen voor deze specifieke instantie.

Interactie-effecten

De studie onthult significante interactie-effecten tussen encodingkeuzes en solver-configuraties:

• Incrementeel Oplossen: Biedt substantiële versnellingen voor Block Encodings (bijv. 24,4% verbetering voor Xa) omdat de trappenstructuur van de blokken grotendeels stabiel blijft naarmate de span afneemt. Daarentegen biedt het geen voordeel (of zelfs een lichte degradatie) voor One-Variable Encodings (1G, 1L) omdat de ordeningsrestricties opnieuw worden gedefinieerd ten opzichte van de nieuwe bovengrens, wat geleerde clausules ongeldig maakt.
• Symmetriebreking: De effectiviteit is sterk afhankelijk van de encoding. Het verbetert de prestaties aanzienlijk voor POP-S-B (24,5% versnelling) en 1L (13,2% versnelling), maar verslechtert de prestaties voor 2G (11,9% vertraging) en POPH-S-B (11,4% vertraging).
• Blokbreedte: De keuze tussen vaste en variërende blokbreedtes had een minimale impact (<1,2% verschil) op de 50 standaard instanties, wat suggereert dat het leren van clausules door de solver goed adapteert aan beide strategieën.

Encoding Grootte vs. Efficiëntie

In tegenstelling tot de intuïtie dat minder variabelen en clausules sneller oplossen, behaalde de Xa encoding (die 7x meer variabelen en 5,5x meer clausules genereert dan de meest compacte 1G encoding) de snelste oplostijden. Dit ondersteunt het principe dat hulpvariabelen de unit propagation kunnen versterken, waardoor "shortcuts" ontstaan voor de solver om implicaties efficiënter af te leiden.

Betekenis en Claims

Het artikel claimt dat de systematische designstudie een gat in de literatuur vult met betrekking tot SAT-encodings voor het BCP. Hoewel symmetriebreking en incrementeel oplossen zijn bestudeerd voor GCP, was hun toepassing en interactie met BCP-specifieke encodings voorheen niet onderzocht.

De primaire bijdragen zijn:

1. Het Oplossen van het Onoplosbare: Het framework is de eerste die de GEOM120b benchmark tot bewezen optimaliteit heeft opgelost binnen een redelijke tijd, een taak die vorige exacte methoden niet binnen een uur konden voltooien.
2. Verenigd Framework: Het biedt een uitgebreide vergelijkende studie van zes encodingmethoden en hun configureerbare kenmerken, waarbij wordt vastgesteld dat Block Encodings superieur zijn voor de moeilijkste instanties, terwijl Order-Based Encodings (zoals 2L en 1G) een gunstige afweging bieden tussen implementatiecomplexiteit en prestaties voor algemene gevallen.
3. Inzicht in Interacties: Het werk benadrukt dat encodingkenmerken niet onafhankelijk opereren. Specifiek moeten incrementeel oplossen en symmetriebreking zorgvuldig worden gekozen op basis van het specifieke encodingtype, aangezien ze synergetische of antagonistische effecten kunnen hebben.

De auteurs concluderen dat hoewel block encodings de beste prestaties leveren op de meest uitdagende instanties, de systematische exploratie van encodingontwerpkeuzes essentieel is voor het verbeteren van exacte BCP-solvers. Toekomstig werk wordt gesuggereerd in het uitbreiden van het framework naar het Bandbreedte MultiColoring Problem (BMCP) en het ontwikkelen van adaptieve configuratie-selectiemechanismen.