💻 computer science

A SAT-Based Exact Approach for Radio k-Labeling

本文提出了一种用于无线电 $k$ -标记问题的精确、增量式基于 SAT 的框架，该框架通过为 38 个实例建立新的最佳已知解，并为 146 个基准图中的 109 个证明其最优性，从而超越了最先进的商业求解器和启发式算法。

原作者： Huong Vu Thanh, Duc Dao Van, Khanh To Van

发布于 2026-07-23

📖 1 分钟阅读☕ 轻松阅读

原作者： Huong Vu Thanh, Duc Dao Van, Khanh To Van

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你是某个大型广播电台网络的总工程师，你的工作是为散布在城市各处的数百个发射器分配频率频道。难点在于，你不能直接给每个人分配相同的频道，否则他们会互相干扰。如果两个发射器紧挨在一起，它们需要的频率必须相隔很远；如果它们稍远一些，频率可以稍微靠近一点，但仍不能太近。目标是使用尽可能小的频率范围（即“跨度”），以确保整个系统在没有干扰的情况下运行。在数学世界中，这被称为“无线电 k-标记”（radio k-labeling）问题。这是一个给地图上的点分配数字的谜题，其中点与点之间的距离决定了它们数字之间需要相隔多远。

长期以来，数学家们一直试图解决这个谜题。有些人构建了巧妙的捷径（启发式算法），可以快速猜出一个不错的答案，但他们无法证明那一定是“最好”的答案。另一些人则尝试使用强大的计算机程序（如 ILP 求解器）来寻找完美解，但当地图变得太大或过于复杂时，这些程序往往会不堪重负，在完成任务之前就耗尽内存或时间。核心问题在于：是否存在一种方法，可以在不让计算机崩溃的情况下，为这些棘手的地图找到绝对最佳且经过验证的解决方案？

这篇论文介绍了一种使用名为“SAT 求解器”的工具来解决这个谜题的全新、超级智能的方法。你可以把 SAT 求解器想象成一名侦探，他负责检查一组规则是否能同时成立。作者构建了一个框架，它不仅仅是检查一次规则，而是玩一场“找热找冷”的游戏。它从一个较宽的允许频率范围开始，并询问侦探：“用这么多频率可以做到吗？”如果答案是“可以”，侦探就会找到一个解，但框架会立即说：“好吧，但能不能用更少的频率做到？”然后它会收紧规则并再次询问。这个魔术技巧在于，侦探会记住它从之前的“否”回答中所学到的一切。通过不从头开始，而是利用这些记忆，它能够跳过巨大的不可能解空间，从而使搜索过程极其迅速。

研究人员在 146 种不同类型的地图上测试了这种新的“增量式 SAT”（incremental SAT）方法，这些地图涵盖了从简单的直线、圆圈到复杂的、扭曲的结构（如蛇形和树形）。他们发现，这种方法是一个强大的力量。它发现了 38 个此前从未有人发现过的全新最佳已知答案。更重要的是，它证明了其中 109 个解实际上是绝对最优解，这个数字比以往任何方法所能确认的数量都要高得多。虽然旧的计算机程序（ILP 求解器）在处理简单的“平坦”地图时仍然表现最佳，但新的 SAT 方法在点与点之间距离不断增加的复杂地图中完全占据了统治地位。事实证明，通过将 SAT 侦探的记忆力与旧程序的蛮力相结合，该团队已经开启了一种解决无线电频率谜题的新途径，而这些谜题此前被认为太难，无法被完美破解。

技术摘要：一种基于 SAT 的无线电 $k$ -标记法精确求解方法

问题定义
本文研究的是无线电 $k$ -标记问题（也称为无线电 $k$ -着色问题），这是一个源自信道分配问题的组合优化问题。给定一个连通图 $G=(V, E)$ ，其直径为 $k = \text{diam}(G)$ ，目标是为顶点分配非负整数标签 $f(v)$ ，使得对于每一对不同的顶点 $u, v$ ，条件 $|f(u) - f(v)| \ge k + 1 - d(u, v)$ 均成立，其中 $d(u, v)$ 是最短路径距离。目标是最小化标记的跨度（span），定义为 $\max_{v \in V} f(v)$ 。可能的最小跨度称为无线电数（radio number），记作 $rn(G)$。

虽然针对特定图族（如路径、圈、树）存在理论构造，且启发式算法能为一般图提供可行解，但针对广泛图类的精确解仍然很少。现有的整数线性规划（ILP）公式由于搜索空间快速增长以及在优化迭代之间缺乏信息复用，面临着可扩展性问题。

方法论
作者提出了一种精确的、增量式的基于 SAT 的框架，该框架结合了紧凑的阶序编码（order encoding）和迭代优化策略。

SAT 编码：
本文开发了两种基于标签域 $\{1, \dots, UB\}$ 的布尔可满足性（SAT）编码，其中 $UB$ 是预计算的上界：
- 直接编码（Direct Encoding）： 使用赋值变量 $x_{v,l}$ （表示顶点 $v$ 是否具有标签 $l$ ）。它通过成对冲突子句强制执行约束。虽然在逻辑上与 ILP 模型等价，但其无线电约束需要 $O(n^2 UB k)$ 个子句，导致在单位解析（unit resolution）下的传播能力较弱。
- 阶序编码（Order Encoding）： 除了赋值变量外，还引入了阈值变量 $g_{v,l}$ （表示 $f(v) \ge l$ 是否成立）。这种编码能更紧凑地表示无线电约束 $|f(u) - f(v)| \ge \Delta_{uv}$ 。它将无线电约束的子句数量从 $O(n^2 UB k)$ 减少到 $O(n^2 UB)$ ，消除了对 $k$ 的依赖。阶序编码还实现了更强的传播，因为不等式 $f(v) \ge c$ 可以映射为单个文字（literals）。
增量求解策略：
该框架采用增量式 SAT 求解范式。该算法不是为每次迭代重新构建公式，而是构建一个单一的求解器实例。算法流程如下：
- 阶段 1： 计算全对间距离并设定 $k = \text{diam}(G)$ 。
- 阶段 2： 构建具有初始上界 $UB$ 的 SAT 模型。
- 阶段 3： 迭代求解公式。如果找到了具有跨度 $\beta$ 的满足赋值，则指示求解器禁止任何 $\ge \beta$ 的跨度（收紧边界）并重新求解。至关重要的是，前一次迭代中的学习子句会被保留，从而避免了冗余的搜索工作。当求解器返回 UNSAT（证明了最优性）或达到时间限制时，循环终止。
对称性破缺：
对于具有旋转对称性的圈图（ $C_n$ ），作者引入了一个对称性破缺约束，将第一个顶点的标签固定为 1（ $f(0)=1$ ）。这减少了搜索空间，并在不丢弃最优解的情况下显著加速了最优性的证明。

核心贡献

新颖框架： 第一个用于无线电 $k$ -标记问题的通用精确 SAT 优化框架，利用了阶序编码和增量求解。
效率提升： 阶序编码相比直接编码减少了子句复杂度并改善了传播；增量方法通过复用学习到的子句，显著降低了与独立 SAT 调用或标准 ILP 方法（会丢弃先前搜索信息）相比的计算开销。
对称性处理： 引入了针对圈图的特定对称性破缺约束，展示了在求解时间上的大幅提升以及增加的已认证最优解数量。

实验结果
该框架在涵盖九种图族（路径、圈、三角蛇形图、 $kC_m$ -蛇形图、梯形图、书本图、友谊图和二项树）的 146 个基准实例上进行了评估，时间限制为 1,200 秒。

性能对比启发式算法： 所提出的 Order-SAT 方法在 98 个未知闭式最优解的实例中，建立了 38 个新的最佳已知无线电数。它生成的可行边界始终比现有的启发式算法（Ub1, Ub3）和直接编码 SAT 更紧凑。
性能对比 ILP：
- 直径增长型图： 对于直径随规模增长的图族（如蛇形图、梯形图、二项树），Order-SAT 在解的质量（更紧的边界）和认证的最优解数量方面均优于商业 ILP 求解器（CPLEX, Gurobi）。ILP 求解器在这些实例上经常耗尽内存或返回松弛的当前最优解。
- 直径恒定型图： 对于直径为常数的图族（如书本图、友谊图），ILP 求解器更为有效，能够快速为所有实例认证最优性。
结合方法： 通过将 SAT 框架与 ILP 模型相结合，本研究为 146 个实例中的 109 个实例认证了最优解，大幅扩展了具有证明最优性的无线电标记基准集。
统计显著性： Friedman 检验确认，Order-SAT 在所有对比方法（包括商业求解器和启发式算法）中取得了最佳整体排名（平均排名 2.58）。

意义
本文声称，增量式 SAT 求解构成了一种实用的精确优化范式，适用于传统上由理论构造和启发式算法主导的图标记问题。这项工作表明：

现代 SAT 求解器在结合紧凑编码和增量策略时，可以解决传统 ILP 公式在可扩展性方面难以应对的复杂组合优化问题。
所提方法与 ILP 是互补的：对于直径增长的图，它优于 ILP；而对于直径恒定的图，ILP 仍是首选。
该框架成功弥合了理论边界与认证精确解之间的差距，为确定复杂图结构中的无线电数提供了强大的工具。

作者总结道，这种方法为特定图类提供了一种极具竞争力的商业求解器替代方案，并突显了增量式 SAT 求解在其他图标记和组合优化问题中的潜力。

技术摘要：一种基于 SAT 的无线电 kkk-标记法精确求解方法

类似论文

技术摘要：一种基于 SAT 的无线电 $k$ -标记法精确求解方法