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

Proof of `Just-in-Time Scheduling on Unrelated Parallel Machines`

groundedproofs/Lax117284Proofs/JitHard/Final.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.

Read the Lean proof on GitHub

Description

Deciding whether every job of an instance of R∣∣∑jZjR || ∑_j Z_j can be just in time is NP-hard. Every language in NP reduces to interval scheduling with eligible machine sets, by the second theorem of lax−470956lax-470956, and that problem reduces to this one: every job is given the due date dj+1d_j + 1 and the processing time it has, and on a machine it may not use, the processing time dj+1d_j + 1, so that it covers the time point 11, which one extra job per machine, due at 11 and of length 11 on every machine, occupies. Those extra jobs overlap one another and so sit on distinct machines, hence on all of them, and a job that sits on a machine it may not use would overlap the extra job of that machine. The map is computed by a word RAM program, which is polynomial in the length of the code, since the extra jobs are only added when there is a job, and then there are as many machines as the matrix of the input has columns.