Seminarium Kombinatoryka, Teoria Grafów i Zbiorów Uporządkowanych
Wydział Matematyki i Nauk Informacyjnych, Politechnika Warszawska
Kalendarz Środy, 10:15-11:45
Pinezka Gmach MiNI PW, Sala 431, ul. Koszykowa 75, Warszawa
Komputer Seminaria odbywają się stacjonarnie z transmisją na platformie MS Teams.
Mail Jeśli chcesz dołączyć do spotkania, to napisz do sekretarza seminarium.

Najbliższy referat
04.11.2026 Grzegorz Gutowski Uniwersytet Jagielloński
A Simple Computer-Assisted Proof of the 5/6-Bound for Real-Period Pinwheel Scheduling
\(\quad\)In pinwheel scheduling with real periods, an instance consists of \(n\) tasks with real periods \(1\leq a_1\leq a_2\leq\cdots\leq a_n\). The goal is to find a schedule that assigns a task to each day in \(\mathbb{N}\) such that, for every task \(i \in \{1,\dots,n\}\) and every positive integer \(\ell\), task \(i\) occurs at least \(\ell\) times in every block of \(\lceil\ell a_i\rceil\) consecutive days. Given an instance \((a_1,a_2,\ldots,a_n)\), its dimension is \(n\), its density is \(\sum_{i=1}^n 1/a_i\), and its potential is \(\sum_{i=1}^{n-1} 1/a_i\). \(\quad\)For integer periods, a long-standing conjecture stated that every instance of density at most \(5/6\) admits a periodic schedule. Kawamura proved this conjecture using a computer-assisted proof [STOC 2024, PNAS 2026]. We extend this result to real periods while retaining the density bound of \(5/6\). Our computer-assisted proof builds on Kawamura's ideas while using fewer explicit schedules. For integer periods, Kawamura reduced the problem to checking finitely many cases. To handle real periods, we use a satisfiability modulo theories (SMT) solver for linear real arithmetic. \(\quad\)We show that the following two results in bounded dimension suffice: (i) every instance of dimension at most \(8\) and density at most \(5/6\) admits a schedule; (ii) every instance of dimension \(9\) and potential at most \(5/6\) admits a schedule. We certify both results with a set of 14397 explicit periodic schedules that includes a valid schedule for every instance in (i) or (ii). We reduce every instance of larger dimension and potential at most \(5/6\) to an instance of dimension 9 and potential at most \(5/6\). Our result confirms the real-period conjecture of Fujiwara, Miyagi, and Ouchi [DMTCS 2026] and provides a compact and computer-verifiable proof.
Zespół prowadzący