Density threshold in pinwheel scheduling, covering version

This page provides the supporting data for Lemma 5 of our paper “A Computer-Assisted Proof of the Optimal Density Bound for Pinwheel Covering”.

The lemma states that all pinwheel covering instances consisting of integers 3, 4, …, 20 and satisfying a certain modified density bound are schedulable. Let 𝓐 be the set of such instances. Let 𝓑 be the finite subset of 𝓐 consisting of instances that are inclusion-minimal and do not contain 10. It suffices to check the schedulability of all instances in 𝓑.

Rather than listing schedules for all 25242331 instances in 𝓑, we give schedules for a set 𝓒 of 11687 instances such that each instance in 𝓑 can be transformed to an instance in 𝓒 (which is not necessarily in 𝓑) by applying the following operation several times: replace the two largest elements 𝑎 and 𝑏 ≤ 𝑎 by a single element max{𝑎/2, 𝑏}. This operation preserves unschedulability, and hence the lemma follows.

This file lists the instances in 𝓒 and their schedules. Each line consists of an instance, followed by a colon and then a finite sequence [𝑠₁ … 𝑠_𝑚] of periods. This means that the instance is satisfied by a cyclic schedule where agents with periods 𝑠₁, …, 𝑠_𝑚 work in order. Multiple agents with the same period work in a round-robin fashion. For example, the line “(3 5 5 5 7): [5 3 5 7 5 3 5]” says that the pinwheel instance (3, 5, 5, 5, 7), which means we have an agent A with period 3, three agents B, C, D with period 5, and an agent E with period 7, has a valid schedule where we indefinitely repeat the 21-day sequence of agents B, A, C, E, D, A, B, C, A, D, E, B, A, C, D, A, B, E, C, A, D.
This is the C++ program that generated the list. It can be compiled by g++ -Wall -O3 -std=c++20 -fopenmp covering.cpp, and then run in about 25 minutes on my laptop.