通过SAT求解循环反带宽问题
Solving Cyclic Antibandwidth Problem by SAT
AI总结：
本文提出基于SAT求解的首个精确方法SAT-CAB，有效解决一般图上的循环反带宽问题，证明全局最优解并超越现有启发式方法。
摘要：
循环反带宽问题（CABP）是反带宽问题的一种变体，是一个NP难的图标记问题，具有广泛的应用。尽管已有大量研究，现有的最先进方法对于CABP大多是启发式或元启发式方法，精确方法仅限于受限的图类。在本文中，我们提出了一个基于SAT求解的首个精确方法，用于一般图上的CABP，称为SAT-CAB。该方法能够系统地探索解空间并保证全局最优性，克服了之前报告的启发式算法的局限性。该方法依赖于一种新颖且高效的SAT编码，将问题转换为一系列At-Most-One约束。特别地，我们引入了CABP固有的At-Most-One约束的紧凑表示，这显著减少了生成的公式大小，并使现代SAT求解器能够有效地探索解空间并证明全局最优性。在标准基准实例上的广泛计算实验表明，所提出的方法能够高效地解决具有实际意义的CABP实例，并识别出若干此前未知的最优解。此外，对于一些基准实例，首次证明了全局最优的循环反带宽值。比较结果表明，SAT-CAB在一般图上能够一致地匹配或超越由最先进启发式算法如MS-GVNS、HABC-CAB和MACAB以及强商业约束编程和混合整数编程求解器如CPLEX和Gurobi获得的最佳解，同时提供最优性保证。这些结果推动了CABP的前沿，并为一般图上的精确和混合方法提供了新的基准。
英文摘要：
The Cyclic Antibandwidth Problem (CABP), a variant of the Antibandwidth Problem, is an NP-hard graph labeling problem with numerous applications. Despite significant research efforts, existing state-of-the-art approaches for CABP are exclusively heuristic or metaheuristic in nature, and exact methods have been limited to restricted graph classes. In this paper, we present the first exact approach for the CABP on general graphs, based on SAT solving, called SAT-CAB. The proposed method is able to systematically explore the solution space and guarantee global optimality, overcoming the limitations of previously reported heuristic algorithms. This approach relies on a novel and efficient SAT encoding of CABP, in which the problem is transformed into a sequence of At-Most-One constraints. In particular, we introduce a compact representation of the At-Most-One constraints inherent to CABP, which significantly reduces the size of the resulting formulas and enables modern SAT solvers to effectively explore the solution space and to certify global optimality. Extensive computational experiments on standard benchmark instances show that the proposed method efficiently solves CABP instances of practical relevance, while identifying several previously unknown optimal solutions. Moreover, global optimal cyclic antibandwidth values are proven for a number of benchmark instances for the first time. Comparative results indicate that SAT-CAB consistently matches or surpasses the best-known solutions obtained by state-of-the-art heuristic algorithms such as MS-GVNS, HABC-CAB, and MACAB, as well as strong commercial Constraint Programming and Mixed Integer Programming solvers like CPLEX and Gurobi, particularly on general graphs, while also providing optimality guarantees. These results advance the state of the art for CABP and provide a new baseline for exact and hybrid methods on general graphs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
