Binary encoding of a scheduling instance
Lax470956.BinaryEncoding · concepts/Lax470956/BinaryEncoding.lean · lax-470956
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A scheduling instance as a binary word, the representation classical complexity measures running time against. A number is written as its binary digits preceded by its length in unary, which makes the encoding self-delimiting; an instance is the number of jobs, the number of machines, the three arrays of processing times, deadlines and weights, and the eligibility matrix, in that order.
Concept map
Lean source view on GitHub
| 1 | import Lax470956.Scheduling |
| 2 | import Lax434930.PolynomialTime |
| 3 | import Mathlib.Data.List.FinRange |
| 4 | import Mathlib.Data.Nat.Bits |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Binary encoding of a scheduling instance |
| 9 | type: definition |
| 10 | --- |
| 11 | A scheduling instance as a binary word, the representation classical complexity measures |
| 12 | running time against. A number is written as its binary digits preceded by its length in |
| 13 | unary, which makes the encoding self-delimiting; an instance is the number of jobs, the |
| 14 | number of machines, the three arrays of processing times, deadlines and weights, and the |
| 15 | eligibility matrix, in that order. |
| 16 | |
| 17 | # Formalization notes |
| 18 | |
| 19 | This encoding exists beside the word encoding of `InstanceEncoding` and does not replace |
| 20 | it. They answer different questions. A word RAM is handed numbers and charges one |
| 21 | instruction per operation on them, so its input is a list of numbers and its running time |
| 22 | is measured in their count; a Turing machine is handed bits, so a claim of polynomial |
| 23 | time is a claim about the number of bits. The two statements of this submission that |
| 24 | quantify over all of NP are Turing-machine statements and use this encoding; the |
| 25 | fixed-parameter statement is a word RAM statement and uses the other. |
| 26 | |
| 27 | Numbers are written in binary rather than unary. The difference is not cosmetic for a |
| 28 | hardness claim: under a unary encoding the input is exponentially longer, which makes a |
| 29 | polynomial-time reduction easier to achieve and the resulting hardness claim |
| 30 | correspondingly weaker — it would be a claim of *strong* NP-hardness only. Binary is |
| 31 | what the unqualified statement means. |
| 32 | |
| 33 | The eligibility matrix is written in full, one bit per job-machine pair, rather than as |
| 34 | adjacency lists. At bits it is within a polynomial of any other reasonable choice, |
| 35 | and polynomial time is invariant under polynomial changes of encoding; the matrix is the |
| 36 | simpler object and matches the encoding of a graph elsewhere in the archive. |
| 37 | |
| 38 | The encoding need not be injective on instances that differ only in inaccessible data, |
| 39 | and nothing here claims it is. What the statements need is that it is computable in |
| 40 | polynomial time and that the reduction's image is determined, both of which are |
| 41 | obligations of the proof layer. |
| 42 | -/ |
| 43 | |
| 44 | namespace Lax470956.BinaryEncoding |
| 45 | |
| 46 | open Lax470956.Scheduling Lax434930.PolynomialTime |
| 47 | |
| 48 | /-- A natural number as a binary word: its digits, least significant first, preceded by |
| 49 | their number in unary. The unary prefix makes the code self-delimiting. -/ |
| 50 | def encodeNat (n : ℕ) : Word := |
| 51 | List.replicate n.bits.length true ++ [false] ++ n.bits |
| 52 | |
| 53 | /-- An instance as a binary word: the two counts, the processing times, the deadlines, |
| 54 | the weights, and the eligibility matrix in row order. -/ |
| 55 | def encodeInstance (I : Instance) : Word := |
| 56 | encodeNat I.jobs ++ encodeNat I.machines ++ |
| 57 | (List.finRange I.jobs).flatMap (fun j => encodeNat (I.p j)) ++ |
| 58 | (List.finRange I.jobs).flatMap (fun j => encodeNat (I.d j)) ++ |
| 59 | (List.finRange I.jobs).flatMap (fun j => encodeNat (I.w j)) ++ |
| 60 | (List.finRange I.jobs).flatMap |
| 61 | (fun j => (List.finRange I.machines).map fun i => decide (i ∈ I.eligible j)) |
| 62 | |
| 63 | end Lax470956.BinaryEncoding |
| 64 |
Formalization notes
This encoding exists beside the word encoding of and does not replace it. They answer different questions. A word RAM is handed numbers and charges one instruction per operation on them, so its input is a list of numbers and its running time is measured in their count; a Turing machine is handed bits, so a claim of polynomial time is a claim about the number of bits. The two statements of this submission that quantify over all of NP are Turing-machine statements and use this encoding; the fixed-parameter statement is a word RAM statement and uses the other.
Numbers are written in binary rather than unary. The difference is not cosmetic for a hardness claim: under a unary encoding the input is exponentially longer, which makes a polynomial-time reduction easier to achieve and the resulting hardness claim correspondingly weaker — it would be a claim of strong NP-hardness only. Binary is what the unqualified statement means.
The eligibility matrix is written in full, one bit per job-machine pair, rather than as adjacency lists. At bits it is within a polynomial of any other reasonable choice, and polynomial time is invariant under polynomial changes of encoding; the matrix is the simpler object and matches the encoding of a graph elsewhere in the archive.
The encoding need not be injective on instances that differ only in inaccessible data, and nothing here claims it is. What the statements need is that it is computable in polynomial time and that the reduction's image is determined, both of which are obligations of the proof layer.
Used by
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments