Scheduling with two non-unit job lengths is NP-complete
Lax391470.Theorem1 · concepts/Lax391470/Theorem1.lean · lax-391470
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Let be two integer job lengths. Single machine scheduling with release times and deadlines, restricted to instances whose processing times all lie in , is NP-complete.
Hardness is obtained by composing the reduction from satisfiability to the auxiliary problem with the reduction from the auxiliary problem to scheduling on the lengths . Since and are constants, every number of the constructed instance is bounded by a polynomial in the size of the formula, so the source concludes that the problem is even strongly NP-complete. The two bounds are stated as and ; strong NP-completeness itself, which would need a unary encoding of the instance, is not stated here.
The cases left out are polynomial-time solvable: a single job length, and two job lengths of which the shorter is .
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax391470.Lemma1 |
| 2 | import Lax391470.Lemma2 |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Scheduling with two non-unit job lengths is NP-complete |
| 7 | type: theorem |
| 8 | --- |
| 9 | Let be two integer job lengths. Single machine scheduling with release times |
| 10 | and deadlines, restricted to instances whose processing times all lie in , is |
| 11 | NP-complete. |
| 12 | |
| 13 | Hardness is obtained by composing the reduction from satisfiability to the auxiliary |
| 14 | problem with the reduction from the auxiliary problem to scheduling |
| 15 | on the lengths . Since and are constants, every number of the |
| 16 | constructed instance is bounded by a polynomial in the size of the formula, so the source |
| 17 | concludes that the problem is even strongly NP-complete. The two bounds are stated as |
| 18 | `SatConstruction.times_le` and `StackedConstruction.times_le`; strong NP-completeness |
| 19 | itself, which would need a unary encoding of the instance, is not stated here. |
| 20 | |
| 21 | The cases left out are polynomial-time solvable: a single job length, and two job |
| 22 | lengths of which the shorter is . |
| 23 | |
| 24 | # Formalization notes |
| 25 | |
| 26 | Membership in NP holds for every pair of lengths and is stated without hypotheses. A |
| 27 | certificate is a schedule with integer start times; feasibility confines every start |
| 28 | time between a release time and a deadline of the instance, so its encoding is no longer |
| 29 | than that of the instance. |
| 30 | -/ |
| 31 | |
| 32 | namespace Lax391470.Theorem1 |
| 33 | |
| 34 | open Lax391470.BinaryEncoding Lax434930.PolynomialTime |
| 35 | open Lax434930.NondeterministicPolynomialTime Lax429075.Reductions |
| 36 | |
| 37 | /-- Scheduling on the lengths `{p, q}` belongs to NP. -/ |
| 38 | axiom twoLengths_mem_NP (p q : ℕ) : TwoLengths p q ∈ NP |
| 39 | |
| 40 | /-- For job lengths `p > q > 1`, scheduling on the lengths `{p, q}` is NP-hard. -/ |
| 41 | axiom twoLengths_npHard (p q : ℕ) (hq : 1 < q) (hqp : q < p) : |
| 42 | ∀ A : Language, A ∈ NP → ManyOne A (TwoLengths p q) |
| 43 | |
| 44 | /-- **Theorem 1.** For job lengths `p > q > 1`, scheduling on the lengths `{p, q}` is |
| 45 | NP-complete. -/ |
| 46 | axiom twoLengths_npComplete (p q : ℕ) (hq : 1 < q) (hqp : q < p) : |
| 47 | NPComplete (TwoLengths p q) |
| 48 | |
| 49 | end Lax391470.Theorem1 |
| 50 |
Formalization notes
Membership in NP holds for every pair of lengths and is stated without hypotheses. A certificate is a schedule with integer start times; feasibility confines every start time between a release time and a deadline of the instance, so its encoding is no longer than that of the instance.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments