Binary encodings and the two languages
Lax391470.BinaryEncoding · concepts/Lax391470/BinaryEncoding.lean · lax-391470
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
Scheduling instances and instances of the auxiliary problem as binary words, the representation against which classical complexity measures running time, and the two decision problems of this submission as languages of such words.
A natural number is written as its binary digits preceded by their number in unary, which makes the code self-delimiting; an integer is a sign bit followed by its absolute value. A scheduling instance is the number of jobs followed by the release time, the deadline and the processing time of every job in turn. An instance of the auxiliary problem is the number of ordinary jobs, the number of connected pairs, then for every ordinary job its release time, its deadline and one bit telling whether it is long, then for every connected pair its four deadlines.
For fixed job lengths and , the language of scheduling on the lengths consists of the encodings of the instances on those lengths that have a feasible schedule, and the language consists of the encodings of the ordered instances of the auxiliary problem that have a solution at those lengths.
Concept map
Lean source view on GitHub
| 1 | import Lax391470.AuxiliaryProblem |
| 2 | import Lax434930.PolynomialTime |
| 3 | import Mathlib.Data.List.FinRange |
| 4 | import Mathlib.Data.Nat.Bits |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Binary encodings and the two languages |
| 9 | type: definition |
| 10 | --- |
| 11 | Scheduling instances and instances of the auxiliary problem as binary words, the |
| 12 | representation against which classical complexity measures running time, and the two |
| 13 | decision problems of this submission as languages of such words. |
| 14 | |
| 15 | A natural number is written as its binary digits preceded by their number in unary, |
| 16 | which makes the code self-delimiting; an integer is a sign bit followed by its absolute |
| 17 | value. A scheduling instance is the number of jobs followed by the release time, the |
| 18 | deadline and the processing time of every job in turn. An instance of the auxiliary |
| 19 | problem is the number of ordinary jobs, the number of connected pairs, then for every |
| 20 | ordinary job its release time, its deadline and one bit telling whether it is long, then |
| 21 | for every connected pair its four deadlines. |
| 22 | |
| 23 | For fixed job lengths and , the language of *scheduling on the lengths |
| 24 | * consists of the encodings of the instances on those lengths that have a |
| 25 | feasible schedule, and the language consists of the encodings of the |
| 26 | ordered instances of the auxiliary problem that have a solution at those lengths. |
| 27 | |
| 28 | # Formalization notes |
| 29 | |
| 30 | Numbers are written in binary, the usual convention, under which NP-hardness is the |
| 31 | usual claim. Hardness under a unary encoding of the scheduling instance would be the |
| 32 | stronger claim, strong NP-hardness: the reduction would then have to produce numbers |
| 33 | bounded by a polynomial in its input, since a unary word must stay polynomially long. That |
| 34 | this reduction does produce such numbers, which is what the source's claim of strong |
| 35 | NP-completeness rests on, is recorded separately. |
| 36 | |
| 37 | The job lengths and are parameters of the language and not part of the input: |
| 38 | the theorem is about every fixed pair of lengths. A word that encodes no instance, or an |
| 39 | instance with a processing time outside , or an instance of the auxiliary |
| 40 | problem whose deadlines are not ordered, belongs to neither language. |
| 41 | -/ |
| 42 | |
| 43 | namespace Lax391470.BinaryEncoding |
| 44 | |
| 45 | open Lax434930.PolynomialTime |
| 46 | |
| 47 | /-- A natural number as a binary word: its digits, least significant first, preceded by |
| 48 | their number in unary. -/ |
| 49 | def encodeNat (n : ℕ) : Word := |
| 50 | List.replicate n.bits.length true ++ [false] ++ n.bits |
| 51 | |
| 52 | /-- An integer as a binary word: one bit for the sign, then the absolute value. -/ |
| 53 | def encodeInt (z : ℤ) : Word := decide (z < 0) :: encodeNat z.natAbs |
| 54 | |
| 55 | /-- A scheduling instance as a binary word. -/ |
| 56 | def encodeInstance (I : Scheduling.Instance) : Word := |
| 57 | encodeNat I.jobs ++ |
| 58 | (List.finRange I.jobs).flatMap fun j => |
| 59 | encodeInt (I.r j) ++ encodeInt (I.d j) ++ encodeNat (I.p j) |
| 60 | |
| 61 | /-- An instance of the auxiliary problem as a binary word. -/ |
| 62 | def encodeAux (A : AuxiliaryProblem.Instance) : Word := |
| 63 | encodeNat A.ordinary ++ encodeNat A.pairs ++ |
| 64 | ((List.finRange A.ordinary).flatMap fun o => |
| 65 | encodeNat (A.r o) ++ encodeNat (A.d o) ++ [A.long o]) ++ |
| 66 | (List.finRange A.pairs).flatMap fun i => |
| 67 | encodeNat (A.longEarly i) ++ encodeNat (A.longDue i) ++ |
| 68 | encodeNat (A.shortEarly i) ++ encodeNat (A.shortDue i) |
| 69 | |
| 70 | /-- **Scheduling on the lengths `{p, q}`**, as a language. -/ |
| 71 | def TwoLengths (p q : ℕ) : Language := |
| 72 | {w | ∃ I : Scheduling.Instance, encodeInstance I = w ∧ I.LengthsIn p q ∧ I.Schedulable} |
| 73 | |
| 74 | /-- **The auxiliary problem `AUX(p, q)`**, as a language. -/ |
| 75 | def AUX (p q : ℕ) : Language := |
| 76 | {w | ∃ A : AuxiliaryProblem.Instance, encodeAux A = w ∧ A.Ordered ∧ A.Solvable p q} |
| 77 | |
| 78 | end Lax391470.BinaryEncoding |
| 79 |
Formalization notes
Numbers are written in binary, the usual convention, under which NP-hardness is the usual claim. Hardness under a unary encoding of the scheduling instance would be the stronger claim, strong NP-hardness: the reduction would then have to produce numbers bounded by a polynomial in its input, since a unary word must stay polynomially long. That this reduction does produce such numbers, which is what the source's claim of strong NP-completeness rests on, is recorded separately.
The job lengths and are parameters of the language and not part of the input: the theorem is about every fixed pair of lengths. A word that encodes no instance, or an instance with a processing time outside , or an instance of the auxiliary problem whose deadlines are not ordered, belongs to neither language.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments