An Optimal Density Bound for Discretized Point Patrolling

This repository contains three independent folders representing different results.

dppatrolling (Theorem 3.5): Supporting content for an algorithm that achieves a state-of-the-art (until Theorem 4.7) $\frac{13}{10}$ bound for the discretized point patrolling problem.

dppatrolling_opt (Theorem 4.7): Supporting content for an algorithm that achieves a state-of-the-art and also provably optimal $\sum_{i = 0}^{\infty} \frac{1}{2^i + 1} \approx 1.264$ bound for the discretized point patrolling problem.

bamboogt (Theorem 5.4): Supporting content for an algorithm that achieves a state of the art $\frac{9}{7}$ bound for the bamboo garden trimming problem.

To explore each result, and particularly run certifiers and full surface generators, first navigate to the folder (e.g. cd bamboogt). Then, each folder has a corresponding README.md file for direction.

File Structure

Each case or subcase in this repository is composed of the following four files:

1. lists.csv

2. lists-processed.csv

3. schedules.txt

4. reductions.txt

These files form a basic unit together. This structure for demonstrating the schedulability of a large class of instances is taken from Kawamura's content resolving the long-standing $\frac{5}{6}$ conjecture in pinwheel scheduling.

The files can be interpreted in the following way:

The overall goal is to find a schedule for every list in lists.csv.

To achieve this goal, we first find schedules for particular hard instances, specifically those in lists-processed.csv, which we give explicit schedules for in schedules.txt.

Then, we show that the schedulability of these instances implies schedulability of the lists in lists.csv.

In particular, through repeated applications of the monotonicity principle, if we have two lists $L_1$ and $L_2$ of the same length with the elements of $L_2$ being at most (or at least, in the case of bamboo garden trimming) the corresponding element in $L_1$, then the schedulability of $L_1$ implies the schedulability of $L_2$. In the same way, as discussed in the text, if for any $\theta$, $L_1 = \text{fold}(L_2, \theta)$ (for any of our fold operations), the schedulability of $L_1$ implies the schedulability of $L_2$.

These corresponding relations between the elements of lists-processed.csv and lists.csv are recorded in reductions.txt.