Two tests from the words up: NP-hardness of 1|r_j|L_max and Smith's rule
Lax434175.Sanity · concepts/Lax434175/Sanity.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
A test of the hardness statements end to end, on a registered result. Elffers and de Weerdt prove single-machine scheduling with release times and deadlines NP-complete when the job lengths lie in for fixed (formalized in lax-391470, on binary words). An instance with integer release times and deadlines , all shifted up by the largest absolute value among them, is an instance of with due dates the shifted deadlines, and it is feasible exactly when the maximum lateness can be made at most ; its standard word with threshold is computed from the binary word in polynomial time.
Theorem. is NP-hard on the standard reading.
A test of the algorithmic side end to end: Smith's rule. On one machine, the total weighted completion time is smallest when the jobs run without idle time in the order of (jobs of weight last). A program reads the standard word of an instance of (not a problem of the zoo's data, which leaves out problems this easy) and its threshold, sorts the jobs by comparing with , adds up the weighted completion times and compares with the threshold.
Theorem. is decided within instructions, plus the length of the word, on short words.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax434175.ZooParallel |
| 2 | import Lax434175.StandardReading |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Two tests from the words up: NP-hardness of 1|r_j|L_max and Smith's rule |
| 7 | type: theorem |
| 8 | --- |
| 9 | A test of the hardness statements end to end, on a registered result. Elffers |
| 10 | and de Weerdt prove single-machine scheduling with release times and deadlines |
| 11 | NP-complete when the job lengths lie in for fixed |
| 12 | (formalized in lax-391470, on binary words). An instance with integer release |
| 13 | times and deadlines , all shifted up by the largest absolute value |
| 14 | among them, is an instance of with due dates the shifted |
| 15 | deadlines, and it is feasible exactly when the maximum lateness can be made at |
| 16 | most ; its standard word with threshold is computed from the binary word |
| 17 | in polynomial time. |
| 18 | |
| 19 | **Theorem.** is NP-hard on the standard reading. |
| 20 | |
| 21 | A test of the algorithmic side end to end: Smith's rule. On one machine, the |
| 22 | total weighted completion time is smallest when the jobs run without idle time |
| 23 | in the order of (jobs of weight last). A program reads the |
| 24 | standard word of an instance of (not a problem of the |
| 25 | zoo's data, which leaves out problems this easy) and its threshold, sorts the |
| 26 | jobs by comparing with , adds up the weighted completion times |
| 27 | and compares with the threshold. |
| 28 | |
| 29 | **Theorem.** is decided within instructions, |
| 30 | plus the length of the word, on short words. |
| 31 | -/ |
| 32 | |
| 33 | namespace Lax434175.Sanity |
| 34 | open Lax434175 Lax434175.Results Lax434175.Assembly |
| 35 | |
| 36 | /-- `1|rj|Lmax` is NP-hard on the standard reading. -/ |
| 37 | -- zoo-result: {"problem": "1|r_j|L_{\\max}", "param": "", "claim": "is NP-hard", "note": "through lax-391470 (two job lengths), a test of the hardness statements end to end"} |
| 38 | axiom npHard_rjLmax : NPHard (StandardReading.ops.at ZooParallel.p158) |
| 39 | |
| 40 | /-- `1||ΣwjCj`, a single machine and the total weighted completion time. -/ |
| 41 | def singleWC : Spec OperationsFamily.family := |
| 42 | OperationsFamily.spec (machineCount := .atMost 1) (objective := .sumWC) |
| 43 | |
| 44 | /-- **Smith's rule**, end to end: `1||ΣwjCj` is decided within `O(n log n)` |
| 45 | instructions plus the length of the word. -/ |
| 46 | axiom smith : |
| 47 | DecidesWithin (StandardReading.ops.at singleWC) fun x => |
| 48 | (ResultParameters.Ops.n singleWC x + 1) * (Nat.log 2 (ResultParameters.Ops.n singleWC x) + 1) + |
| 49 | inputSize (StandardReading.ops.at singleWC) x |
| 50 | |
| 51 | end Lax434175.Sanity |
| 52 |
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments