The auxiliary problem is NP-complete
Lax391470.Lemma2 · concepts/Lax391470/Lemma2.lean · lax-391470
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
For any two integer job lengths , the problem is NP-complete.
Hardness is by reduction from satisfiability of formulas in conjunctive normal form. A satisfying assignment yields a solution in which the sections of the false literals are delayed by one unit: every clause has a true literal, whose section is not delayed and whose clause block is active, and at that block the chain of connected pairs of the clause can switch from completing short jobs early to completing long jobs early. Conversely, in any solution every job runs inside its own block, one of the sections of and is delayed for every , and a chain of clause blocks can be scheduled only if it passes an active block in a section that is not delayed; setting the literals of the delayed sections to false satisfies the formula.
The assumption is needed: one unit of delay must not leave room for a short job.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax391470.BinaryEncoding |
| 2 | import Lax391470.SatConstruction |
| 3 | import Lax429075.Reductions |
| 4 | import Lax429075.Satisfiability |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: The auxiliary problem is NP-complete |
| 9 | type: theorem |
| 10 | --- |
| 11 | For any two integer job lengths , the problem is |
| 12 | NP-complete. |
| 13 | |
| 14 | Hardness is by reduction from satisfiability of formulas in conjunctive normal form. A |
| 15 | satisfying assignment yields a solution in which the sections of the false literals are |
| 16 | delayed by one unit: every clause has a true literal, whose section is not delayed and |
| 17 | whose clause block is active, and at that block the chain of connected pairs of the |
| 18 | clause can switch from completing short jobs early to completing long jobs early. |
| 19 | Conversely, in any solution every job runs inside its own block, one of the sections of |
| 20 | and is delayed for every , and a chain of clause blocks can be |
| 21 | scheduled only if it passes an active block in a section that is not delayed; setting |
| 22 | the literals of the delayed sections to false satisfies the formula. |
| 23 | |
| 24 | The assumption is needed: one unit of delay must not leave room for a short job. |
| 25 | |
| 26 | # Formalization notes |
| 27 | |
| 28 | A reduction is a function on all words. A word that does not encode a formula is sent to |
| 29 | the encoding of a fixed instance without a solution: a single ordinary short job that is |
| 30 | due at time . |
| 31 | |
| 32 | The statements separate what is asserted. The first two concern one map on words: that |
| 33 | it preserves and reflects membership, and that a Turing machine computes it in |
| 34 | polynomial time. NP-hardness follows from them and the Cook–Levin theorem, which the |
| 35 | archive proves. Membership in NP is a further statement, and NP-completeness is the |
| 36 | conjunction. |
| 37 | -/ |
| 38 | |
| 39 | namespace Lax391470.Lemma2 |
| 40 | |
| 41 | open Lax391470.BinaryEncoding Lax434930.PolynomialTime |
| 42 | open Lax434930.NondeterministicPolynomialTime Lax429075.Reductions |
| 43 | |
| 44 | /-- An instance of the auxiliary problem without a solution, when `q ≥ 1`: one ordinary |
| 45 | short job, released and due at time `0`. -/ |
| 46 | def blocked : AuxiliaryProblem.Instance where |
| 47 | ordinary := 1 |
| 48 | r _ := 0 |
| 49 | d _ := 0 |
| 50 | long _ := false |
| 51 | pairs := 0 |
| 52 | longEarly := Fin.elim0 |
| 53 | longDue := Fin.elim0 |
| 54 | shortEarly := Fin.elim0 |
| 55 | shortDue := Fin.elim0 |
| 56 | |
| 57 | /-- **The reduction**, as a map on words: the encoding of a formula is sent to the |
| 58 | encoding of the instance built from it, and every other word to the encoding of |
| 59 | `blocked`. -/ |
| 60 | def reduce (p q : ℕ) (w : Word) : Word := |
| 61 | match Lax429075.Encoding.decodeCNF w with |
| 62 | | some F => encodeAux (SatConstruction.inst p q F) |
| 63 | | none => encodeAux blocked |
| 64 | |
| 65 | /-- **The reduction is correct.** -/ |
| 66 | axiom reduce_correct (p q : ℕ) (hq : 1 < q) (hqp : q < p) (w : Word) : |
| 67 | w ∈ Lax429075.Satisfiability.SAT ↔ reduce p q w ∈ AUX p q |
| 68 | |
| 69 | /-- **The reduction runs in polynomial time.** -/ |
| 70 | axiom reduce_polyTime (p q : ℕ) : |
| 71 | Nonempty (Turing.TM2ComputableInPolyTime id id (reduce p q)) |
| 72 | |
| 73 | /-- For job lengths `p > q > 1`, `AUX(p, q)` is NP-hard. -/ |
| 74 | axiom aux_npHard (p q : ℕ) (hq : 1 < q) (hqp : q < p) : |
| 75 | ∀ A : Language, A ∈ NP → ManyOne A (AUX p q) |
| 76 | |
| 77 | /-- `AUX(p, q)` belongs to NP. -/ |
| 78 | axiom aux_mem_NP (p q : ℕ) : AUX p q ∈ NP |
| 79 | |
| 80 | /-- **Lemma 2.** For job lengths `p > q > 1`, `AUX(p, q)` is NP-complete. -/ |
| 81 | axiom aux_npComplete (p q : ℕ) (hq : 1 < q) (hqp : q < p) : NPComplete (AUX p q) |
| 82 | |
| 83 | end Lax391470.Lemma2 |
| 84 |
Formalization notes
A reduction is a function on all words. A word that does not encode a formula is sent to the encoding of a fixed instance without a solution: a single ordinary short job that is due at time .
The statements separate what is asserted. The first two concern one map on words: that it preserves and reflects membership, and that a Turing machine computes it in polynomial time. NP-hardness follows from them and the Cook–Levin theorem, which the archive proves. Membership in NP is a further statement, and NP-completeness is the conjunction.
Builds on
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