A SAT-Based Exact Approach for Radio k-Labeling

Technisches Resümee: Ein SAT-basierter exakter Ansatz für die Radio-$k$-Labeling

Problemdefinition
Die vorliegende Arbeit befasst sich mit dem Radio-$k$-Labeling-Problem (auch bekannt als Radio-$k$-Färbung), einem kombinatorischen Optimierungsproblem, das aus dem Kanalzuweisungsproblem abgeleitet ist. Gegeben sei ein zusammenhängender Graph $G=(V, E)$ mit dem Durchmesser $k = \text{diam}(G)$. Das Ziel besteht darin, den Knoten nichtnegative ganzzahlige Labels $f(v)$ zuzuweisen, sodass für jedes Paar distinkter Knoten $u, v$ die Bedingung $|f(u) - f(v)| \ge k + 1 - d(u, v)$ gilt, wobei $d(u, v)$ die kürzeste Pfadentfernung ist. Das Ziel ist es, die Spanne der Labelung zu minimieren, definiert als $\max_{v \in V} f(v)$. Die minimal mögliche Spanne wird als Radio-Zahl bezeichnet und mit $rn(G)$ notiert.

Obwohl theoretische Konstruktionen für spezifische Graphfamilien (z. B. Pfade, Zyklen, Bäume) existieren und heuristische Algorithmen zulässige Lösungen für allgemeine Graphen liefern, sind exakte Lösungen für breite Graphklassen rar gesät. Bestehende Modelle der ganzzahligen linearen Programmierung (ILP) leiden unter Skalierbarkeitsproblemen aufgrund des rasanten Wachstums des Suchraums und des Mangels an Informationswiederverwendung zwischen den Optimierungsiterationen.

Methodik
Die Autoren schlagen einen exakten, inkrementellen SAT-basierten Rahmen vor, der eine kompakte Ordnungs-Kodierung (Order Encoding) mit einer iterativen Optimierungsstrategie kombiniert.

1. SAT-Kodierungen:
   Die Arbeit entwickelt zwei Boolesche Erfüllbarkeits-Kodierungen (SAT-Kodierungen) basierend auf dem Label-Bereich $\{1, \dots, UB\}$, wobei $UB$ eine vorab berechnete obere Schranke ist:

   • Direkte Kodierung (Direct Encoding): Verwendet Zuweisungsvariablen $x_{v,l}$ (wahr, wenn Knoten $v$ das Label $l$ besitzt). Sie erzwingt Constraints über paarweise Konfliktklauseln. Obwohl sie logisch äquivalent zum ILP-Modell ist, erfordert sie $O(n^2 UB k)$ Klauseln für die Radio-Constraints, was zu einer schwachen Propagation unter Unit Resolution führt.
   • Ordnungs-Kodierung (Order Encoding): Führt neben den Zuweisungsvariablen Schwellenwertvariablen $g_{v,l}$ (wahr, wenn $f(v) \ge l$) ein. Diese Kodierung stellt den Radio-Constraint $|f(u) - f(v)| \ge \Delta_{uv}$ kompakter dar. Sie reduziert die Anzahl der Radio-Constraint-Klauseln von $O(n^2 UB k)$ auf $O(n^2 UB)$, indem die Abhängigkeit von $k$ in der Klauselanzahl eliminiert wird. Die Ordnungs-Kodierung ermöglicht zudem eine stärkere Propagation, da Ungleichungen wie $f(v) \ge c$ auf einzelne Literale abgebildet werden.

2. Inkrementale Lösestrategie:
   Das Framework nutzt ein inkrementelles SAT-Solving-Paradigma. Anstatt die Formel für jede Iteration neu aufzubauen, wird eine einzige Solver-Instanz einmalig erstellt. Der Algorithmus verläuft wie folgt:

   • Phase 1: Berechnung aller Paardistanzen und Festlegung von $k = \text{diam}(G)$.
   • Phase 2: Aufbau des SAT-Modells mit einer initialen oberen Schranke $UB$.
   • Phase 3: Iteratives Lösen der Formel. Wenn eine erfüllbare Zuweisung mit der Spanne $\beta$ gefunden wird, wird der Solver angewiesen, jede Spanne $\ge \beta$ zu verbieten (Verengung der Schranke) und erneut zu lösen. Entscheidend ist, dass gelernte Klauseln (learned clauses) aus vorherigen Iterationen erhalten bleiben, wodurch redundante Sucharbeit vermieden wird. Die Schleife terminiert, wenn der Solver UNSAT zurückgibt (was die Optimalität zertifiziert) oder ein Zeitlimit erreicht ist.

3. Symmetriebrechung (Symmetry Breaking):
   Für Zyklusgraphen ($C_n$), die eine Rotationssymmetrie aufweisen, führen die Autoren eine Symmetriebrechung durch, die das Label des ersten Knotens auf 1 fixiert ($f(0)=1$). Dies reduziert den Suchraum und beschleunigt den Nachweis der Optimalität erheblich, ohne optimale Lösungen zu verwerfen.

Wesentliche Beiträge

• Neuartiges Framework: Das erste allgemeine exakte SAT-basierte Optimierungs-Framework für das Radio-$k$-Labeling-Problem, welches Ordnungs-Kodierung und inkrementelles Lösen nutzt.
• Effizienzsteigerungen: Die Ordnungs-Kodierung reduziert die Klauselkomplexität und verbessert die Propagation im Vergleich zur direkten Kodierung. Der inkrementelle Ansatz nutzt gelernte Klauseln wieder, was den Rechenaufwand im Vergleich zu unabhängigen SAT-Aufrufen oder Standard-ILP-Ansätzen, die vorherige Suchinformationen verwerfen, signifikant reduziert.
• Symmetrie-Handhabung: Die Einführung spezifischer Symmetriebrechung-Constraints für Zyklusgraphen demonstriert erhebliche Beschleunigungen bei den Lösungszeiten und eine höhere Anzahl zertifizierter Optima.

Experimentelle Ergebnisse
Das Framework wurde an 146 Benchmark-Instanzen aus neun Graphfamilien (Pfade, Zyklen, dreieckige Schlangen, $kC_m$-Schlangen, Leitern, Bücher, Freundschaftsgraphen und Binomialbäume) mit einem Zeitlimit von 1.200 Sekunden evaluiert.

• Performance vs. Heuristiken: Die vorgeschlagene Order-SAT-Methode etablierte 38 neue beste bekannte Radio-Zahlen unter den 98 Instanzen, für die kein geschlossene Form für das Optimum bekannt war. Sie lieferte konsistent engere zulässige Schranken als bestehende Heuristiken (Ub1, Ub3) und die direkte Kodierung.
• Performance vs. ILP:
  • Graphen mit wachsendem Durchmesser: Bei Familien, in denen der Durchmesser mit der Größe wächst (z. B. Schlangen, Leitern, Binomialbäume), übertraf Order-SAT kommerzielle ILP-Solver (CPLEX, Gurob) sowohl in der Lösungsqualität (engere Schranken) als auch in der Anzahl der zertifizierten Optima. ILP-Solver erschöpften auf diesen Instanzen oft den Speicher oder lieferten lose Incumbents zurück.
  • Graphen mit beschränktem Durchmesser: Für Familien mit konstantem Durchmesser (z. B. Buch-Graphen, Freundschaftsgraphen) waren ILP-Solver effektiver und zertifizierten die Optimalität für alle Instanzen schnell.
• Kombinierter Ansatz: Durch die Kombination des SAT-Frameworks mit ILP-Modellen konnte die Studie die optimalen Lösungen für 109 der 146 Instanzen zertifizieren, womit sie die Menge der Radio-Labeling-Benchmarks mit bewiesener Optimalität erheblich erweitert hat.
• Statistische Signifikanz: Ein Friedman-Test bestätigte, dass Order-SAT das beste Gesamtranking (Mittelwert-Rang 2,58) unter allen verglichenen Methoden, einschließlich kommerzieller Solver und Heuristiken, erreichte.

Bedeutung
Die Arbeit behauptet, dass inkrementelles SAT-Solving ein praktisches exaktes Optimierungsparadigma für Graph-Labeling-Probleme darstellt, die traditionell von theoretischen Konstruktionen und heuristischen Algorithmen dominiert wurden. Die Arbeit zeigt auf:

1. Moderne SAT-Solver können, wenn sie mit kompakten Kodierungen und inkrementellen Strategien kombiniert werden, schwierige kombinatorische Optimierungsprobleme lösen, bei denen traditionelle ILP-Formulierungen unter Skalierbarkeitsproblemen leiden.
2. Der vorgeschlagene Ansatz ist komplementär zu ILP; er ist überlegen für Graphen mit wachsenden Durchmessern, während ILP für Graphen mit beschränktem Durchmesser weiterhin bevorzugt wird.
3. Das Framework schließt erfolgreich die Lücke zwischen theoretischen Schranken und zertifizierten exakten Lösungen und bietet ein robustes Werkzeug zur Bestimmung von Radio-Zahlen in komplexen Graphstrukturen.

Die Autoren kommen zu dem Schluss, dass dieser Ansatz eine hochgradig wettbewerbsfähige Alternative zu kommerziellen Solvern für spezifische Graphklassen darstellt und das Potenzial von inkrementellem SAT-Solving für andere Graph-Labeling- und kombinatorische Optimierungsprobleme hervorhebt.