This page provides the supporting data for Lemma 5 of my paper “Proof of the Density Threshold Conjecture for Pinwheel Scheduling”, which proves the “5/6 conjecture” for pinwheel scheduling.
The lemma states that all pinwheel instances consisting of integers up to 21 and satisfying a certain modified density bound are schedulable. Let 𝓐 be the set of such instances. Instead of showing the schedulability of all 25592971 instances in 𝓐, it suffices to do so for the set 𝓑⊆𝓐 of 676224 instances that are minimal (with respect to componentwise comparison among instances of the same length) in 𝓐. Furthermore, rather than listing schedules for all instances in 𝓑, we give schedules for a set 𝓒 of 61616 instances such that each instance in 𝓑 can be transformed to one in 𝓒 (which is not necessarily in 𝓐) by applying the following operation several times: replace the two largest elements 𝑎 and 𝑏 ≤ 𝑎 by a single element 𝑏/2. This operation preserves unschedulability, and hence the lemma follows.
(4 5 5 7 7): (5 4 5 7 5 4 7)” says that the pinwheel instance (4, 5, 5, 7, 7), which means we have five tasks A, B, C, D, E with periods 4, 5, 5, 7, 7, respectively, has a valid schedule where we indefinitely repeat the 14-day sequence of tasks B, A, C, D, B, A, E, C, A, B, D, C, A, E.g++ -Wall -O3 -std=c++20 -fopenmp packing.cpp, and then run in about 45 minutes on my laptop.