Knapsack is NP-hard

The reduction is Karp's, from EXACT COVER: give the set s the weight ∑_{e ∈ s} B ^ rank e, one digit block per ground element, and give the target the digit 1 in every block. A subfamily then has the right weight exactly when it covers every element once – provided that the digits never carry, which is what choosing the base B above the number of sets buys.

The gadget, in the shape an interpretation can build

The base is B = 2 ^ |A|, so a block is |A| bit positions, and the bit positions are pairs: the position (e, x) is the x-th bit of the block of the ground element e. The order on positions is lexicographic, so the block of e is a contiguous range of |A| positions and the rank of its lowest position is |A| * rank e (DescriptiveComplexity.KnapRed.bitRank_kLow) – place value (2 ^ |A|) ^ rank e, as wanted.

Only the lowest position of a block ever carries a bit: the weight of s has a 1 at (e, ⊥) for e ∈ s, and the target has a 1 at (e, ⊥) for every e. The digit of the block of e in the sum over a subfamily G is therefore the number of sets of G containing e, at most the number of sets, hence at most |A| < 2 ^ |A| = B. Uniqueness of base-B expansions (DescriptiveComplexity.digitNum_inj) turns the equation into “every digit is 1”, which is exactly exactness of the cover.

The order is needed twice – to say “the lowest position of a block” and to pin the padding of the items down to a single representative – so this is an DescriptiveComplexity.OrderedFOReduction, and being one has the pleasant side effect of supplying the finiteness that the counting needs.

Formula builders over the ordered expansion of set systems

@[reducible, inline]

abbrev DescriptiveComplexity.KnapRed.ssOrd : FirstOrder.Language

The ordered expansion of the language of set systems.

Equations

• DescriptiveComplexity.KnapRed.ssOrd = FirstOrder.Language.setSystem.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.KnapRed.elemSym : ssOrd.Relations 1

The ground-element symbol in the ordered expansion.

Equations

• DescriptiveComplexity.KnapRed.elemSym = Sum.inl FirstOrder.Language.ssElem

@[reducible, inline]

abbrev DescriptiveComplexity.KnapRed.famSym : ssOrd.Relations 1

The family symbol in the ordered expansion.

Equations

• DescriptiveComplexity.KnapRed.famSym = Sum.inl FirstOrder.Language.ssFam

@[reducible, inline]

abbrev DescriptiveComplexity.KnapRed.memSym : ssOrd.Relations 2

The incidence symbol in the ordered expansion.

Equations

• DescriptiveComplexity.KnapRed.memSym = Sum.inl FirstOrder.Language.ssMem

def DescriptiveComplexity.KnapRed.elemF {α : Type} (x : α) : ssOrd.Formula α

x is a ground element, as a formula.

Equations

• DescriptiveComplexity.KnapRed.elemF x = DescriptiveComplexity.KnapRed.elemSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.KnapRed.famF {α : Type} (f : α) : ssOrd.Formula α

f is a set of the family, as a formula.

Equations

• DescriptiveComplexity.KnapRed.famF f = DescriptiveComplexity.KnapRed.famSym.formula₁ (FirstOrder.Language.var f)

def DescriptiveComplexity.KnapRed.memF {α : Type} (x f : α) : ssOrd.Formula α

x belongs to f, as a formula.

Equations

• DescriptiveComplexity.KnapRed.memF x f = DescriptiveComplexity.KnapRed.memSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var f)

def DescriptiveComplexity.KnapRed.leF {α : Type} (x y : α) : ssOrd.Formula α

x ≤ y, as a formula.

Equations

• DescriptiveComplexity.KnapRed.leF x y = FirstOrder.Language.leSymb.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.KnapRed.eqF {α : Type} (x y : α) : ssOrd.Formula α

x = y, as a formula.

Equations

• DescriptiveComplexity.KnapRed.eqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

def DescriptiveComplexity.KnapRed.ltF {α : Type} (x y : α) : ssOrd.Formula α

x < y, as a formula.

Equations

• DescriptiveComplexity.KnapRed.ltF x y = DescriptiveComplexity.KnapRed.leF x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.KnapRed.eqF x y)

noncomputable def DescriptiveComplexity.KnapRed.minF {α : Type} (x : α) : ssOrd.Formula α

x holds a minimum of the order, as a formula.

Equations

• DescriptiveComplexity.KnapRed.minF x = DescriptiveComplexity.botF x

@[simp]

theorem DescriptiveComplexity.KnapRed.realize_elemF {α A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] {v : α → A} {x : α} : (elemF x).Realize v ↔ SSElem (v x)

@[simp]

theorem DescriptiveComplexity.KnapRed.realize_famF {α A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] {v : α → A} {f : α} : (famF f).Realize v ↔ SSFam (v f)

@[simp]

theorem DescriptiveComplexity.KnapRed.realize_memF {α A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] {v : α → A} {x f : α} : (memF x f).Realize v ↔ SSMem (v x) (v f)

@[simp]

theorem DescriptiveComplexity.KnapRed.realize_leF {α A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (leF x y).Realize v ↔ v x ≤ v y

@[simp]

theorem DescriptiveComplexity.KnapRed.realize_eqF {α A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (eqF x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.KnapRed.realize_ltF {α A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] {v : α → A} {x y : α} : (ltF x y).Realize v ↔ v x < v y

@[simp]

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

Lexicographic order on pairs

def DescriptiveComplexity.KnapRed.Lex2 {A : Type} [LinearOrder A] (w w' : Fin 2 → A) : Prop

The lexicographic order on pairs of elements, as the interpretation sees them: coordinates of a 2-tuple.

Equations

• DescriptiveComplexity.KnapRed.Lex2 w w' = (w 0 < w' 0 ∨ w 0 = w' 0 ∧ w 1 ≤ w' 1)

The interpretation

inductive DescriptiveComplexity.KnapRed.KTag : Type

Tags of the reduction: the items (one per set of the family) and the bit positions (one per pair “ground element, index inside its block”).

• itm : KTag

  The item of a set of the family.

• pos : KTag

  A bit position.

@[instance_reducible]

instance DescriptiveComplexity.KnapRed.instDecidableEqKTag : DecidableEq KTag

Equations

• DescriptiveComplexity.KnapRed.instDecidableEqKTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.KnapRed.instFintypeKTag : Fintype KTag

Equations

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

instance DescriptiveComplexity.KnapRed.instNonemptyKTag : Nonempty KTag

noncomputable def DescriptiveComplexity.KnapRed.itemF : KTag → ssOrd.Formula (Fin 1 × Fin 2)

Defining formula for the items: the sets of the family, padded canonically.

Equations

• DescriptiveComplexity.KnapRed.itemF DescriptiveComplexity.KnapRed.KTag.itm = DescriptiveComplexity.KnapRed.famF (0, 0) ⊓ DescriptiveComplexity.KnapRed.minF (0, 1)
• DescriptiveComplexity.KnapRed.itemF DescriptiveComplexity.KnapRed.KTag.pos = ⊥

def DescriptiveComplexity.KnapRed.posnF : KTag → ssOrd.Formula (Fin 1 × Fin 2)

Defining formula for the bit positions: the pairs whose first coordinate is a ground element.

Equations

• DescriptiveComplexity.KnapRed.posnF DescriptiveComplexity.KnapRed.KTag.pos = DescriptiveComplexity.KnapRed.elemF (0, 0)
• DescriptiveComplexity.KnapRed.posnF DescriptiveComplexity.KnapRed.KTag.itm = ⊥

noncomputable def DescriptiveComplexity.KnapRed.bitF : KTag → KTag → ssOrd.Formula (Fin 2 × Fin 2)

Defining formula for the bits of the weights: the weight of the set s has a 1 at the lowest position of the block of e exactly when e ∈ s.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.KnapRed.bitF x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.KnapRed.tgtF : KTag → ssOrd.Formula (Fin 1 × Fin 2)

Defining formula for the bits of the target: a 1 at the lowest position of every block.

Equations

• DescriptiveComplexity.KnapRed.tgtF DescriptiveComplexity.KnapRed.KTag.pos = DescriptiveComplexity.KnapRed.elemF (0, 0) ⊓ DescriptiveComplexity.KnapRed.minF (0, 1)
• DescriptiveComplexity.KnapRed.tgtF DescriptiveComplexity.KnapRed.KTag.itm = ⊥

def DescriptiveComplexity.KnapRed.lexF : ssOrd.Formula (Fin 2 × Fin 2)

The lexicographic comparison of the two argument tuples, as a formula.

Equations

• DescriptiveComplexity.KnapRed.lexF = DescriptiveComplexity.KnapRed.ltF (0, 0) (1, 0) ⊔ DescriptiveComplexity.KnapRed.eqF (0, 0) (1, 0) ⊓ DescriptiveComplexity.KnapRed.leF (0, 1) (1, 1)

def DescriptiveComplexity.KnapRed.leKF : KTag → KTag → ssOrd.Formula (Fin 2 × Fin 2)

Defining formula for the order: items first, positions next, each group ordered lexicographically.

Equations

• DescriptiveComplexity.KnapRed.leKF DescriptiveComplexity.KnapRed.KTag.itm DescriptiveComplexity.KnapRed.KTag.itm = DescriptiveComplexity.KnapRed.lexF
• DescriptiveComplexity.KnapRed.leKF DescriptiveComplexity.KnapRed.KTag.itm DescriptiveComplexity.KnapRed.KTag.pos = ⊤
• DescriptiveComplexity.KnapRed.leKF DescriptiveComplexity.KnapRed.KTag.pos DescriptiveComplexity.KnapRed.KTag.itm = ⊥
• DescriptiveComplexity.KnapRed.leKF DescriptiveComplexity.KnapRed.KTag.pos DescriptiveComplexity.KnapRed.KTag.pos = DescriptiveComplexity.KnapRed.lexF

noncomputable def DescriptiveComplexity.KnapRed.kInterp : FOInterpretation ssOrd FirstOrder.Language.binWeights KTag 2

The interpretation of a binary-weighted instance in a set system: one item per set, one bit position per pair “ground element, index”.

Equations

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

The points of the interpreted structure

def DescriptiveComplexity.KnapRed.kPt {A : Type} (t : KTag) (w : Fin 2 → A) : kInterp.Map A

The point of tag t over the pair w.

Equations

• DescriptiveComplexity.KnapRed.kPt t w = (t, w)

@[simp]

theorem DescriptiveComplexity.KnapRed.kPt_snd {A : Type} (t : KTag) (w : Fin 2 → A) (j : Fin 2) : (kPt t w).2 j = w j

def DescriptiveComplexity.KnapRed.kItem {A : Type} (a₀ s : A) : kInterp.Map A

The item of the set s, padded with the minimum a₀.

Equations

• DescriptiveComplexity.KnapRed.kItem a₀ s = DescriptiveComplexity.KnapRed.kPt DescriptiveComplexity.KnapRed.KTag.itm ![s, a₀]

def DescriptiveComplexity.KnapRed.kPos {A : Type} (e x : A) : kInterp.Map A

The bit position (e, x): the x-th position of the block of e.

Equations

• DescriptiveComplexity.KnapRed.kPos e x = DescriptiveComplexity.KnapRed.kPt DescriptiveComplexity.KnapRed.KTag.pos ![e, x]

def DescriptiveComplexity.KnapRed.kLow {A : Type} (a₀ e : A) : kInterp.Map A

The lowest position of the block of e.

Equations

• DescriptiveComplexity.KnapRed.kLow a₀ e = DescriptiveComplexity.KnapRed.kPos e a₀

@[simp]

theorem DescriptiveComplexity.KnapRed.kItem_fst {A : Type} (a₀ s : A) : (kItem a₀ s).2 0 = s

@[simp]

theorem DescriptiveComplexity.KnapRed.kLow_fst {A : Type} (a₀ e : A) : (kLow a₀ e).2 0 = e

@[simp]

theorem DescriptiveComplexity.KnapRed.kLow_snd {A : Type} (a₀ e : A) : (kLow a₀ e).2 1 = a₀

theorem DescriptiveComplexity.KnapRed.kItem_injective {A : Type} (a₀ : A) : Function.Injective (kItem a₀)

Characterization of the interpreted relations

@[simp]

theorem DescriptiveComplexity.KnapRed.bwItem_itm {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w : Fin 2 → A) : BWItem (kPt KTag.itm w) ↔ SSFam (w 0) ∧ IsBot (w 1)

@[simp]

theorem DescriptiveComplexity.KnapRed.bwItem_pos {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w : Fin 2 → A) : ¬BWItem (kPt KTag.pos w)

@[simp]

theorem DescriptiveComplexity.KnapRed.bwPosn_pos {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w : Fin 2 → A) : BWPosn (kPt KTag.pos w) ↔ SSElem (w 0)

@[simp]

theorem DescriptiveComplexity.KnapRed.bwPosn_itm {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w : Fin 2 → A) : ¬BWPosn (kPt KTag.itm w)

@[simp]

theorem DescriptiveComplexity.KnapRed.bwTgt_pos {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w : Fin 2 → A) : BWTgt (kPt KTag.pos w) ↔ SSElem (w 0) ∧ IsBot (w 1)

@[simp]

theorem DescriptiveComplexity.KnapRed.bwTgt_itm {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w : Fin 2 → A) : ¬BWTgt (kPt KTag.itm w)

@[simp]

theorem DescriptiveComplexity.KnapRed.bwBit_itm_pos {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w w' : Fin 2 → A) : BWBit (kPt KTag.itm w) (kPt KTag.pos w') ↔ (SSFam (w 0) ∧ IsBot (w 1)) ∧ SSElem (w' 0) ∧ SSMem (w' 0) (w 0) ∧ IsBot (w' 1)

@[simp]

theorem DescriptiveComplexity.KnapRed.bwBit_itm_itm {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w w' : Fin 2 → A) : ¬BWBit (kPt KTag.itm w) (kPt KTag.itm w')

@[simp]

theorem DescriptiveComplexity.KnapRed.bwBit_pos {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w w' : Fin 2 → A) (t : KTag) : ¬BWBit (kPt KTag.pos w) (kPt t w')

@[simp]

theorem DescriptiveComplexity.KnapRed.bwLe_itm_itm {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w w' : Fin 2 → A) : BWLe (kPt KTag.itm w) (kPt KTag.itm w') ↔ Lex2 w w'

@[simp]

theorem DescriptiveComplexity.KnapRed.bwLe_pos_pos {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w w' : Fin 2 → A) : BWLe (kPt KTag.pos w) (kPt KTag.pos w') ↔ Lex2 w w'

@[simp]

theorem DescriptiveComplexity.KnapRed.bwLe_itm_pos {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w w' : Fin 2 → A) : BWLe (kPt KTag.itm w) (kPt KTag.pos w')

@[simp]

theorem DescriptiveComplexity.KnapRed.bwLe_pos_itm {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w w' : Fin 2 → A) : ¬BWLe (kPt KTag.pos w) (kPt KTag.itm w')

theorem DescriptiveComplexity.KnapRed.isLinOrd_bwLe {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] : IsLinOrd BWLe

The interpreted order is a linear order: the two tags in order, each carrying the lexicographic order on pairs.

The place values

theorem DescriptiveComplexity.KnapRed.eq_kItem {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) {i : kInterp.Map A} (h : BWItem i) : i = kItem a₀ (i.2 0) ∧ SSFam (i.2 0)

An item is the padded item of the set it carries.

theorem DescriptiveComplexity.KnapRed.bitRank_kLow {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] {a₀ : A} (ha₀ : IsBot a₀) (e : A) : bitRank BWLe BWPosn (kLow a₀ e) = Nat.card A * bitRank (fun (x1 x2 : A) => x1 ≤ x2) SSElem e

The block structure: the rank of the lowest position of the block of e is |A| times the rank of e, so its place value is (2 ^ |A|) ^ rank e – one digit of base 2 ^ |A| per ground element.

Weights and target, as base-2 ^ |A| numbers

noncomputable def DescriptiveComplexity.KnapRed.base (A : Type) [Finite A] : ℕ

The base: one digit per ground element, |A| bits wide, which is above the number of sets, so digits never carry into the next block.

Equations

• DescriptiveComplexity.KnapRed.base A = 2 ^ Nat.card A

theorem DescriptiveComplexity.KnapRed.base_pos {A : Type} [Finite A] : 0 < base A

theorem DescriptiveComplexity.KnapRed.one_lt_base {A : Type} [Finite A] [Nonempty A] : 1 < base A

The counting step

Correctness

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

def DescriptiveComplexity.KnapRed.itemsOf {A : Type} (a₀ : A) (G : A → Prop) (i : kInterp.Map A) : Prop

The items of a subfamily: the padded items of its sets.

Equations

• DescriptiveComplexity.KnapRed.itemsOf a₀ G i = ∃ (s : A), G s ∧ i = DescriptiveComplexity.KnapRed.kItem a₀ s

def DescriptiveComplexity.KnapRed.coverOfItems {A : Type} (a₀ : A) (S : kInterp.Map A → Prop) (s : A) : Prop

The subfamily of a set of items: the sets whose padded item is chosen.

Equations

• DescriptiveComplexity.KnapRed.coverOfItems a₀ S s = S (DescriptiveComplexity.KnapRed.kItem a₀ s)

theorem DescriptiveComplexity.KnapRed.subsetSum_itemsOf {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a₀ : A} (ha₀ : IsBot a₀) {G : A → Prop} (hG : ExactCoverBy SSElem SSFam SSMem G) : (∀ (i : kInterp.Map A), itemsOf a₀ G i → BWItem i) ∧ ∑ᶠ (i : kInterp.Map A) (_ : i ∈ {i : kInterp.Map A | itemsOf a₀ G i}), BWWeight i = BWTarget (kInterp.Map A)

The items of an exact cover sum to the target.

theorem DescriptiveComplexity.KnapRed.exactCoverBy_coverOfItems {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a₀ : A} (ha₀ : IsBot a₀) {S : kInterp.Map A → Prop} (hSi : ∀ (i : kInterp.Map A), S i → BWItem i) (hsum : ∑ᶠ (i : kInterp.Map A) (_ : i ∈ {i : kInterp.Map A | S i}), BWWeight i = BWTarget (kInterp.Map A)) : ExactCoverBy SSElem SSFam SSMem (coverOfItems a₀ S)

A set of items summing to the target is an exact cover.

theorem DescriptiveComplexity.KnapRed.hasExactCover_iff_hasSubsetSum (A : Type) [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : HasExactCover A ↔ HasSubsetSum (kInterp.Map A)

Correctness of the reduction: the set system has an exact cover iff the interpreted binary-weighted instance has a set of items summing to the target.

noncomputable def DescriptiveComplexity.exactCover_ordered_fo_reduction_knapsack : OrderedFOReduction ExactCover Knapsack

Exact Cover FO-reduces to Knapsack, over any linear order on the input: one item per set, one digit block of |A| bits per ground element, weights carrying a 1 in the block of each of their elements and the target a 1 in every block.

Equations

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