Theorem 1
Lax496464.Theorem1 · concepts/Lax496464/Theorem1.lean · lax-496464
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Just-in-time scheduling in a two-stage flexible flow shop is strongly NP-hard, already when every weight is one.
The reduction is from Hitting Set. For , the shop built from a family over admits just-in-time jobs exactly when the family has a hitting set of size .
One direction schedules: a hitting set assigns to each of its elements one machine, which runs in every epoch either the selection job of the element that hits that epoch's set or the two dummies of the element it is responsible for, and the preprocessing of those dummies fits into the epoch exactly. The other direction extracts: the preprocessing budget of an epoch admits at most dummies, so a solution of the target size holds exactly one selection job and dummies in every epoch, the element a machine is responsible for never decreases from one segment to the next, and with more than gaps between segments some gap sees no change at all — the elements of that segment hit every set.
The numbers of the constructed shop are polynomial in , and , and hence in the length of the Hitting Set instance, so the hardness is strong: no algorithm polynomial in the magnitudes of the due dates can exist unless .
Concept map
Evidence
In the paper
- page 8 of this submission's paper
Lean source view on GitHub
| 1 | import Lax496464.Construction |
| 2 | import Lax496464.NPHardness |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Theorem 1 |
| 7 | type: theorem |
| 8 | --- |
| 9 | Just-in-time scheduling in a two-stage flexible flow shop is strongly NP-hard, already |
| 10 | when every weight is one. |
| 11 | |
| 12 | The reduction is from Hitting Set. For , the shop built from a family |
| 13 | over admits just-in-time |
| 14 | jobs exactly when the family has a hitting set of size . |
| 15 | |
| 16 | One direction schedules: a hitting set assigns to each of its elements one machine, |
| 17 | which runs in every epoch either the selection job of the element that hits that epoch's |
| 18 | set or the two dummies of the element it is responsible for, and the preprocessing of |
| 19 | those dummies fits into the epoch exactly. The other direction extracts: the |
| 20 | preprocessing budget of an epoch admits at most dummies, so a solution of the |
| 21 | target size holds exactly one selection job and dummies in every epoch, the |
| 22 | element a machine is responsible for never decreases from one segment to the next, and |
| 23 | with more than gaps between segments some gap sees no change at all — the |
| 24 | elements of that segment hit every set. |
| 25 | |
| 26 | The numbers of the constructed shop are polynomial in , and , and hence in the |
| 27 | length of the Hitting Set instance, so the hardness is strong: no algorithm polynomial in |
| 28 | the magnitudes of the due dates can exist unless . |
| 29 | |
| 30 | # Formalization Notes |
| 31 | |
| 32 | Two statements, with different content and different costs. |
| 33 | |
| 34 | The first is the correctness of the construction, which is what the section proves, and |
| 35 | it is an equivalence between two combinatorial facts — no machine and no encoding occur |
| 36 | in it. It carries the hypothesis , which the problem reduced from |
| 37 | supplies, and without which the construction is false. |
| 38 | |
| 39 | The second is the hardness claim, which quantifies over every language in NP and composes |
| 40 | the construction with the NP-hardness of Hitting Set. It is stated against the classical |
| 41 | Turing-machine notion, since that is what a claim of NP-hardness means, and on the |
| 42 | unit-weight slice, because the construction lands there: the theorem is about |
| 43 | , the shop with no weights at all. |
| 44 | |
| 45 | What stands between the two is the ordinary work of a reduction: composing two |
| 46 | polynomial-time maps, and reading the composite's output size off the construction. The |
| 47 | hardness of Hitting Set itself is `HittingSetHardness`. |
| 48 | -/ |
| 49 | |
| 50 | namespace Lax496464.Theorem1 |
| 51 | |
| 52 | open Lax496464.FlowShop Lax496464.FlowShop.Instance |
| 53 | open Lax496464.HittingSet Lax496464.Construction Lax496464.NPHardness |
| 54 | |
| 55 | /-- **Theorem 1, the construction.** For `2 ≤ k ≤ n`, the constructed shop has a feasible |
| 56 | set of `R·m·(2k−1)` just-in-time jobs exactly when `P` has a hitting set of size `k`. -/ |
| 57 | axiom construct_correct (P : HittingSet.Instance) (k : ℕ) (hk : 2 ≤ k) (hkn : k ≤ P.n) : |
| 58 | Instance.HasHittingSet P k ↔ HasWeight (construct P k) (target P k) |
| 59 | |
| 60 | /-- **Theorem 1.** Just-in-time scheduling in a two-stage flexible flow shop is strongly |
| 61 | NP-hard, already on instances all of whose weights are one. -/ |
| 62 | axiom stronglyNPHard_hasWeight : |
| 63 | StronglyNPHardOn (fun I W => HasWeight I W) fun I => ∀ j : I.Job, I.w j = 1 |
| 64 | |
| 65 | end Lax496464.Theorem1 |
| 66 |
Formalization Notes
Two statements, with different content and different costs.
The first is the correctness of the construction, which is what the section proves, and it is an equivalence between two combinatorial facts — no machine and no encoding occur in it. It carries the hypothesis , which the problem reduced from supplies, and without which the construction is false.
The second is the hardness claim, which quantifies over every language in NP and composes the construction with the NP-hardness of Hitting Set. It is stated against the classical Turing-machine notion, since that is what a claim of NP-hardness means, and on the unit-weight slice, because the construction lands there: the theorem is about , the shop with no weights at all.
What stands between the two is the ordinary work of a reduction: composing two polynomial-time maps, and reading the composite's output size off the construction. The hardness of Hitting Set itself is .
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments