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

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 ${\alpha }^{\ast }=1.264\dots$ such that every instance with ${\sum }_{i}1/a_i\ge {\alpha }^{\ast }$ is schedulable. This resolves an open problem posed by Kawamura and Soejima (2020). Our proof combines Kawamura's (2026) techniques for the packing version with new mathematical insights to reduce the analysis to a finite set of instances, which are then verified through an exhaustive computer-aided search that draws on ideas from Gąsieniec, Smith, and Wild (2022). The same result was obtained independently by Mishra (2026).

A conference version will appear in ESA 2026