带宽着色的SAT编码：一种系统设计研究
SAT Encodings for Bandwidth Coloring: A Systematic Design Study
AI总结：
本文提出了一种统一框架，通过系统研究SAT编码方法，改进了带宽着色问题的求解性能，特别是在处理最难实例时实现了最优解。
摘要：
带宽着色问题（BCP）通过在相邻顶点之间施加最小分离约束来扩展图着色问题，出现在频率分配应用中。虽然基于SAT的方法在精确求解BCP方面显示出前景，但编码设计空间仍 largely 未被探索。本文提出了对BCP的SAT编码的系统研究，提出了一种统一框架，包含六个编码方法，分为三类：一变量、二变量和块编码。我们评估了关键特征的影响，包括增量求解和对称性打破。尽管对称性打破已在图着色中被研究，但尚未系统评估用于基于SAT的BCP求解器。我们的分析揭示了编码选择与求解器配置之间显著的交互效应。所提出的框架在GEOM和MS-CAP基准上实现了最先进的性能。块编码在GEOM120b实例上以约1000秒的时间证明最优解，而先前的方法在1小时内无法解决。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
