Proof of `Day-Independent Due Dates` (1st statement)
groundedproofs/Lax117284Proofs/Theorem3_Colouring.lean · lax-117284
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The language is decided by a reduction to 2-satisfiability, which is in polynomial time, that carries out the decision itself and writes a formula with no clause for a yes-instance and an unsatisfiable formula for every other word. A word RAM program reads the instance and the parameter, checks that every job takes some time and is not due before it starts, checks that every day repeats the table of the first, counts for every client of the first day the jobs that run at the instant its job starts — the clique number of the interval graph of the day, which is its chromatic number — takes the largest of the counts, and compares the parameter times that count with the number of days. An instance without days is a yes-instance exactly when the parameter is zero or there is no client. The program runs in time quadratic in the length of the input.