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)

theorem DescriptiveComplexity.KnapRed.tuple₂_ext {A : Type} {w w' : Fin 2 → A} (h0 : w 0 = w' 0) (h1 : w 1 = w' 1) : w = w'

Two 2-tuples with the same coordinates are equal.

theorem DescriptiveComplexity.KnapRed.lex2_refl {A : Type} [LinearOrder A] (w : Fin 2 → A) : Lex2 w w

theorem DescriptiveComplexity.KnapRed.lex2_trans {A : Type} [LinearOrder A] {u v w : Fin 2 → A} (h₁ : Lex2 u v) (h₂ : Lex2 v w) : Lex2 u w

theorem DescriptiveComplexity.KnapRed.lex2_antisymm {A : Type} [LinearOrder A] {u v : Fin 2 → A} (h₁ : Lex2 u v) (h₂ : Lex2 v u) : u = v

theorem DescriptiveComplexity.KnapRed.lex2_total {A : Type} [LinearOrder A] (u v : Fin 2 → A) : Lex2 u v ∨ Lex2 v u

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)

theorem DescriptiveComplexity.KnapRed.kPt_surj {A : Type} (q : kInterp.Map A) : ∃ (t : KTag) (w : Fin 2 → A), q = kPt t w

theorem DescriptiveComplexity.KnapRed.kPt_eq_iff {A : Type} {t t' : KTag} {w w' : Fin 2 → A} : kPt t w = kPt t' w' ↔ t = t' ∧ w = 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₀)

theorem DescriptiveComplexity.KnapRed.kLow_injective {A : Type} (a₀ : A) : Function.Injective (kLow a₀)

theorem DescriptiveComplexity.KnapRed.eq_kLow_iff {A : Type} {a₀ e : A} {t : KTag} {w : Fin 2 → A} : kPt t w = kLow a₀ e ↔ t = KTag.pos ∧ w = ![e, a₀]

Being the lowest position of a block, coordinate by coordinate.

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')

theorem DescriptiveComplexity.KnapRed.bwLe_pos_kLow {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] (w : Fin 2 → A) (a₀ e : A) : BWLe (kPt KTag.pos w) (kLow a₀ e) ↔ Lex2 w ![e, a₀]

Comparison with the lowest position of a block.

@[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

theorem DescriptiveComplexity.KnapRed.binNum_eq_digit {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) {p : kInterp.Map A → Prop} {sub : A → Prop} (hsub : ∀ (e : A), sub e → SSElem e) (hp : ∀ (q : kInterp.Map A), BWPosn q ∧ p q ↔ ∃ (e : A), sub e ∧ q = kLow a₀ e) : binNum BWLe BWPosn p = digitNum (fun (x1 x2 : A) => x1 ≤ x2) SSElem (base A) fun (e : A) => if sub e then 1 else 0

A binary number whose bits sit on the lowest positions of the blocks selected by sub is the base-2 ^ |A| number with digit 1 there.

theorem DescriptiveComplexity.KnapRed.bwTarget_eq {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) : BWTarget (kInterp.Map A) = digitNum (fun (x1 x2 : A) => x1 ≤ x2) SSElem (base A) fun (e : A) => if SSElem e then 1 else 0

The target is the number with digit 1 in every block.

theorem DescriptiveComplexity.KnapRed.bwWeight_eq {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) {i : kInterp.Map A} (h : BWItem i) : BWWeight i = digitNum (fun (x1 x2 : A) => x1 ≤ x2) SSElem (base A) fun (e : A) => if SSElem e ∧ SSMem e (i.2 0) then 1 else 0

The weight of an item is the number with digit 1 in the blocks of the elements of its set.

The counting step

theorem DescriptiveComplexity.KnapRed.sum_weights_eq {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) {S : kInterp.Map A → Prop} (hS : ∀ (i : kInterp.Map A), S i → BWItem i) : ∑ᶠ (i : kInterp.Map A) (_ : i ∈ {i : kInterp.Map A | S i}), BWWeight i = digitNum (fun (x1 x2 : A) => x1 ≤ x2) SSElem (base A) fun (e : A) => {i : kInterp.Map A | S i ∧ SSElem e ∧ SSMem e (i.2 0)}.ncard

The sum of the selected weights, read digit by digit: the digit of the block of e is the number of selected items whose set contains e.

theorem DescriptiveComplexity.KnapRed.count_lt_base {A : Type} [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] {S : kInterp.Map A → Prop} (hS : ∀ (i : kInterp.Map A), S i → BWItem i) {a₀ : A} (ha₀ : IsBot a₀) (e : A) : {i : kInterp.Map A | S i ∧ SSElem e ∧ SSMem e (i.2 0)}.ncard < base A

Only items are selected, and there are at most |A| of them, so the digits of the sum stay below the base.

Correctness

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.