Binary Encoding of an Instance
Lax496464.BinaryEncoding · concepts/Lax496464/BinaryEncoding.lean · lax-496464
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance as a binary word, the representation against which classical complexity measures running time. A number is written as its binary digits preceded by their number in unary, which makes the encoding self-delimiting; an instance is the number of jobs, the number of machines, and then the four arrays of preprocessing times, processing times, due dates and weights, in that order.
Concept map
In the paper
- page 2 of this submission's paper
Lean source view on GitHub
| 1 | import Lax496464.FlowShop |
| 2 | import Lax434930.PolynomialTime |
| 3 | import Mathlib.Data.List.FinRange |
| 4 | import Mathlib.Data.Nat.Bits |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Binary Encoding of an Instance |
| 9 | type: definition |
| 10 | --- |
| 11 | An instance as a binary word, the representation against which classical complexity |
| 12 | measures running time. A number is written as its binary digits preceded by their number |
| 13 | in unary, which makes the encoding self-delimiting; an instance is the number of jobs, |
| 14 | the number of machines, and then the four arrays of preprocessing times, processing |
| 15 | times, due dates and weights, in that order. |
| 16 | |
| 17 | # Formalization Notes |
| 18 | |
| 19 | This encoding exists beside the word encoding and does not replace it. The two answer |
| 20 | different questions. A word RAM is handed numbers and charges one instruction per |
| 21 | operation on them, so its input is a list of numbers and its running time is counted in |
| 22 | their number; a Turing machine is handed bits, so a claim of polynomial time there is a |
| 23 | claim about a number of bits. The statement that quantifies over all of NP is a |
| 24 | Turing-machine statement and uses this encoding. |
| 25 | |
| 26 | Numbers are written in binary rather than in unary. The difference is not cosmetic for a |
| 27 | hardness claim: under a unary encoding the input is exponentially longer, a |
| 28 | polynomial-time reduction correspondingly easier to achieve, and the resulting claim |
| 29 | weaker. Binary is what an unqualified claim of NP-hardness means, and the extra clause |
| 30 | that makes a claim of *strong* NP-hardness is stated separately, as a bound on the |
| 31 | numbers a reduction emits, rather than by changing the encoding under it. |
| 32 | |
| 33 | The encoding need not be injective on instances that differ only in inaccessible data, |
| 34 | and nothing here claims it is. What the statements need is that it is computable in |
| 35 | polynomial time and that a reduction's image is determined, both obligations of the proof |
| 36 | layer. |
| 37 | -/ |
| 38 | |
| 39 | namespace Lax496464.BinaryEncoding |
| 40 | |
| 41 | open Lax496464.FlowShop Lax496464.FlowShop.Instance Lax434930.PolynomialTime |
| 42 | |
| 43 | /-- A natural number as a binary word: its digits, least significant first, preceded by |
| 44 | their number in unary. The unary prefix makes the code self-delimiting. -/ |
| 45 | def encodeNat (n : ℕ) : Word := |
| 46 | List.replicate n.bits.length true ++ [false] ++ n.bits |
| 47 | |
| 48 | /-- An instance as a binary word: the two counts, then the preprocessing times, the |
| 49 | processing times, the due dates and the weights. -/ |
| 50 | def encodeInstance (I : Instance) : Word := |
| 51 | encodeNat I.jobs ++ encodeNat I.machines ++ |
| 52 | (List.finRange I.jobs).flatMap (fun j => encodeNat (I.p j)) ++ |
| 53 | (List.finRange I.jobs).flatMap (fun j => encodeNat (I.q j)) ++ |
| 54 | (List.finRange I.jobs).flatMap (fun j => encodeNat (I.d j)) ++ |
| 55 | (List.finRange I.jobs).flatMap (fun j => encodeNat (I.w j)) |
| 56 | |
| 57 | /-- An instance together with a threshold, as a binary word. -/ |
| 58 | def encodeDecisionInstance (I : Instance) (W : ℕ) : Word := |
| 59 | encodeInstance I ++ encodeNat W |
| 60 | |
| 61 | /-- The largest number appearing in an instance. A reduction witnesses *strong* |
| 62 | NP-hardness when this stays polynomial in the length of its input. -/ |
| 63 | def maxNumber (I : Instance) : ℕ := |
| 64 | ((List.finRange I.jobs).map fun j => |
| 65 | max (max (I.p j) (I.q j)) (max (I.d j) (I.w j))).foldr max (max I.jobs I.machines) |
| 66 | |
| 67 | end Lax496464.BinaryEncoding |
| 68 |
Formalization Notes
This encoding exists beside the word encoding and does not replace it. The two 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 counted in their number; a Turing machine is handed bits, so a claim of polynomial time there is a claim about a number of bits. The statement that quantifies over all of NP is a Turing-machine statement and uses this encoding.
Numbers are written in binary rather than in unary. The difference is not cosmetic for a hardness claim: under a unary encoding the input is exponentially longer, a polynomial-time reduction correspondingly easier to achieve, and the resulting claim weaker. Binary is what an unqualified claim of NP-hardness means, and the extra clause that makes a claim of strong NP-hardness is stated separately, as a bound on the numbers a reduction emits, rather than by changing the encoding under it.
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 a reduction's image is determined, both 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