破解 30 年对称调度难题：风车调度 5/6 密度猜想的终极证明

TL;DR

在计算机科学和运筹学领域中，如何安排周期性任务以避免冲突（Pinwheel Scheduling）是一个经典难题。自 1993 年以来，学者们一直猜想：只要任务执行强度的总和（密度）不超过 5/6，就一定存在合法的调度方案。本文作者 Akitoshi Kawamura 通过将整数周期扩展到实数域，配合高效的计算机搜索，终于彻底封死了这个问题的证明闭环，并将该成果应用到了“竹园修剪”优化问题中。

背景定位：工业界的时间表艺术

想象一个工厂，有 $k$ 台机器需要维护，机器 $i$ 必须每 $a_i$ 天至少维护一次。如果每天只能维护一台机器，我们能支持多少台机器同时运行？ 这就是风车调度 (Pinwheel Scheduling) 的核心。由于 (2, 3, 6) 这样的实例在密度刚好超过 5/6 时就会失效，因此 5/6 被认为是该问题的“黄金阈值”。此前，人类最好的证明成绩仅停留在 0.75（3/4）。

技术深挖：从整数到实数的跨越

作者意识到，直接在整数空间处理调度非常琐碎。他提出了分数周期 (Fractional Periods) 的新视角：

• 物理直觉：如果周期 $a_i$ 是实数，要求在 $r$ 天内任务执行次数不少于 $\lfloor r/a_i\rfloor$。
• 这种做法的好处：它允许我们对周期进行微小的缩放（Weakening）和拆分（Splitting），从而将复杂的任务实例平滑地演变为更简单的形式。

核心算法流程

为了证明无限的实例空间，作者设计了两个关键算子：

1. Folding (折叠)：将大周期任务递归地替换为更小周期的任务，同时严格控制总密度的漂移。
2. Rounding (舍入)：将已经减小周期的任务调整回整数状态，以便进行图搜索验证。

图 1: 复杂周期实例 (3, 4, 5, 8) 的一种 8 天循环高度对称调度方案。

实验与验证：计算机辅助的最后一步

尽管有了数学规约，剩余需要验证的实例仍然天文数字。作者通过以下技术大幅优化了搜索速度：

• 状态转换图 (State Transition Graphs)：将调度建模为图中的环路搜索。
• 死状态检测 (Dead States)：利用“紧急度”公式，提前剪掉那些注定会发生调度冲突（Deadline Miss）的分支。
• 等价类合并：对具有相同周期的任务进行排列组合去重，将搜索空间压缩了几个数量级。

最终，作者开源了 pinwheel_solver，在验证了 $C_{5/6}^{22}$ 集合中的所有关键实例后，宣告了 5/6 猜想的成立。

衍生应用：让修剪竹子的效率提升

除了理论证明，本文还解决了一个有趣的优化问题——竹园修剪问题 (BGT)。

• 任务：竹子每天长高 $h_i$，每天只能剪一棵，目标是尽可能降低园中最高竹子的高度。
• 战绩：作者利用 5/6 阈值定理，设计了一个多项式算法，将该问题的近似比从 1.42 压低至 1.33 (4/3)。

图 2: 通过 1.33 倍率缩放，确保缩放后的密度依然落在 5/6 的安全区内。

总结与洞察

本文的成功再次证明了：在复杂的组合数学面前，**“理论归约 + 强力计算”**是破解数十年悬案的重型武器。虽然 5/6 的结论已经确定，但作者在文末也留下了一个迷人的猜想：如果最小周期 $a_1$ 增大，密度阈值是否能进一步逼近 1？

局限性：尽管证明了存在性，但对于任务量极大的实例，寻找最优循环调度的在线生成器（FOLS）在极端场景下的计算开销仍有待进一步优化。