AI 中文总结
针对带宽多着色问题，提出基于SAT的精确框架，通过高效编码结合颜色域缩减和增量求解策略，显著修剪搜索空间，实验证明该框架比之前方法有改进，能证明更多实例最优性，扩大可证明最优性的基准实例范围。
AI 中文摘要
带宽多着色问题（BMCP）是带宽着色问题（BCP）的NP难扩展，在电信、资源分配和调度中有重要应用。现有元启发式算法不能证明全局最优性，基于约束编程（CP）和整数编程（IP）的精确方法计算量大且解质量不如元启发式算法。本文提出首个基于SAT的BMCP精确框架，主要贡献是高效的SAT编码，结合颜色域缩减和增量SAT求解策略，显著修剪搜索空间。实验结果表明该框架比之前的精确方法有显著改进，能证明更多实例的最优性，扩大了可证明最优性的基准实例范围。
英文摘要
The Bandwidth Multicoloring Problem (BMCP) is an NP-hard extension of the Bandwidth Coloring Problem (BCP) with important applications in telecommunications, resource allocation, and scheduling. While state-of-the-art metaheuristics can efficiently produce high-quality solutions, they cannot certify global optimality. Existing exact approaches based on Constraint Programming (CP) and Integer Programming (IP) provide such guarantees but typically require extensive computation and still lag behind metaheuristics in solution quality, leaving many benchmark instances without optimality certificates. In this paper, we present the first SAT-based exact framework for the BMCP. Our main contribution is an efficient SAT encoding that compactly models both intra-vertex and inter-vertex color distance constraints. Combined with tight color domain reduction and an incremental SAT-solving strategy, the proposed formulation significantly prunes the search space and enables efficient exact optimization. Experimental results on the GEOM and MS-CAP benchmark suites demonstrate substantial improvements over previous exact approaches. On the challenging GEOM benchmark, the proposed framework proves optimality for more instances within only one hour of computation than the previous CP/IP approach, which required a 48-hour time limit, while also verifying the optimality of several previously reported best-known solutions. These results demonstrate that SAT-based reasoning provides an effective exact optimization framework for the BMCP and substantially expands the range of benchmark instances whose optimality can be certified.
