SAT Encodings for Bandwidth Coloring: A Systematic Design Study

TL;DR

This paper systematically explores SAT encodings for the Bandwidth Coloring Problem, evaluating their impact and achieving state-of-the-art results on challenging benchmarks through a unified framework.

Contribution

It introduces a comprehensive framework with six SAT encoding methods for BCP and evaluates key features like symmetry breaking and incremental solving.

Findings

Block encodings solve the hardest GEOM120b instance to optimality.

Symmetry breaking significantly interacts with encoding choices.

The framework outperforms previous methods on benchmark instances.

Abstract

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.