A Computer-Assisted Proof of the Optimal Density Bound for Pinwheel Covering

TL;DR

The paper determines the exact density threshold $D(A)$ for schedulability in the covering pinwheel scheduling problem, proving that every instance with $D(A) \ge α^*$ (where $α^* ≈ 1.264$) is schedulable and resolving a long-standing open question. The authors extend Kawamura's packing techniques to the covering setting, allow real-valued periods, and perform exhaustive computer-assisted verification on a carefully reduced finite instance set. The key technical contributions include a no-period-2 reduction via Lemma lem:mainrelaxed, a period-elimination induction on type, and a suite of computational methods (state-space reduction, folding, and parallel search) to certify schedulability for the finite search space. Together, these results establish the optimal density bound and demonstrate a rigorous computer-assisted approach to resolving complex combinatorial scheduling problems.

Abstract

In the covering version of the pinwheel scheduling problem, a daily task must be assigned to agents under the constraint that agent $i$ can perform the task at most once in any $a_i$-day interval. In this paper, we determine the optimal constant $α^* = 1.264\ldots {}$ such that every instance with $\sum_{i} \frac{1}{a_i} \ge α^*$ is schedulable. This resolves an open problem posed by Soejima and Kawamura (2020). Our proof combines Kawamura's (2024) techniques for the packing version with new mathematical insights, along with an exhaustive computer-aided search that draws on some ideas from Gąsieniec, Smith, and Wild (2022).

Theorems & Definitions (8)

• Theorem 1
• Theorem 2: KawamuraKaw24
• Lemma 3
• Lemma 4: Kawamura, Kobayashi, and KusanoKKK25
• Lemma 5
• Lemma 6
• proof
• proof : Proof of Theorem \ref{['thm:main']}