AI 中文总结
本研究提出一种基于SAT的精确方法，可在3600秒内为多数中小型二维带宽最小化问题基准实例证明最优带宽，优于之前耗时72小时的精确方法，还发现并证明了三个更优带宽值。
AI 中文摘要
二维带宽最小化问题（2DBMP）旨在将 guest 图单射嵌入到正方形网格中，以最小化其边的最大曼哈顿距离。启发式方法可提供较紧的上界，但这些上界本身无法证明最优性。我们提出一种高效的基于SAT的2DBMP精确方法，该方法增量搜索最小可行带宽，并通过可满足性和不可满足性结果证明最优性。在标准$\boldsymbol{\rceil\boldsymbol{\boldsymbol{n}}\rceil \times \rceil\boldsymbol{\boldsymbol{n}}\rceil}$宿主网格上，在3600秒的时间限制下，所提出的SAT方法为43个Regular实例中的41个、93个Harwell--Boeing实例中的42个证明了最优带宽，在3600秒时间限制内实现了比之前采用72小时时间限制评估的精确方法更广泛的最优性证明。此外，该方法证明了三个带宽值优于本研究中考虑的所有已发表比较值，并将这三个值确定为最优。我们进一步在替代宿主几何结构（即$2\times\rceil\boldsymbol{\boldsymbol{n}/2\rceil}$和$n\times n$网格）上评估该方法，以评估其在标准宿主之外的有效性。总体而言，结果表明，所提出的SAT方法为本研究中考虑的顶点数少于400的中小型基准实例提供了一种有效的精确方法，而启发式方法对于更大和更具挑战性的实例仍然重要。
英文摘要
The two-dimensional bandwidth minimization problem (2DBMP) seeks an injective embedding of a guest graph into a square grid that minimizes the maximum Manhattan distance over its edges. Heuristic methods can provide strong upper bounds, but these bounds do not by themselves certify optimality. We present an efficient exact SAT-based approach for 2DBMP that incrementally searches for the minimum feasible bandwidth and certifies optimality through satisfiability and unsatisfiability results. On the standard $\lceil\sqrt n\rceil \times \lceil\sqrt n\rceil$ host grid, under a 3600 s time limit, the proposed SAT approach certifies optimal bandwidths for 41 of 43 Regular instances and 42 of 93 Harwell--Boeing instances, achieving substantially broader optimality certification within the 3600 s time limit than a previous exact approach evaluated with a 72-hour time limit. In addition, it certifies three bandwidth values that improve all previously published comparison values considered in this study and establishes all three as optimal. We further evaluate the approach on alternative host geometries, namely $2\times\lceil n/2\rceil$ and $n\times n$ grids, to assess its effectiveness beyond the standard host. Overall, the results demonstrate that the proposed SAT approach provides an effective exact method for the small- and medium-sized benchmark instances considered in this study, with fewer than 400 vertices, while heuristic methods remain important for larger and more challenging instances.
Comments30 pages, 10 figures, 9 tables
