While this submission is a draft, it cannot be used by other submissions.

Proof of `Structural Parameters of the Conflict Graph` (2nd statement)

groundedproofs/Lax117284Proofs/Theorem4_Clients.lean · lax-117284

What this proof establishes

no assumptions

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

  • page 5 of this submission's paper

Description

The problem is decided by a word RAM program that reads the word, with nn clients and mm days, and tests whether it is at least 2(2n2+n+3)+22 ^ (2 n² + n + 3) + 2 long, by doubling a counter held at the length. If it is, and the fairness parameter is at most mm, the program writes the word of an integer program with 2(n2+n)+n2 ^ (n² + n) + n variables: one per pair of a type of day (its conflict relation) and a set of clients, which the pair says run together on the days of that type, and one slack per client; one constraint fixes, for each type, the number of days of that type, and one says, for each client, that the days it is not served on are at most m−km - k. It then chooses a word length w′w' for which that word fits, and runs the program that solves the integer programs of the family (IlpClients.ilpClientsfptIlpClients.ilpClients_fpt, proved) on it at that word length, by an interpreter of word RAM programs written in the IMP+ language, the memory of the interpreted machine being an array of 2 ^ w' cells. The program is read as data, so it is the same for every word length. If the word is too short, the number of schedules is at most a function of nn alone, and the program enumerates them. A parameter above mm is answered nono at once when there is a client. No result is cited.