本文研究 最小跨度反带宽标记 (MSABL) 与 最小跨度循环反带宽标记 (MSCABL) 两类 NP 难图标记问题。传统的反带宽问题固定标签集合，目标是最大化相邻顶点标签之间的最小（循环）距离 $d_{\min}$；而本文固定一个期望的最小距离 $\delta$，在满足 $d_{\min}\ge \delta$ 的前提下，最小化标签的最大值，即 标签跨度 $\mathrm{span}=\max\{\ell(v)\}-\min\{\ell(v)\}$。
为求解 MSABL/MSCABL，作者构建了统一的 布尔可满足性 (SAT) 框架。核心思路是将原问题转化为一系列 决策问题：给定候选跨度 $S$，判断是否存在满足约束的标记方案。由于可行性随 $S$ 的增大而单调（若 $S$ 可行，则任意 $S'\ge S$ 亦可行），可以采用二分搜索或线性递增搜索加速。
SAT 编码要点
- 变量：$x_{v,k}$ 表示顶点 $v$ 是否被标记为 $k$（$k\in\{1,\dots,S\}$）。
- 唯一性约束：每个顶点恰好选一个标签：$$\sum_{k=1}^{S} x_{v,k}=1\quad\forall v.$$
- 标签唯一约束（可选的 no‑hole 约束）：每个标签最多被一个顶点使用：$$\sum_{v\in V} x_{v,k}\le 1\quad\forall k.$$
- 最小距离约束：对每条边 $(u,v)\in E$，要求标签差的循环距离不小于 $\delta$：$$\bigl|\ell(u)-\ell(v)\bigr|_{\text{cyc}} \ge \delta,$$ 其中循环距离定义为 $\min{|a-b|, S-|a-b|}$。
两种 SAT 求解策略
-
并行 SAT：同时启动多个 SAT 求解器，每个求解器对应不同的候选跨度 $S_i$（如 $S, S+1, \dots$），利用多核加速整体搜索。
-
增量 SAT：仅维护单个 SAT 实例，初始 $S=\delta$，在每次不满足时 添加 新的标签变量并 约束 先前解空间，从而避免重复构造。
实验
- 基准：Harwell‑Boeing 稀疏矩阵集合中的图实例。
- 对比求解器：CPLEXCP、CPLEXMIP、Gurobi。
- 结果：在无 no‑hole 约束时，SAT 方法在解的质量上与商业求解器持平；并行 SAT 在 MSCABL 上表现最佳，增量 SAT 在 MSABL 上优势明显。加入 no‑hole 约束后，SAT 仍能与 CPLEXCP 竞争，并显著超越 CPLEXMIP 与 Gurobi，尤其是 MSCABL。
这些实验表明，SAT 求解是 MSABL 与 MSCABL 的一种高效精确方法。
点评