Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SAT Encodings for Bandwidth Coloring: A Systematic Design Study

Duc Trung Kim Nguyen, Tuyen Van Kieu, Khanh Van To

TL;DR

This work conducts a systematic study of SAT encodings for the Bandwidth Coloring Problem (BCP), a generalization of graph coloring with distance constraints on edges. It proposes a unified framework featuring six encodings (1G, 1L, 2G, 2L, X, Xa) across one-, two-, and block-variable categories, and examines solver features such as incremental solving, symmetry breaking, and block-width strategies. The empirical results on GEOM and MS-CAP benchmarks show state-of-the-art performance, with block encodings Xa solving the hardest instance GEOM120b to proven optimality in roughly $1000$ seconds, and general improvements across many instances by careful combination of encoding choices. The findings reveal strong interaction effects between encoding type and solver configuration, with incremental solving benefiting block encodings significantly while sometimes hurting simpler encodings, and symmetry breaking providing encoding-dependent gains. Overall, the study demonstrates the practical advantage of block-based SAT encodings for exact BCP solving and offers guidance for adaptive encoding design in future work.

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.

SAT Encodings for Bandwidth Coloring: A Systematic Design Study

TL;DR

This work conducts a systematic study of SAT encodings for the Bandwidth Coloring Problem (BCP), a generalization of graph coloring with distance constraints on edges. It proposes a unified framework featuring six encodings (1G, 1L, 2G, 2L, X, Xa) across one-, two-, and block-variable categories, and examines solver features such as incremental solving, symmetry breaking, and block-width strategies. The empirical results on GEOM and MS-CAP benchmarks show state-of-the-art performance, with block encodings Xa solving the hardest instance GEOM120b to proven optimality in roughly seconds, and general improvements across many instances by careful combination of encoding choices. The findings reveal strong interaction effects between encoding type and solver configuration, with incremental solving benefiting block encodings significantly while sometimes hurting simpler encodings, and symmetry breaking providing encoding-dependent gains. Overall, the study demonstrates the practical advantage of block-based SAT encodings for exact BCP solving and offers guidance for adaptive encoding design in future work.

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.
Paper Structure (39 sections, 3 theorems, 10 equations, 8 figures, 5 tables, 2 algorithms)

This paper contains 39 sections, 3 theorems, 10 equations, 8 figures, 5 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Problem Definition
  3. Graph Coloring Problem
  4. Bandwidth Coloring Problem
  5. Literature Review
  6. Metaheuristic Approaches
  7. Integer and Constraint Programming
  8. SAT-based Approaches
  9. Research Gaps
  10. SAT Encoding Framework
  11. Framework Overview
  12. Upper Bound Computation
  13. One-Variable Encodings
  14. Greater-than Encoding (1G)
  15. Less-than Encoding (1L)
  16. ...and 24 more sections

Key Result

Proposition 4.1

Let $n=|V|$, $m=|E|$, $k$ be the span, and $\bar{d}$ be the average edge weight. Table table:encoding-size compares the asymptotic size of the proposed encodings with those from faber2024. The proposed 1G and 1L encodings have the same asymptotic complexity as POP-S-B, while 2G and 2L match POPH-S-B (with a constant factor increase due to channeling constraints). All order-based encodings have cl

Figures (8)

  • Figure 1: Example of the Bandwidth Coloring Problem.
  • Figure 2: Staircase block structure for a vertex $u$ with block width $w=8$. The backward chain (top-left) builds ranges starting from $x_{u,1}$ and extending toward the block boundary. The bidirectional chains (middle) support both directions for inter-block ranges. The forward chain (bottom-right) builds ranges ending at the block boundary.
  • Figure 3: Cumulative success curves showing instances solved as a function of time limit. Xa$^*$ = Xa (fixed, $x$, Sym.); X$^*$ = X (vary, $x$, Sym.); Xa = Xa (fixed, no Inc., no Sym.).
  • Figure 4: Solving time for each configuration on the ten hardest instances. Xa$^*$ = Xa (fixed, $x$, Sym.); 2L$^*$ = 2L (Sym.); 1G$^*$ = 1G (Sym.).
  • Figure 5: GEOM120b solving time and cumulative time for the ten hardest instances. Xa$^*$ = Xa (fixed, $x$, Sym.); X$^*$ = X (vary, $x$, Sym.); Xa = Xa (fixed, no Inc., no Sym.); 2L$^*$ = 2L (Sym.); 1G$^*$ = 1G (Sym.).
  • ...and 3 more figures

Theorems & Definitions (7)

  • Definition 2.1: Graph Coloring Problem
  • Definition 2.2: Bandwidth Coloring Problem
  • Proposition 4.1: Encoding Size Comparison
  • Theorem A.1: Correctness of Order-Based Encodings
  • proof
  • Proposition B.1: Symmetry Breaking Validity
  • proof