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.
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 clients and days,
and tests whether it is at least long, by doubling a counter held at the
length. If it is, and the fairness parameter is at most , the program writes the word of an
integer program with 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 . It then chooses a
word length for which that word fits, and runs the program that solves the integer programs of
the family (, 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 alone, and the program enumerates them. A parameter above is answered
at once when there is a client. No result is cited.