1 Introduction↩︎

The Bandwidth Coloring Problem (BCP) is a combinatorial optimization problem that extends the classical graph coloring problem (GCP), with numerous practical applications in areas such as scheduling, resource allocation, and network design. The problem can be formally defined as follows: given an edge-weighted undirected graph \(G = (V,E)\), a weight function \(d: E \to \mathbb{Z}^+\) assigns a positive integer weight to each edge \(e = \{u,v\} \in E\). The objective of the BCP is to find a coloring \(c: V \to \mathbb{N}\) such that \(\forall e = \{u,v\} \in E: |c(u) - c(v)| \geq d(\{u,v\})\), while minimizing the span value, defined as \(k = \max_{v \in V} c(v)\).

The Bandwidth Multicoloring Problem (BMCP) generalizes the BCP by allowing each vertex to be assigned multiple colors. Formally, let \(G = (V,E)\) be an undirected graph equipped with two weight functions: a vertex weight function \(w: V \to \mathbb{Z}^+\) specifying the number of colors required for each vertex, and an edge weight function \(d: E \to \mathbb{Z}^+\) defining the minimum color separation between adjacent vertices. The objective of the BMCP is to find a multicoloring assignment \(c: V \rightarrow \mathcal{P}(\mathbb{Z}^+)\) that minimizes the span value \(k = \max_{u \in V, m\in c(u)} m\) while satisfying the following conditions: first, each vertex \(u \in V\) is assigned exactly \(w(u)\) distinct colors; second, any two distinct colors \(m, n \in c(u)\) assigned to the same vertex must satisfy \(|m - n| \geq d(\{u,u\})\); and finally, for any edge \(e = \{u,v\} \in E\), every color \(m \in c(u)\) and \(n \in c(v)\) must satisfy \(|m - n| \geq d(\{u,v\})\).

Both the BCP and the BMCP arise naturally from frequency assignment problems (FAP) [1] in the field of telecommunications, where the graph’s vertices represent radio transmitters and the edge weights dictate the minimum frequency separations required to avoid electromagnetic interference [2]. Because both models are generalizations of the classical graph coloring problem, they are strongly NP-hard [3]. Consequently, a vast amount of literature has been dedicated to metaheuristic approaches to find high-quality approximations, including iterated tabu search [4], learning-based hybrid search [5], path relinking [6], and variable neighborhood search [7]. While these methods perform well on large-scale instances, optimality matters profoundly in combinatorial optimization. Establishing mathematically proven optimal solutions is not merely a theoretical exercise; it is a necessity for benchmark certification and for reliably validating heuristic results. Furthermore, providing exact lower bounds is crucial for supporting future algorithm development. The critical importance of exact methods is perhaps best highlighted by their ability to identify incorrect published solutions, as demonstrated when exact approaches successfully proved that a previously published heuristic solution for the BMCP [8] was mathematically flawed [9].

Despite this pressing need for provable optimality, existing exact methods for the BMCP have essentially stagnated since 2021. The current state-of-the-art exact solvers rely heavily on Constraint Programming (CP) and Integer Programming (IP) models introduced by Dias et al. [9], [10]. While these models can handle small-scale instances, they suffer from exponential computational complexity and fail to scale effectively. Conversely, the adjacent field of the BCP has recently experienced a major breakthrough. Boolean Satisfiability (SAT)-based methods have dramatically changed the state-of-the-art for the BCP [11], [12]. Most notably, Faber et al. [13] introduced partial-ordering-based SAT encodings (POP-S-B and POPH-S-B) that successfully identified optimal solutions for 32 out of 33 instances in the challenging GEOM dataset [14]. Surprisingly, despite the massive success of SAT solving in the BCP, the BMCP has never benefited from SAT methodologies. Extending these formulations to the BMCP is highly non-trivial. Naive adaptations, such as transforming the BMCP into a BCP via vertex splitting, inevitably lead to an unmanageable explosion in the number of variables and clauses, severely crippling solver efficiency.

This paper fills that methodological gap by proposing the first dedicated SAT-based framework designed natively for the complex combinatorial structure of the BMCP. The primary contributions of this work are summarized as follows. First, we introduce the very first SAT-based framework for the BMCP, completely bypassing the inefficiencies of vertex decomposition. As our primary contribution, we propose a novel Order-Based Encoding (OBE) that natively captures the problem’s complex combinatorial structure. Second, our proposed methodology significantly improves upon the state-of-the-art in exact solving, decisively outperforming existing CP and IP formulations. Third, by leveraging this encoding, we successfully prove optimality for several previously open instances within the benchmark datasets. Finally, and most importantly, our SAT formulation achieves these unprecedented exact solutions under a much smaller computational budget than what was previously required by the existing exact models, underscoring the exceptional efficiency and scalability of our approach.

The remainder of this paper is organized as follows. Section 2 reviews related work on metaheuristic and exact approaches for the BMCP. Section 3 presents the proposed SAT-based approach, describing the encoding method. Section 4 reports computational experiments on the GEOM and MS-CAP benchmark instances. Finally, Section 5 summarizes the findings and discusses directions for future research.

2 Related work↩︎

The Bandwidth Coloring Problem and its generalization, the Bandwidth Multicoloring Problem, model resource allocation scenarios where interacting elements must be separated by predefined distances. While the BCP assigns a single color to each vertex such that adjacent vertices respect specific edge-weight separations, the BMCP introduces the additional complexity of demanding multiple colors per vertex, governed by internal vertex separation constraints. Because these problems are NP-hard, the pursuit of optimal or near-optimal solutions has motivated a rich body of literature. Existing methodologies can be broadly categorized into heuristic or metaheuristic techniques, which prioritize computational speed for large instances, and exact methods, which are mathematically designed to guarantee solution optimality. Table ¿tbl:tab:previous-work? provides an overview of existing studies, including their key contributions, the problems addressed, and the availability of optimality guarantees for the BCP and the BMCP.

width=

Metaheuristic algorithms have been extensively applied to both the BCP and the BMCP, primarily due to their ability to efficiently generate high-quality solutions. To tackle the BMCP using these methods, the problem is typically reduced to a standard BCP by decomposing each vertex into a clique, where the clique size corresponds to the vertex’s color demand, and internal edge weights equal the vertex’s minimum separation distance. Several prominent frameworks have been successfully adapted for these problems. These include the Multistart Iterated Tabu Search (MITS) [4], which leverages fast incremental evaluation to streamline objective function updates; Learning-based Hybrid Search (LHS) [15], which combines forward-checking construction with adaptive tabu search repair; path relinking strategies [6], which maintain a balance between search intensification and diversification; and Variable Neighborhood Search (VNS) [7], which structures local search around conflict metrics and edge weights.

Despite their computational speed and scalability, these metaheuristic approaches possess inherent limitations, most notably their fundamental inability to guarantee global optimality. As previously established, proving optimality is not merely a theoretical exercise but a critical necessity for advancing the field. Exact mathematical guarantees are indispensable for rigorously certifying benchmarks, reliably validating the outputs of heuristic algorithms, and providing exact lower bounds that support future algorithmic development. Moreover, such rigor is uniquely capable of identifying and correcting erroneously published solutions. In real-world applications such as telecommunications frequency assignment, the absence of these exact guarantees can have severe practical consequences; relying on heuristic algorithms, which are prone to stagnating in local optima and heavily dependent on extensive parameter tuning, often yields suboptimal allocations, ultimately leading to costly spectrum waste and signal interference.

To address the need for mathematical guarantees, exact formulations for the BMCP have been explored through the lens of Constraint Programming and Integer Programming. Dias et al. [9], [10] proposed both CP and IP models designed to find provably optimal solutions. In their CP model, they utilize integer variables \(x(i,k)\) to represent the \(k\)-th color assigned to vertex \(i\) (\(1 \leq k \leq w(i)\)). This is supported by a global constraint, allMinDistance, which ensures that the minimum distance between any two colors assigned to the same vertex is at least the vertex’s minimum separation distance. The CP formulation is given by: \[\begin{align} \text{Minimize} \quad & \max_{\substack{i \in V \\ 1 \le k \le w(i)}} x(i,k) \\ \text{Subject to} \quad & |x(i,k)-x(j,m)| \ge d(\{i,j\}) && \forall \{i,j\}\in E, \\ & && 1 \le k \le w(i) \notag \\ & && 1 \le m \le w(j) \notag \\ & \text{allMinDistance}\!\left( \{x(i,k):1\le k\le w(i)\}, d(\{i,i\}) \right) && \forall i\in V \\ & x(i,k)\in\mathbb{Z}^{+} && \forall i\in V, \\ & && 1 \le k \le w(i) \notag \end{align}\]

Alternatively, their IP model introduces two sets of variables: \(x_{ic}\), a binary variable indicating whether color \(c\) is assigned to vertex \(i\), and \(z_{\max}\), an integer variable representing the maximum color used. The IP formulation is expressed as: \[\begin{align} \text{Minimize} \quad & z_{\max} \\[0.5ex] \text{Subject to} \quad & \sum_{c=1}^{UB} x_{ic} = w(i) && \forall i \in V \\ & x_{ic} + x_{je} \le 1 && \begin{aligned}[t] &\forall \{i,j\} \in E, i \neq j,\\ &1 \le c,e \le UB,\\ &|c-e| < d(\{i,j\}) \end{aligned} \\ & x_{ic} + x_{ie} \le 1 && \begin{align}[t] &\forall i \in V,\\ &1 \le c,e \le UB,\\ &|c-e| < d(\{i,i\}) \end{align} \\ & z_{\max} \ge c\,x_{ic} && \begin{align}[t] &\forall i \in V,\\ &1 \le c \le UB \end{align} \\ & x_{ic} \in \{0,1\} && \begin{aligned}[t] &\forall i \in V,\\ &1 \le c \le UB \end{aligned} \\ & z_{\max} \in \mathbb{R} \end{align}\]

Their comparative studies of these formulations show that the IP model generally outperforms the CP model in terms of computational efficiency, particularly for larger instances. While the IP model is more computationally efficient at proving optimality, they note that the CP model still holds a specific advantage in certain scenarios. If the solvers hit the designated time limit without finding the optimal solution, the CP model tends to return a higher-quality feasible solution than the IP model. However, both models face significant challenges when scaling to larger problem sizes due to the exponential growth of the search space.

By translating complex combinatorial constraints into a unified Boolean formula, SAT methods leverage the highly optimized inference engines of modern SAT solvers. Because these solvers utilize advanced techniques such as Conflict-Driven Clause Learning (CDCL) [16], which allows the algorithm to learn from dead ends and drastically prune the search tree, they excel at navigating tightly constrained problem spaces. For the BCP, the most significant recent advancement was made by Faber et al. (2024) [13], who proposed highly effective partial-ordering-based SAT encodings (POP-S-B and POPH-S-B). By generalizing earlier ordering approaches, their encodings optimally solved several previously open GEOM benchmark instances for the first time.

Consequently, the current state of the literature reveals a significant research gap in solving the BMCP. First, while metaheuristic algorithms produce excellent feasible solutions, they inherently lack the mathematical mechanisms required to prove optimality. Second, exact approaches such as the CP and IP models developed by Dias et al. [9], [10] successfully provide these strict optimality guarantees, yet their scalability remains highly restricted, severely limiting their application to larger problem instances. Finally, despite the fact that SAT-based methods demonstrated tremendous success and computational efficiency for the related BCP in 2024, there is currently no existing SAT encoding formulated for the BMCP. Bridging this gap requires more than trivial adaptations; relying on naive reductions, such as transforming a BMCP instance into a standard BCP by splitting vertices into dense cliques, inherently triggers a catastrophic proliferation of variables and clauses that neutralizes the advanced CDCL mechanisms. Therefore, there is an imperative need to formulate compact, native SAT encodings that directly capture both intra-vertex and inter-vertex distance constraints to effectively harness the deductive power of SAT solvers for the BMCP.

3 SAT Encodings for the Bandwidth Multicoloring Problem↩︎

In this section, we develop three SAT formulations for the BMCP. To establish our framework, we first introduce a Flat Encoding (FE) as a direct baseline, followed by an intermediate Slot-Based Encoding (SBE) that utilizes local bounds. Finally, we present the core contribution of this paper: the highly optimized Order-Based Encoding (OBE), which elegantly overcomes the spatial and computational limitations of the prior models.

3.1 Global and Local Bound Computation↩︎

To reduce the search space and accelerate SAT-based solving, we establish tight lower and upper bounds for the span, as well as restricted color domains for individual vertices.

The minimum span is constrained by the densest substructures within the graph. For any clique \(C \subseteq V\), the required span is at least \(1 + (W_C - 1) \cdot d_{min}^C\), where \(W_C = \sum_{v \in C} w(v)\) is the total color requirement and \(d_{min}^C = \min_{u, v \in C} d(\{u,v\})\) is the tightest distance constraint in \(C\). We define the lower bound \(LB\) as the maximum bound discovered across maximal cliques, which are extracted using the Bron-Kerbosch algorithm [17]. A formal proof is provided in Appendix 6.

Conversely, an upper bound (\(UB\)) caps the SAT variables’ domains. The trivial bound \(1 + \left( \sum_{u \in V} w(u) - 1 \right) \cdot \max_{\{u,v\} \in E} d(\{u,v\})\) is overly large and yields intractable SAT formulas. Instead, we compute a tighter \(UB\) via a greedy heuristic [10] (Algorithm 1). By prioritizing vertices with the largest weight \(w(u)\), the algorithm sequentially assigns colors, incrementally increasing candidate values until all distance constraints are satisfied. The maximum color utilized by this heuristic becomes our global \(UB\).

Given a target span \(k \in [LB, UB]\), we restrict the allowed color domains for each vertex to preemptively prune invalid assignments. To explicitly break symmetries, we enforce a strict ascending order for the colors assigned to any vertex \(u\): \(c(u)_1 < c(u)_2 < \dots < c(u)_{w(u)}\). This ordering dictates tight bounds on the minimum (\(LB_{u,i}\)) and maximum (\(UB_{u,i}\)) possible values for the \(i\)-th color of vertex \(u\): \[\begin{align} {2} LB_{u,i} &= 1 + (i-1)\cdot d(\{u,u\}) &\qquad& \forall u \in V,\; i \in [1,w(u)] \\ UB_{u,i} &= k - (w(u)-i) \cdot d(\{u,u\}) &\qquad& \forall u \in V,\; i \in [1,w(u)] \end{align}\]

If \(UB_{u,i} < LB_{u,i}\) for any vertex \(u\) and index \(i\), the targeted span \(k\) is mathematically too small to accommodate \(u\)’s intra-vertex constraints. Consequently, we can immediately deduce that \(k\) is invalid without generating or evaluating the SAT formula.

3.2 Flat Encoding (FE)↩︎

Serving as our initial baseline, this flat SAT encoding is a direct transformation of the IP model proposed by Dias et al. [9], [10]. The encoding uses Boolean variables for each vertex \(u \in V\) and each available color \(m \in \{1, 2, \dots, k\}\) with the semantics that \(x_{u,m} = \text{true} \iff m\in c(u)\).

The constraints are defined as follows:

• Color cardinality constraint: \[\sum_{m=1}^k x_{u, m} = w(u) \quad \forall u \in V\]

• Intra-vertex color distance constraint: \[\neg x_{u, m} \lor \neg x_{u, n} \quad \begin{align} &\forall u \in V, \; \forall m,n \in \{1, \dots, k\} \\ &\text{s.t. } m < n \text{ and } n - m < d(\{u,u\}) \end{align}\]

• Inter-vertex color distance constraint: \[\neg x_{u,m} \lor \neg x_{v,n} \quad \begin{align} &\forall \{u,v\} \in E, u \neq v, \; \forall m,n \in \{1, \dots, k\} \\ &\text{s.t. } |m - n| < d(\{u,v\}) \end{align}\]

3.3 Slot-Based Encoding (SBE)↩︎

The flat encoding does not take advantage of the restricted color domains computed for each vertex, as it evaluates all colors up to the target span \(k\). To address this issue and build towards our primary formulation, this encoding leverages the local bounds to exploit the strict ascending order for the colors assigned to any vertex. It employs Boolean variables \(x_{u,i,m} = \text{true} \iff c(u)_i = m \quad \forall u \in V, i \in [1, w(u)], m \in [LB_{u,i}, UB_{u,i}]\).

The constraints for this encoding are:

• Exactly-one value for the \(i\)-th color: \[\sum_{m=LB_{u,i}}^{UB_{u,i}} x_{u, i, m} = 1 \quad \forall u \in V, \forall i \in [1, w(u)]\]

• Intra-vertex color distance constraint: \[\neg x_{u,i,m} \lor \neg x_{u,i+1,n} \quad \begin{align} &\forall u \in V, \; \forall i \in [1, w(u)-1], \\ &\forall m \in [LB_{u,i}, UB_{u,i}], \; \forall n \in [LB_{u,i+1}, UB_{u,i+1}] \\ &\text{s.t. } n - m < d(\{u,u\}) \end{align}\]

• Inter-vertex color distance constraint: \[\neg x_{u,i,m} \lor \neg x_{v,j,n} \quad \begin{align} &\forall \{u,v\} \in E, u \neq v, \; \forall i \in [1, w(u)], \; \forall j \in [1, w(v)] \\ &\forall m \in [LB_{u,i}, UB_{u,i}], \; \forall n \in [LB_{v,j}, UB_{v,j}] \\ &\text{s.t. } |m - n| < d(\{u,v\}) \end{align}\]

The Color cardinality constraint is inherently satisfied by instantiating variables over the explicit index \(i \in [1, w(u)]\), which naturally guarantees that each vertex \(u\) is assigned exactly \(w(u)\) colors, making an explicit encoding of this constraint unnecessary.

3.4 Order-Based Encoding (OBE)↩︎

Representing the primary contribution of this work, we extend the partial-ordering concepts proposed by Faber et al. [13] and our intermediate slot-based approach to develop the Order-Based Encoding (OBE) for the BMCP. The encoding uses the following variables:

• \(x_{u,i,m} = \text{true} \iff c(u)_i=m\)

• \(g_{u,i,m} = \text{true} \iff c(u)_i\geq m\)

The constraints are defined as follows:

• Linkage between variables \(x\) and \(g\): \[\begin{align} {2} x_{u,i,m} &\leftrightarrow g_{u,i,m} \wedge \neg g_{u,i,m+1} &\qquad& \begin{aligned}[t] &\forall u \in V,\; i \in [1,w(u)],\\ &m \in [LB_{u,i},UB_{u,i}-1] \end{aligned} \\ x_{u,i,UB_{u,i}} &\leftrightarrow g_{u,i,UB_{u,i}} &\qquad& \forall u \in V,\; i \in [1,w(u)] \end{align}\]

• Monotonicity of variable \(g\): \[\begin{align} {2} \label{eq:monotonicity} g_{u,i,m} \rightarrow g_{u,i,m-1} &\qquad& \begin{aligned}[t] &\forall u \in V,\; i \in [1,w(u)],\\ &m \in [LB_{u,i}+1,UB_{u,i}] \end{aligned} \end{align}\tag{1}\]

• Lower bound of the color value assigned to each vertex: \[\begin{align} {2} g_{u,i,LB_{u,i}} \qquad \forall u \in V, i \in [1, w(u)] \end{align}\]

• Intra-vertex color distance constraint: \[\begin{align} {2} g_{u,i,m} \rightarrow g_{u,i+1,m+d(\{u,u\})} &\qquad& \begin{aligned}[t] &\forall u \in V,\; i \in [1,w(u)-1],\\ &m \in [LB_{u,i}, UB_{u,i}] \end{aligned} \end{align}\]

• Inter-vertex color distance constraint: \[\begin{align} {2} x_{u,i,m} \rightarrow (g_{v,j,m+d(\{u,v\})} \vee \neg g_{v,j,m - d(\{u,v\})+1}) &\qquad& \begin{aligned}[t] &\forall \{u,v\} \in E, u \neq v,\\ &i \in [1, w(u)], j \in [1, w(v)],\\ &m \in [LB_{u,i}, UB_{u,i}] \end{aligned} \end{align}\]

(Non-existent variables are considered as true or false constants accordingly and do not appear in the formula).

Explicit SAT clauses for the Exactly-one value for the \(i\)-th color constraint are unnecessary in this formulation. Specifically, linkage and monotonicity constraints ensure that the sequence \(g_{u,i,m}\) transitions from true to false exactly once, forcing exactly one \(x_{u,i,m}\) to evaluate to true for each index \(i\). A formal proof for the order-based encoding is provided in Appendix 7.

3.5 Complexity Analysis↩︎

In this section, we analyze the spatial complexity of the proposed SAT encodings by comparing the asymptotic number of variables and clauses they generate. To facilitate this comparison, let \(W = \max_{u \in V} w(u)\) denote the maximum weight among all vertices in the graph.

Table 1 provides a theoretical summary of the encoding sizes for the FE, SBE, and OBE. It is important to note that both the FE and SBE formulations utilize Sinz’s sequential counter encoding [18].

3.6 Finding the optimal solution↩︎

The SAT formulation described in the preceding sections models the BMCP as a decision problem: determining whether a valid coloring exists for a given fixed span. To solve the optimization variant of the BMCP—finding the minimum possible span \(k^*\)—we must systematically evaluate different span values. Rather than repeatedly generating and solving independent SAT instances from scratch, which discards valuable learned clauses and incurs significant encoding overhead, we employ an incremental SAT-solving strategy.

Our optimization process utilizes a top-down linear search. As established in Section 3.1, the upper bound algorithm guarantees an initial valid span \(UB\). Therefore, the solver is instantiated exactly once with the complete encoding for the span value \(UB\). To progressively search for a better span, we iteratively restrict the search space by forbidding the maximum currently allowed color.

To evaluate if the graph can be colored with a span of \(k-1\) (given that \(k\) is currently valid), we do not need to alter the existing constraints. Instead, we dynamically inject unit clauses that strictly prohibit any vertex from being assigned the color value \(k\). Depending on the chosen encoding, we append the corresponding incremental formula to the solver:

• Flat encoding: \[\label{eq:incremental-flat} \neg x_{u,k} \qquad \forall u \in V\tag{2}\]

• Slot-based encoding: \[\label{eq:incremental-slot} \neg x_{u,i,k} \qquad \forall u \in V, i \in [1, w(u)] \quad \text{s.t.} \quad LB_{u,i} \leq k \leq UB_{u,i}\tag{3}\]

• Order-based encoding: \[\label{eq:incremental-order} \neg g_{u,i,k} \qquad \forall u \in V, i \in [1, w(u)] \quad \text{s.t.} \quad LB_{u,i} \leq k \leq UB_{u,i}\tag{4}\]

By adding these unit clauses, the SAT solver structurally invalidates any assignment relying on the color \(k\), effectively forcing the target span to \(k-1\). This process is repeated, decrementing the target span one by one, until the solver returns an UNSAT status. The optimal span \(k^*\) is then strictly the last value for which a SAT status was achieved.

The complete procedure is formalized in Algorithm 2.

4 Experimental Evaluation↩︎

4.1 Dataset↩︎

We evaluate the proposed Order-Based Encoding (OBE) using 53 established benchmark instances from prior BMCP literature, divided into two distinct suites.

The first suite comprises 33 geometric instances, known as the GEOM set, introduced by Trick [14]. Vertices are distributed across a \(10,000 \times 10,000\) grid, with edges connecting nodes within a predefined distance threshold; edge weights are inversely proportional to this distance. This set includes sparse (GEOMn) and dense (GEOMna, GEOMnb) configurations. Vertex weights are uniformly distributed in \([1, 10]\) for GEOMn and GEOMna, and \([1, 3]\) for GEOMnb.

The second suite contains the remaining 20 instances, derived from the classic Philadelphia (21 vertices) and Helsinki (25 vertices) instances, originally formulated for the Minimum Span Channel Assignment Problem (MS-CAP) [8], plus a 55-vertex artificial extension. These instances directly model the physical topology and interference constraints of real-world cellular telecommunication networks.

4.2 Experimental Setup↩︎

All local experiments were conducted on an Intel Core i5-12500H with 16 GB RAM running Ubuntu 24.04 LTS. A 3600-second time limit was applied to these experiments, covering both the encoding and search phases. To isolate encoding effectiveness, all SAT-based methods utilized CaDiCaL (v3.0.0) [19]. Additionally, all local experiments used identical initial lower and upper bounds (see Section 3.1). The baseline FE and SBE formulations, alongside our main OBE model, were implemented in C++. Specifically, the FE and SBE method utilizes the sequential counter encoding [18] to enforce its cardinality constraints, whereas the OBE method handles these inherently. We conducted two primary sets of comparisons:

First, we compared OBE against FE, SBE, and two SAT models (POP-S-B and POPH-S-B) by Faber et al. [13]. Because the latter models only apply to the BCP, BMCP instances were first converted into equivalent BCP instances. We executed POP-S-B and POPH-S-B using the authors’ original Python 3.14 source code¹.

Second, OBE was compared against exact models, heuristics, and metaheuristics. We re-implemented the CP and IP models proposed by Dias et al. [9], [10], evaluating them with CPLEX v22.2² and Gurobi v13.0.2³. For the LPR heuristic [6] and VNS metaheuristic [7], we cite the authors’ published computational results directly; consequently, these were the only comparisons not bound by our shared hardware or the 3600-second time limit.

4.3 Metrics↩︎

To comprehensively evaluate and compare the performance of the various approaches, we defined specific evaluation metrics tailored to the two primary sets of comparisons outlined in Section 4.2. Two main metrics were consistently applied across all comparisons: the best span value obtained (\(k^*\)) and the total computational time required to find or report the solution. To ensure statistical rigor, the evaluated methods were subsequently ranked using the Friedman test [20], with the analysis conducted exclusively based on the best span value.

In addition to the core metrics, we evaluated the number of instances where the optimal span was successfully found and proven. This metric was applied to the entirety of the first set of comparisons (evaluating OBE against FE, SBE, POP-S-B, and POPH-S-B) as well as to the exact models evaluated in the second set. This metric was omitted for the LPR heuristic and VNS metaheuristic portions of the second comparison set, as approximate methods cannot definitively prove solution optimality.

4.4 Results and Analysis↩︎

In the following tables, underlined and boldface values indicate the best span (\(k^*\)) and proven optimal solutions, respectively. The rows #OPTIMAL and #BEST denote the total counts of optimal and best-known spans, while #AVG. Rank reports the average Friedman test ranking. The Gap column shows the difference between the OBE model’s span and the overall minimum \(k^*\). Finally, TO, MO, and a hyphen (-) represent Time Out (3600s), Memory Out, and failure to find a feasible solution, respectively.

4.4.1 Comparison of OBE with Alternative SAT Encodings↩︎

The computational results evaluating the efficacy of the proposed Order-Based Encoding (OBE) against alternative SAT encodings, specifically SBE, FE, POP-S-B, and POPH-S-B [13], reveal a substantial performance paradigm shift in both solving capacity and solution quality. Tables ¿tbl:tab:compare95sat95geom? and ¿tbl:tab:compare95sat95mscap? detail this comparison across the GEOM and MS-CAP benchmark datasets, respectively.

width=

width=

Regarding the capacity to prove optimality, the proposed OBE formulation demonstrates a superiority over existing models. Most strikingly, on the GEOM dataset, OBE exactly doubles the number of proven optimal solutions compared to FE, solving 14 instances to optimality versus FE’s 7. Furthermore, OBE is the only SAT encoding capable of proving optimality on instances such as GEOM30, GEOM50, GEOM60, and GEOM70b, where all other models prematurely exhausted the computational time limit. While the performance gap narrows on the MS-CAP dataset, with OBE, SBE, and FE each proving optimality for 16 out of 20 configurations, OBE maintains its top-tier status while simultaneously exposing the limitations of the specialized POP-S-B and POPH-S-B models, which managed to prove only 8 and 6 optimal solutions, respectively. This disparity indicates that OBE’s underlying logical structure significantly accelerates the solver’s ability to prune the search space and verify lower bounds.

Beyond the verification of exact optima, the true practical significance of the OBE formulation lies in its robustness when processing difficult instances. In this regard, OBE is exceptionally reliable. Across the entirety of the 53 instances spanning both datasets, the calculated gap between the span identified by OBE and the minimum overall \(k^*\) is zero for 51 instances. Consequently, even when interrupted by a timeout, OBE consistently returns a solution that is highly competitive with, and frequently superior to, the best solutions generated by alternative SAT encodings, with FE being the only model to find marginally tighter bounds on two specific MS-CAP configurations.

The interpretation of the bounds further underscores OBE’s dominance. OBE successfully secured the best-known span in the vast majority of the evaluated configurations (33 out of 33 in GEOM, and 18 out of 20 in MS-CAP). In stark contrast, the search trajectories of alternative encodings often stagnated far from the optimal region. For example, on the GEOM dataset, the closest competitor in terms of solution quality (POPH-S-B) could only reach the best bound in approximately 39% of the instances (13 out of 33), while FE reached it in only about 21% (7 out of 33). On challenging MS-CAP instances utilizing the \(C^6_{21}\) matrices, alternative models struggled to find high-quality spans, whereas OBE reported tighter bounds. Conversely, FE demonstrated a slight advantage on instances utilizing the \(C^8_{21}\) matrices, where it managed to surpass OBE. This empirical evidence signifies that OBE not only elevates the ceiling of SAT-based optimization by solving more instances to proven optimality, but also fundamentally raises the floor by consistently providing highly competitive, near-optimal bounds when exact verification remains computationally intractable.

The most significant interpretation of these results lies in the disproportionate computational expenditure required by competing methods to achieve comparable solution quality. To reach the bounds on challenging instances, LPR and VNS required an exorbitant allocation of time. For example, on the GEOM120a instance, LPR consumed over 24,800 seconds, and the VNS metaheuristic demanded a staggering 59,717 seconds. Similarly, VNS required more than 21,600 seconds just to process GEOM50a. By stark contrast, all OBE evaluations were strictly truncated at 3,600 seconds. Despite this severe computational restriction, OBE consistently matched the best-known bounds established by these specialized approximate methods on massive instances like GEOM70, GEOM80b, and GEOM90, resulting in a gap of zero. The ability of OBE to yield identical or superior span values in a mere fraction of the time redefines the practical utility of SAT encodings. It proves that the OBE model does not merely compete with heuristics on solution quality, but fundamentally outclasses them in computational efficiency, offering a balance between rigorous exactness and execution speed.

5 Conclusion↩︎

This paper presented the first SAT-based exact framework for the Bandwidth Multicoloring Problem (BMCP). The proposed approach is centered on an efficient SAT encoding that compactly models both intra-vertex and inter-vertex color distance constraints. Combined with tight color domain reduction and incremental SAT solving, the resulting formulation effectively reduces the search space while preserving exactness. Experimental results on the standard GEOM and MS-CAP benchmark suites demonstrate that the proposed framework significantly advances the state of the art in exact BMCP solving. Within a one-hour time limit, it proves optimality for several benchmark instances that remained unsolved by previous exact approaches and verifies the optimality of previously reported best-known solutions. In particular, on the challenging GEOM benchmark, our comprehensive evaluation increases the total number of instances with proven optimality from 9 to 16, compared with the previous state-of-the-art CP/IP-based exact approach. Specifically, the proposed OBE framework independently solves 14 instances to optimality, while our modern Gurobi re-implementation of the IP model uniquely resolves 2 additional instances. Remarkably, these advancements were achieved requiring a computational time limit of only one hour rather than 48 hours. These results demonstrate a substantial improvement in the practical scalability and effectiveness of exact BMCP solving. Although state-of-the-art metaheuristics remain superior in terms of solution quality on the most difficult instances, the proposed framework consistently strengthens the performance of existing exact approaches while preserving the ability to certify global optimality. These results demonstrate that SAT-based reasoning provides an effective and scalable foundation for exact BMCP optimization and significantly extends the frontier of provably optimal solutions. Several directions for future research remain promising. First, the proposed SAT encoding could be further strengthened through additional symmetry-breaking techniques and tighter constraint formulations. Second, integrating SAT with optimization paradigms such as MaxSAT or hybrid SAT-based approaches may further improve scalability on large and difficult instances. Finally, extending the proposed framework to other graph coloring variants involving distance or multicoloring constraints represents another interesting direction for future investigation.

Funding↩︎

This work has been supported by VNU University of Engineering and Technology under project number CN26.01.

Data Availability Statement↩︎

The source code for all encoding implementations, benchmark instances, and experimental datasets are publicly available in a GitHub repository: https://github.com/homulily85/bmcp [21]

6 Correctness of Lower Bound for the BMCP↩︎

In this appendix, we establish the formal correctness of the lower bound for the BMCP.

7 Correctness of Order-Based Encoding↩︎

This appendix establishes the correctness of the proposed order-based encodings.

References↩︎

---

1. https://github.com/s6dafabe/popsatgcpbcp↩︎

2. https://www.ibm.com/products/ilog-cplex-optimization-studio↩︎

3. https://www.gurobi.com/↩︎