AI 中文总结
研究无线电k标签问题，提出基于SAT的精确框架，结合紧凑顺序编码与增量SAT求解，重用学习子句避免重复公式重建。实验表明该方法表现优异，建立多个新最佳已知无线电数，优于现有求解器和启发式方法，还验证了许多实例的最优解。
AI 中文摘要
无线电k标签（或k着色）问题旨在为连通图G的顶点找到非负整数标签的最小跨度分配，使得所有顶点对满足|f(u)-f(v)|≥k+1-d(u,v)。尽管已有许多理论构造和启发式算法，但现有方法通常无法为广泛的图类提供经过验证的最优解。本文提出了一种基于SAT的精确框架，将紧凑顺序编码与增量SAT求解相结合。该框架在重用SAT调用中的学习子句时逐步收紧可接受跨度，避免重复公式重建。在九个图族的146个基准实例上的实验结果表明，该方法建立了38个新的最佳已知无线电数，在146个基准实例中的130个上匹配或改进了最佳已知无线电数。该SAT框架在整体解决方案质量方面优于包括CPLEX和Gurobi在内的现有商业优化求解器，并大幅改进了先前发布的启发式方法。此外，通过将SAT框架与CPLEX和Gurobi求解的ILP模型相结合，该研究为146个基准实例中的109个验证了最优解，大大扩展了具有已证明最优性的无线电标签基准集。这些结果证明了增量SAT求解作为解决困难图标签问题的实用精确优化框架的有效性。
英文摘要
The radio $k$-labeling (or $k$-coloring) problem seeks a minimum-span assignment of nonnegative integer labels to the vertices of a connected graph $G$ such that $ |f(u)-f(v)| \ge k+1-d(u,v) $ for all vertex pairs. Although numerous theoretical constructions and some heuristic algorithms have been proposed, existing approaches generally fail to provide certified optimal solutions for broad graph classes. This paper presents an exact SAT-based framework for radio k-labeling that combines a compact order encoding with incremental SAT solving. The proposed framework incrementally tightens the admissible span while reusing learned clauses across SAT calls, avoiding repeated formula reconstruction. Experimental results on 146 benchmark instances from nine graph families demonstrate that the proposed approach establishes 38 new best-known radio numbers while matching or improving the best-known radio numbers on 130 of the 146 benchmark instances. The proposed SAT framework outperforms state-of-the-art commercial optimization solvers, including CPLEX and Gurobi, in terms of overall solution quality, and substantially improves upon previously published heuristic methods. Furthermore, by combining the SAT frameworks with ILP models solved by CPLEX and Gurobi, the study certifies optimal solutions for 109 of the 146 benchmark instances, substantially expanding the set of radio-labeling benchmarks with proven optimality. These results demonstrate the effectiveness of incremental SAT solving as a practical exact optimization framework for difficult graph-labeling problems.
CommentsPreprint, 14 tables (6 in main text, 8 in Appendix), 9 figures, 1 algorithm. Submitted to Wireless Networks (Springer Nature)
