0-1 integer programming
Lax799700.ZeroOneIP · concepts/Lax799700/ZeroOneIP.lean · lax-799700
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
0-1 INTEGER PROGRAMMING: given a matrix and a vector , is there a 0-1 vector with ? It is the multi-row form of Knapsack and is written in binary like it. The vocabulary carries the columns, the rows, the bit positions, the bits of each coefficient (the catalog's one ternary symbol), the bits of each right-hand side, and a linear order fixing the place values. Entries are natural numbers: Karp states the problem over the integers, and this restriction is the one his reduction produces, so its NP-hardness gives his problem's a fortiori. Membership is by an existential second-order definition, hardness by an ordered first-order reduction from Knapsack.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Mathlib.Algebra.BigOperators.Finprod |
| 2 | import Mathlib.ModelTheory.Semantics |
| 3 | import Mathlib.ModelTheory.Complexity |
| 4 | import Mathlib.Tactic.FinCases |
| 5 | import Mathlib.Data.Set.Finite.Lemmas |
| 6 | import Mathlib.Data.Fintype.EquivFin |
| 7 | import Mathlib.Data.Set.Card |
| 8 | import Mathlib.SetTheory.Cardinal.Finite |
| 9 | import Mathlib.Logic.Equiv.Prod |
| 10 | import Mathlib.ModelTheory.Syntax |
| 11 | import Lax799700.Common |
| 12 | import Lax904597.Machines |
| 13 | import Lax904597.Classes |
| 14 | import Lax799700.Problems |
| 15 | |
| 16 | /-! |
| 17 | --- |
| 18 | title: 0-1 integer programming |
| 19 | type: theorem |
| 20 | --- |
| 21 | 0-1 INTEGER PROGRAMMING: given a matrix and a vector , is there a |
| 22 | 0-1 vector with ? It is the multi-row form of Knapsack and is |
| 23 | written in binary like it. The vocabulary carries the columns, the rows, |
| 24 | the bit positions, the bits of each coefficient (the catalog's one |
| 25 | ternary symbol), the bits of each right-hand side, and a linear order |
| 26 | fixing the place values. Entries are natural numbers: Karp states the |
| 27 | problem over the integers, and this restriction is the one his reduction |
| 28 | produces, so its NP-hardness gives his problem's a fortiori. Membership |
| 29 | is by an existential second-order definition, hardness by an ordered |
| 30 | first-order reduction from Knapsack. |
| 31 | |
| 32 | -/ |
| 33 | |
| 34 | namespace Lax799700.ZeroOneIP |
| 35 | |
| 36 | open Lax799700.Common Lax904597.Machines |
| 37 | |
| 38 | open FirstOrder |
| 39 | |
| 40 | open FirstOrder.Language |
| 41 | |
| 42 | /-- The relation symbols of the language. -/ |
| 43 | inductive zeroOneIPRel : ℕ → Type where |
| 44 | /-- `col j`: `j` is a column, that is, a `0-1` variable. -/ |
| 45 | | col : zeroOneIPRel 1 |
| 46 | /-- `row r`: `r` is a row, that is, an equation. -/ |
| 47 | | row : zeroOneIPRel 1 |
| 48 | /-- `posn p`: `p` is a bit position. -/ |
| 49 | | posn : zeroOneIPRel 1 |
| 50 | /-- `coef r j p`: the entry of row `r` in column `j` has bit 1 at `p`. -/ |
| 51 | | coef : zeroOneIPRel 3 |
| 52 | /-- `rhs r p`: the right-hand side of row `r` has bit 1 at `p`. -/ |
| 53 | | rhs : zeroOneIPRel 2 |
| 54 | /-- `le a b`: the linear order carrying the place values. -/ |
| 55 | | le : zeroOneIPRel 2 |
| 56 | deriving DecidableEq |
| 57 | |
| 58 | /-- The relational language of 0-1 integer programs: columns, rows and bit |
| 59 | positions, the bits of each entry and of each right-hand side, and a linear |
| 60 | order. -/ |
| 61 | def zeroOneIP : FirstOrder.Language := |
| 62 | ⟨fun _ => Empty, zeroOneIPRel⟩ |
| 63 | |
| 64 | instance instIsRelationalZeroOneIP : FirstOrder.Language.IsRelational zeroOneIP := fun _ => |
| 65 | (inferInstance : IsEmpty Empty) |
| 66 | |
| 67 | /-- `col j`: `j` is a column, that is, a `0-1` variable. -/ |
| 68 | abbrev ipCol : zeroOneIP.Relations 1 := |
| 69 | .col |
| 70 | |
| 71 | /-- `row r`: `r` is a row, that is, an equation. -/ |
| 72 | abbrev ipRow : zeroOneIP.Relations 1 := |
| 73 | .row |
| 74 | |
| 75 | /-- `posn p`: `p` is a bit position. -/ |
| 76 | abbrev ipPosn : zeroOneIP.Relations 1 := |
| 77 | .posn |
| 78 | |
| 79 | /-- `coef r j p`: the entry of row `r` in column `j` has bit 1 at `p`. -/ |
| 80 | abbrev ipCoef : zeroOneIP.Relations 3 := |
| 81 | .coef |
| 82 | |
| 83 | /-- `rhs r p`: the right-hand side of row `r` has bit 1 at `p`. -/ |
| 84 | abbrev ipRhs : zeroOneIP.Relations 2 := |
| 85 | .rhs |
| 86 | |
| 87 | /-- `le a b`: the linear order carrying the place values. -/ |
| 88 | abbrev ipLe : zeroOneIP.Relations 2 := |
| 89 | .le |
| 90 | |
| 91 | open FirstOrder |
| 92 | |
| 93 | open Language Structure |
| 94 | |
| 95 | section Shorthands |
| 96 | |
| 97 | variable {A : Type} [zeroOneIP.Structure A] |
| 98 | |
| 99 | /-- `col j`: `j` is a column, that is, a `0-1` variable. -/ |
| 100 | def IPCol {A : Type} [zeroOneIP.Structure A] (a0 : A) : Prop := |
| 101 | FirstOrder.Language.Structure.RelMap ipCol ![a0] |
| 102 | |
| 103 | /-- `row r`: `r` is a row, that is, an equation. -/ |
| 104 | def IPRow {A : Type} [zeroOneIP.Structure A] (a0 : A) : Prop := |
| 105 | FirstOrder.Language.Structure.RelMap ipRow ![a0] |
| 106 | |
| 107 | /-- `posn p`: `p` is a bit position. -/ |
| 108 | def IPPosn {A : Type} [zeroOneIP.Structure A] (a0 : A) : Prop := |
| 109 | FirstOrder.Language.Structure.RelMap ipPosn ![a0] |
| 110 | |
| 111 | /-- `coef r j p`: the entry of row `r` in column `j` has bit 1 at `p`. -/ |
| 112 | def IPCoef {A : Type} [zeroOneIP.Structure A] (a0 : A) (a1 : A) (a2 : A) : Prop := |
| 113 | FirstOrder.Language.Structure.RelMap ipCoef ![a0, a1, a2] |
| 114 | |
| 115 | /-- `rhs r p`: the right-hand side of row `r` has bit 1 at `p`. -/ |
| 116 | def IPRhs {A : Type} [zeroOneIP.Structure A] (a0 : A) (a1 : A) : Prop := |
| 117 | FirstOrder.Language.Structure.RelMap ipRhs ![a0, a1] |
| 118 | |
| 119 | /-- `le a b`: the linear order carrying the place values. -/ |
| 120 | def IPLe {A : Type} [zeroOneIP.Structure A] (a0 : A) (a1 : A) : Prop := |
| 121 | FirstOrder.Language.Structure.RelMap ipLe ![a0, a1] |
| 122 | |
| 123 | /-- The entry of a row in a column, decoded. -/ |
| 124 | noncomputable def IPCoefVal (r j : A) : ℕ := binNum IPLe IPPosn (IPCoef r j) |
| 125 | |
| 126 | /-- The right-hand side of a row, decoded. -/ |
| 127 | noncomputable def IPRhsVal (r : A) : ℕ := binNum IPLe IPPosn (IPRhs r) |
| 128 | |
| 129 | end Shorthands |
| 130 | |
| 131 | section Problem |
| 132 | |
| 133 | variable (A : Type) [zeroOneIP.Structure A] |
| 134 | |
| 135 | /-- A 0-1 integer program is a yes-instance when its order is a linear order |
| 136 | and some set of columns – the variables set to `1` – makes every equation |
| 137 | hold. -/ |
| 138 | def HasZeroOneSolution : Prop := |
| 139 | Finite A ∧ IsLinOrd (IPLe (A := A)) ∧ |
| 140 | ∃ x : A → Prop, (∀ j, x j → IPCol j) ∧ |
| 141 | ∀ r, IPRow r → (∑ᶠ j ∈ {j | x j}, IPCoefVal r j) = IPRhsVal r |
| 142 | |
| 143 | end Problem |
| 144 | |
| 145 | open Lax904597.Problems Lax904597.Classes Lax799700.Problems |
| 146 | |
| 147 | /-- The property `HasZeroOneSolution` is isomorphism-invariant. -/ |
| 148 | axiom hasZeroOneSolution_iso : ∀ {A B : Type} [Lax799700.ZeroOneIP.zeroOneIP.Structure A] [Lax799700.ZeroOneIP.zeroOneIP.Structure B], |
| 149 | (A ≃[Lax799700.ZeroOneIP.zeroOneIP] B) → (HasZeroOneSolution A ↔ HasZeroOneSolution B) |
| 150 | |
| 151 | /-- The problem ZeroOneIP: does the structure satisfy `HasZeroOneSolution`? -/ |
| 152 | def ZeroOneIP : DecisionProblem Lax799700.ZeroOneIP.zeroOneIP := |
| 153 | DecisionProblem.ofPred HasZeroOneSolution |
| 154 | |
| 155 | /-- The yes-instances of ZeroOneIP are exactly the structures satisfying |
| 156 | `HasZeroOneSolution`. -/ |
| 157 | axiom zeroOneIP_iff : ∀ (A : Type) [Lax799700.ZeroOneIP.zeroOneIP.Structure A], ZeroOneIP A ↔ HasZeroOneSolution A |
| 158 | |
| 159 | /-- ZeroOneIP is NP-complete. -/ |
| 160 | axiom zeroOneIP_NP_complete : NP.Complete ZeroOneIP |
| 161 | |
| 162 | end Lax799700.ZeroOneIP |
| 163 |
Used by
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments