0-1 integer programming is NP-hard

A single equation with 0-1 variables is a subset-sum instance, so the reduction from Knapsack is the identity in everything but the vocabulary: the items become the columns, the target becomes the right-hand side, and the whole instance becomes one equation.

The only thing to build is that single row. The interpretation has one tag and dimension one, so its universe is a copy of the input (DescriptiveComplexity.IPRed.ipPt); the row is the minimum of the input order, which is the one element a first-order formula can name. Everything else – columns, positions, bits, and the order carrying the place values, which stays the input's own le – is read off unchanged, so no arithmetic appears anywhere and the correctness proof is a transport of binNum along that copy.

Naming the minimum is the only use of the order, so this is an DescriptiveComplexity.OrderedFOReduction; conveniently, being one also supplies the finiteness and nonemptiness that make the minimum exist.

Formula builders over the ordered expansion of binary-weighted instances

@[reducible, inline]

abbrev DescriptiveComplexity.IPRed.bwOrd : FirstOrder.Language

The ordered expansion of the language of binary-weighted instances.

Equations

• DescriptiveComplexity.IPRed.bwOrd = FirstOrder.Language.binWeights.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.IPRed.itemSym : bwOrd.Relations 1

The item symbol in the ordered expansion.

Equations

• DescriptiveComplexity.IPRed.itemSym = Sum.inl FirstOrder.Language.bwItem

@[reducible, inline]

abbrev DescriptiveComplexity.IPRed.posnSym : bwOrd.Relations 1

The position symbol in the ordered expansion.

Equations

• DescriptiveComplexity.IPRed.posnSym = Sum.inl FirstOrder.Language.bwPosn

@[reducible, inline]

abbrev DescriptiveComplexity.IPRed.bitSym : bwOrd.Relations 2

The bit symbol in the ordered expansion.

Equations

• DescriptiveComplexity.IPRed.bitSym = Sum.inl FirstOrder.Language.bwBit

@[reducible, inline]

abbrev DescriptiveComplexity.IPRed.tgtSym : bwOrd.Relations 1

The target symbol in the ordered expansion.

Equations

• DescriptiveComplexity.IPRed.tgtSym = Sum.inl FirstOrder.Language.bwTgt

@[reducible, inline]

abbrev DescriptiveComplexity.IPRed.leBwSym : bwOrd.Relations 2

The place-value order symbol in the ordered expansion.

Equations

• DescriptiveComplexity.IPRed.leBwSym = Sum.inl FirstOrder.Language.bwLe

def DescriptiveComplexity.IPRed.itemF {α : Type} (x : α) : bwOrd.Formula α

x is an item, as a formula.

Equations

• DescriptiveComplexity.IPRed.itemF x = DescriptiveComplexity.IPRed.itemSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.IPRed.posnF {α : Type} (x : α) : bwOrd.Formula α

x is a bit position, as a formula.

Equations

• DescriptiveComplexity.IPRed.posnF x = DescriptiveComplexity.IPRed.posnSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.IPRed.bitF {α : Type} (i p : α) : bwOrd.Formula α

The weight of i has bit 1 at p, as a formula.

Equations

• DescriptiveComplexity.IPRed.bitF i p = DescriptiveComplexity.IPRed.bitSym.formula₂ (FirstOrder.Language.var i) (FirstOrder.Language.var p)

def DescriptiveComplexity.IPRed.tgtF {α : Type} (p : α) : bwOrd.Formula α

The target has bit 1 at p, as a formula.

Equations

• DescriptiveComplexity.IPRed.tgtF p = DescriptiveComplexity.IPRed.tgtSym.formula₁ (FirstOrder.Language.var p)

def DescriptiveComplexity.IPRed.leBwF {α : Type} (x y : α) : bwOrd.Formula α

x is below y in the place-value order, as a formula.

Equations

• DescriptiveComplexity.IPRed.leBwF x y = DescriptiveComplexity.IPRed.leBwSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.IPRed.minF {α : Type} (x : α) : bwOrd.Formula α

x is a minimum of the input order, as a formula.

Equations

• DescriptiveComplexity.IPRed.minF x = DescriptiveComplexity.botF x

@[simp]

theorem DescriptiveComplexity.IPRed.realize_itemF {α A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] {v : α → A} {x : α} : (itemF x).Realize v ↔ BWItem (v x)

@[simp]

theorem DescriptiveComplexity.IPRed.realize_posnF {α A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] {v : α → A} {x : α} : (posnF x).Realize v ↔ BWPosn (v x)

@[simp]

theorem DescriptiveComplexity.IPRed.realize_bitF {α A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] {v : α → A} {i p : α} : (bitF i p).Realize v ↔ BWBit (v i) (v p)

@[simp]

theorem DescriptiveComplexity.IPRed.realize_tgtF {α A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] {v : α → A} {p : α} : (tgtF p).Realize v ↔ BWTgt (v p)

@[simp]

theorem DescriptiveComplexity.IPRed.realize_leBwF {α A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (leBwF x y).Realize v ↔ BWLe (v x) (v y)

@[simp]

theorem DescriptiveComplexity.IPRed.realize_minF {α A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] {v : α → A} {x : α} : (minF x).Realize v ↔ IsBot (v x)

The interpretation

noncomputable def DescriptiveComplexity.IPRed.ipInterp : FOInterpretation bwOrd FirstOrder.Language.zeroOneIP Unit 1

The interpretation of a 0-1 integer program in a binary-weighted instance: one column per item, one bit position per bit position, and a single row – the minimum of the input order – whose entries are the weights and whose right-hand side is the target.

Equations

• One or more equations did not get rendered due to their size.

The interpreted structure is a copy of the input

def DescriptiveComplexity.IPRed.ipPt {A : Type} (a : A) : ipInterp.Map A

The point of the interpreted structure carrying a.

Equations

• DescriptiveComplexity.IPRed.ipPt a = ((), fun (x : Fin 1) => a)

@[simp]

theorem DescriptiveComplexity.IPRed.ipPt_snd {A : Type} (a : A) (j : Fin 1) : (ipPt a).2 j = a

theorem DescriptiveComplexity.IPRed.ipPt_surj {A : Type} (q : ipInterp.Map A) : q = ipPt (q.2 0)

def DescriptiveComplexity.IPRed.ipEquiv {A : Type} : A ≃ ipInterp.Map A

The interpreted universe is a copy of the input, which is what makes the whole correctness proof a transport.

Equations

• DescriptiveComplexity.IPRed.ipEquiv = { toFun := DescriptiveComplexity.IPRed.ipPt, invFun := fun (q : DescriptiveComplexity.IPRed.ipInterp.Map A) => q.2 0, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem DescriptiveComplexity.IPRed.ipEquiv_apply {A : Type} (a : A) : ipEquiv a = ipPt a

Characterization of the interpreted relations

@[simp]

theorem DescriptiveComplexity.IPRed.ipCol_iff {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] (a : A) : IPCol (ipPt a) ↔ BWItem a

@[simp]

theorem DescriptiveComplexity.IPRed.ipRow_iff {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] (a : A) : IPRow (ipPt a) ↔ IsBot a

@[simp]

theorem DescriptiveComplexity.IPRed.ipPosn_iff {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] (a : A) : IPPosn (ipPt a) ↔ BWPosn a

@[simp]

theorem DescriptiveComplexity.IPRed.ipCoef_iff {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] (r j p : A) : IPCoef (ipPt r) (ipPt j) (ipPt p) ↔ IsBot r ∧ BWItem j ∧ BWPosn p ∧ BWBit j p

@[simp]

theorem DescriptiveComplexity.IPRed.ipRhs_iff {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] (r p : A) : IPRhs (ipPt r) (ipPt p) ↔ IsBot r ∧ BWPosn p ∧ BWTgt p

@[simp]

theorem DescriptiveComplexity.IPRed.ipLe_iff {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] (a b : A) : IPLe (ipPt a) (ipPt b) ↔ BWLe a b

theorem DescriptiveComplexity.IPRed.isLinOrd_ipLe {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] (h : IsLinOrd BWLe) : IsLinOrd IPLe

The interpreted order is the input's own place-value order, read on the copy.

The numbers, transported

Correctness

Stated for an explicit set of items and an explicit 0-1 vector, so that the same lemmas give the equivalence of the two decision problems and the bijection between their solutions (DescriptiveComplexity.Problems.ZeroOneIP.CountingHardness).

def DescriptiveComplexity.IPRed.colsOf {A : Type} (S : A → Prop) (q : ipInterp.Map A) : Prop

The columns of a set of items.

Equations

• DescriptiveComplexity.IPRed.colsOf S q = S (q.2 0)

def DescriptiveComplexity.IPRed.itemsOfCols {A : Type} (x : ipInterp.Map A → Prop) (a : A) : Prop

The items of a set of columns.

Equations

• DescriptiveComplexity.IPRed.itemsOfCols x a = x (DescriptiveComplexity.IPRed.ipPt a)

theorem DescriptiveComplexity.IPRed.isLinOrd_bwLe_of_ipLe {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] (hlin : IsLinOrd IPLe) : IsLinOrd BWLe

The order of the interpreted program is linear exactly when the input's is.

theorem DescriptiveComplexity.IPRed.zeroOneSol_colsOf {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] {S : A → Prop} (hSi : ∀ (i : A), S i → BWItem i) (hsum : ∑ᶠ (i : A) (_ : i ∈ {i : A | S i}), BWWeight i = BWTarget A) : (∀ (q : ipInterp.Map A), colsOf S q → IPCol q) ∧ ∀ (r : ipInterp.Map A), IPRow r → ∑ᶠ (j : ipInterp.Map A) (_ : j ∈ {j : ipInterp.Map A | colsOf S j}), IPCoefVal r j = IPRhsVal r

A set of items summing to the target solves the one-equation program.

theorem DescriptiveComplexity.IPRed.subsetSum_itemsOfCols {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {x : ipInterp.Map A → Prop} (hxc : ∀ (j : ipInterp.Map A), x j → IPCol j) (heq : ∀ (r : ipInterp.Map A), IPRow r → ∑ᶠ (j : ipInterp.Map A) (_ : j ∈ {j : ipInterp.Map A | x j}), IPCoefVal r j = IPRhsVal r) : (∀ (a : A), itemsOfCols x a → BWItem a) ∧ ∑ᶠ (i : A) (_ : i ∈ {i : A | itemsOfCols x i}), BWWeight i = BWTarget A

A solution of the one-equation program is a set of items summing to the target.

theorem DescriptiveComplexity.IPRed.hasSubsetSum_iff_hasZeroOneSolution (A : Type) [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : HasSubsetSum A ↔ HasZeroOneSolution (ipInterp.Map A)

Correctness of the reduction: a binary-weighted instance has a set of items summing to the target iff the one-equation program interpreted in it has a 0-1 solution.

noncomputable def DescriptiveComplexity.knapsack_ordered_fo_reduction_zeroOneIP : OrderedFOReduction Knapsack ZeroOneIP

Knapsack FO-reduces to 0-1 integer programming, over any linear order on the input: the items become the columns, the target the right-hand side, and the whole instance a single equation, carried by the minimum of the order.

Equations

• One or more equations did not get rendered due to their size.