A SAT-Based Exact Approach for Radio k-Labeling

Technical Summary: A SAT-Based Exact Approach for Radio k-Labeling

Problem Definition
The paper addresses the radio $k$-labeling problem (also known as radio $k$-coloring), a combinatorial optimization problem derived from the channel assignment problem. Given a connected graph $G=(V, E)$ with diameter $k = \text{diam}(G)$, the objective is to assign non-negative integer labels $f(v)$ to vertices such that for every pair of distinct vertices $u, v$, the condition $|f(u) - f(v)| \ge k + 1 - d(u, v)$ holds, where $d(u, v)$ is the shortest path distance. The goal is to minimize the span of the labeling, defined as $\max_{v \in V} f(v)$. The minimum possible span is the radio number, denoted $rn(G)$.

While theoretical constructions exist for specific graph families (e.g., paths, cycles, trees) and heuristic algorithms provide feasible solutions for general graphs, exact solutions for broad graph classes remain scarce. Existing Integer Linear Programming (ILP) formulations suffer from scalability issues due to the rapid growth of the search space and the lack of information reuse between optimization iterations.

Methodology
The authors propose an exact, incremental SAT-based framework that combines a compact order encoding with an iterative optimization strategy.

1. SAT Encodings:
   The paper develops two Boolean satisfiability (SAT) encodings based on the label domain $\{1, \dots, UB\}$, where $UB$ is a precomputed upper bound:

   • Direct Encoding: Uses assignment variables $x_{v,l}$ (true if vertex $v$ has label $l$). It enforces constraints via pairwise conflict clauses. While logically equivalent to the ILP model, it requires $O(n^2 UB k)$ clauses for radio constraints, leading to weak propagation under unit resolution.
   • Order Encoding: Introduces threshold variables $g_{v,l}$ (true if $f(v) \ge l$) alongside the assignment variables. This encoding represents the radio constraint $|f(u) - f(v)| \ge \Delta_{uv}$ more compactly. It reduces the number of radio constraint clauses from $O(n^2 UB k)$ to $O(n^2 UB)$ by eliminating the dependence on $k$ in the clause count. The order encoding also enables stronger propagation, as inequalities like $f(v) \ge c$ map to single literals.

2. Incremental Solving Strategy:
   The framework employs an incremental SAT solving paradigm. Instead of rebuilding the formula for each iteration, a single solver instance is constructed once. The algorithm proceeds as follows:

   • Phase 1: Compute all-pairs distances and set $k = \text{diam}(G)$.
   • Phase 2: Build the SAT model with an initial upper bound $UB$.
   • Phase 3: Iteratively solve the formula. If a satisfying assignment is found with span $\beta$, the solver is instructed to forbid any span $\ge \beta$ (tightening the bound) and re-solve. Crucially, learned clauses from previous iterations are preserved, avoiding redundant search effort. The loop terminates when the solver returns UNSAT (certifying optimality) or a time limit is reached.

3. Symmetry Breaking:
   For cycle graphs ($C_n$), which exhibit rotational symmetry, the authors introduce a symmetry-breaking constraint fixing the label of the first vertex to 1 ($f(0)=1$). This reduces the search space and significantly accelerates the proof of optimality without discarding optimal solutions.

Key Contributions

• Novel Framework: The first general exact SAT-based optimization framework for the radio $k$-labeling problem, utilizing order encoding and incremental solving.
• Efficiency Improvements: The order encoding reduces clause complexity and improves propagation compared to direct encoding. The incremental approach reuses learned clauses, significantly reducing computational overhead compared to independent SAT calls or standard ILP approaches that discard previous search information.
• Symmetry Handling: The introduction of specific symmetry-breaking constraints for cycle graphs, demonstrating substantial speedups in solving times and increased numbers of certified optima.

Experimental Results
The framework was evaluated on 146 benchmark instances across nine graph families (paths, cycles, triangular snakes, $kC_m$-snakes, ladders, books, friendship graphs, and binomial trees) with a time limit of 1,200 seconds.

• Performance vs. Heuristics: The proposed Order-SAT method established 38 new best-known radio numbers among the 98 instances without a known closed-form optimum. It consistently produced tighter feasible bounds than existing heuristics (Ub1, Ub3) and direct-encoding SAT.
• Performance vs. ILP:
  • Growing-Diameter Graphs: For families where diameter grows with size (e.g., snakes, ladders, binomial trees), Order-SAT outperformed commercial ILP solvers (CPLEX, Gurobi) in both solution quality (tighter bounds) and the number of certified optima. ILP solvers often exhausted memory or returned loose incumbents on these instances.
  • Bounded-Diameter Graphs: For families with constant diameter (e.g., book graphs, friendship graphs), ILP solvers were more effective, certifying optimality for all instances quickly.
• Combined Approach: By combining the SAT framework with ILP models, the study certified optimal solutions for 109 of the 146 instances, substantially expanding the set of radio-labeling benchmarks with proven optimality.
• Statistical Significance: A Friedman test confirmed that Order-SAT achieved the best overall ranking (mean rank 2.58) among all compared methods, including commercial solvers and heuristics.

Significance
The paper claims that incremental SAT solving constitutes a practical exact optimization paradigm for graph labeling problems that have traditionally been dominated by theoretical constructions and heuristic algorithms. The work demonstrates that:

1. Modern SAT solvers, when combined with compact encodings and incremental strategies, can solve difficult combinatorial optimization problems where traditional ILP formulations struggle with scalability.
2. The proposed approach is complementary to ILP; it is superior for graphs with growing diameters, while ILP remains preferable for bounded-diameter graphs.
3. The framework successfully bridges the gap between theoretical bounds and certified exact solutions, providing a robust tool for determining radio numbers in complex graph structures.

The authors conclude that this approach offers a highly competitive alternative to commercial solvers for specific graph classes and highlights the potential of incremental SAT solving for other graph labeling and combinatorial optimization problems.