The Bandwidth Coloring Problem (BCP) generalizes graph coloring by enforcing minimum separation constraints between adjacent vertices and arises in frequency assignment applications. While SAT-based approaches have shown promise for exact BCP solving, the encoding design space remains largely unexplored. This paper presents a systematic study of SAT encodings for the BCP, proposing a unified framework with six encoding methods across three categories: one-variable, two-variable, and block encodings. We evaluate the impact of key features including incremental solving and symmetry breaking. While symmetry breaking has been studied for graph coloring, it has not been systematically evaluated for SAT-based BCP solvers. Our analysis reveals significant interaction effects between encoding choices and solver configurations. The proposed framework achieves state-of-the-art performance on GEOM and MS-CAP benchmarks. Block encodings solve GEOM120b, the hardest instance, to proven optimality in approximately 1000 seconds, whereas previous methods could not solve it within a one-hour time limit.

翻译：带宽着色问题（BCP）通过强制相邻顶点间的最小间隔约束推广了图着色问题，并出现于频率分配应用中。虽然基于SAT的方法在精确求解BCP方面展现出潜力，但其编码设计空间仍存在大量未探索领域。本文系统研究了BCP的SAT编码，提出了一个包含三类六种编码方法的统一框架：单变量编码、双变量编码与块编码。我们评估了增量求解与对称性破缺等关键特性的影响。尽管对称性破缺在图着色领域已有研究，但尚未在基于SAT的BCP求解器中得到系统评估。我们的分析揭示了编码选择与求解器配置间显著的交互效应。所提框架在GEOM和MS-CAP基准测试中达到了最先进性能。块编码在约1000秒内将最困难算例GEOM120b求解至可证明的最优解，而先前方法在一小时时限内无法求解该算例。