This paper tackles the Minimum Span Antibandwidth Labeling (MSABL) and Minimum Span Cyclic Antibandwidth Labeling (MSCABL) problems, both of which are NP‑hard graph labeling tasks. Traditional antibandwidth formulations fix a label set and maximize the minimum (cyclic) distance $d_{\min}$ between labels of adjacent vertices. In contrast, we fix a desired minimum distance $\delta$ and, under the constraint $d_{\min}\ge \delta$, minimize the label span $\mathrm{span}=\max\{\ell(v)\}-\min\{\ell(v)\}$.
To solve MSABL/MSCABL, we propose a unified Boolean Satisfiability (SAT) framework. The key idea is to turn the problem into a series of decision problems: for a candidate span $S$, decide whether a feasible labeling exists. Feasibility is monotone in $S$ (if $S$ works, any $S'\ge S$ also works), enabling binary or linear search to speed up the process.
SAT encoding essentials
- Variables: $x_{v,k}$ indicates whether vertex $v$ receives label $k$ ($k\in\{1,\dots,S\}$).
- Uniqueness: each vertex gets exactly one label: @@@MATH_BLOCK12@@@\sum{v\in V} x_{v,k}\le 1\quad\forall k.@@@MATH_BLOCK13@@@|\ell(u)-\ell(v)|{\text{cyc}} \ge \delta,$$ where the cyclic distance is $\min{|a-b|, S-|a-b|}$.
Two SAT solving strategies
- Parallel SAT: launch multiple SAT solvers simultaneously, each testing a different candidate span $S_i$ (e.g., $S, S+1,\dots$). Multi‑core parallelism reduces overall search time.
- Incremental SAT: keep a single SAT instance, start with $S=\delta$, and add new label variables and constraints when the current instance is unsatisfiable, thus reusing learned clauses.
Experiments
- Benchmarks: graphs derived from the Harwell‑Boeing sparse matrix collection.
- Competitors: CPLEXCP, CPLEXMIP, Gurobi.
- Findings: Without the no‑hole constraint, SAT approaches match commercial solvers in solution quality; parallel SAT excels on MSCABL, while incremental SAT is superior for MSABL. With the no‑hole constraint, SAT remains competitive with CPLEXCP and significantly outperforms CPLEXMIP and Gurobi, especially on MSCABL.
These results demonstrate that SAT solving is an effective exact method for both MSABL and MSCABL.
Review