发表机构
VNU University of Engineering and Technology（越南国立大学工程技术大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出最小跨度反带宽与循环反带宽标记问题，并开发统一的SAT求解框架，通过并行与增量策略高效求解，实验证明其在解质量上优于CPLEX和Gurobi。
AI 中文摘要
反带宽（Antibandwidth）与循环反带宽（Cyclic Antibandwidth）问题是NP难的图标记问题，旨在最大化分配给相邻顶点的标签之间的最小（循环）距离。对这些问题的广泛研究已产生了多种数学公式和计算方法。然而，它们的最小跨度视角——即固定一个规定的最小（循环）距离，目标是最小化标签跨度——受到的关注相对较少。在本文中，我们通过引入最小跨度反带宽/循环反带宽标记（MSABL/MSCABL）问题来考虑这一互补视角，并开发了一个统一的基于布尔可满足性（SAT）的框架来求解它们。该基于SAT的框架将MSABL/MSCABL表述为一系列决策问题，并利用其单调性来加速搜索过程。我们还考虑了两种SAT求解策略：并行SAT求解和增量SAT求解。前者同时检查多个候选跨度，而后者在逐步限制标签域的同时重用单个SAT实例。所提出的方法在来自Harwell-Boeing稀疏矩阵集合的基准实例上进行了评估，并与CPLEXCP、CPLEXMIP和Gurobi进行了比较。结果表明，基于SAT的方法在解质量上具有很强的竞争力，其中并行方法在MSCABL上整体表现最佳，增量方法在MSABL上表现最佳。在无空洞（no-hole）约束下，它们与CPLEXCP保持竞争力，并显著优于CPLEXMIP和Gurobi，尤其是在MSCABL上。这些结果证明了SAT求解作为MSABL和MSCABL精确方法的有效性。
英文摘要
The Antibandwidth and Cyclic Antibandwidth problems are NP-hard graph labeling problems that aim to maximize the minimum (cyclic) distance between labels assigned to adjacent vertices. Extensive research on these problems has resulted in a variety of mathematical formulations and computational approaches. However, their minimum span perspective, in which a prescribed minimum (cyclic) distance is fixed and the objective is to minimize the label span, has received comparatively little attention. In this paper, we consider this complementary perspective by introducing the Minimum Span Antibandwidth/Cyclic Antibandwidth Labeling (MSABL/MSCABL) problems and developing a unified Boolean Satisfiability (SAT)-based framework for solving them. The SAT-based framework formulates MSABL/MSCABL as a sequence of decision problems and exploits their monotonicity to accelerate the search process. We also consider two SAT solving strategies, parallel and incremental SAT solving: the former examines multiple candidate spans concurrently, while the latter reuses a single SAT instance while progressively restricting the label domain. The proposed approaches are evaluated on benchmark instances from the Harwell-Boeing Sparse Matrix Collection and compared with CPLEXCP, CPLEXMIP, and Gurobi. The results show that SAT-based approaches are highly competitive in solution quality, with the parallel approach performing best overall for MSCABL and the incremental approach for MSABL. With the no-hole constraint, they remain competitive with CPLEXCP and significantly outperform CPLEXMIP and Gurobi, particularly for MSCABL. These results demonstrate the effectiveness of SAT solving as an exact approach for MSABL and MSCABL.
