Solving Cyclic Antibandwidth Problem by SAT
Hieu Truong Xuan, Khanh To Van
TL;DR
This work addresses the Cyclic Antibandwidth Problem (CABP) on general graphs, introducing SAT-CAB, the first exact SAT-based solver capable of proving global optimality. The key idea is to encode CABP via overlapping At-Most-One constraints organized into a novel Cyclic Ladder structure, enabling compact SAT formulations and efficient solving. The approach combines an ILP-inspired formulation, iterative (and parallel) SAT solving, symmetry breaking, and a specialized encoding that significantly reduces formula size compared to direct AMO encodings. Empirical results on diverse graphs (including Harwell-Boeing and random connected graphs) show SAT-CAB achieving best-known CAB values and proving optimality for many instances, while also discovering new bounds; limitations include memory demands and scalability, pointing to future work in further compression and hybridization. Overall, the work closes a gap between heuristic CABP methods and exact optimization, establishing SAT-based exactness as a viable baseline for cyclic graph labeling problems with general graph structures.
Abstract
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.