SAT Encodings for Bandwidth Coloring: A Systematic Design Study
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866915785935421440 |
|---|---|
| author | Nguyen, Duc Trung Kim Van Kieu, Tuyen Van To, Khanh |
| author_facet | Nguyen, Duc Trung Kim Van Kieu, Tuyen Van To, Khanh |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_08423 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | SAT Encodings for Bandwidth Coloring: A Systematic Design Study Nguyen, Duc Trung Kim Van Kieu, Tuyen Van To, Khanh Logic in Computer Science 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. |
| title | SAT Encodings for Bandwidth Coloring: A Systematic Design Study |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2602.08423 |