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)

theorem DescriptiveComplexity.IPRed.ipPt_injective {A : Type} : Function.Injective ipPt

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

theorem DescriptiveComplexity.IPRed.ipCoefVal_eq {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] {r j : A} (hr : IsBot r) (hj : BWItem j) : IPCoefVal (ipPt r) (ipPt j) = BWWeight j

The entry of the single row in the column of an item is the weight of that item.

theorem DescriptiveComplexity.IPRed.ipRhsVal_eq {A : Type} [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] {r : A} (hr : IsBot r) : IPRhsVal (ipPt r) = BWTarget A

The right-hand side of the single row is the target.

Correctness

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.