Multiple-choice knapsack problem

StructureKnapsack item with weight and value#✓fully proved

A knapsack item with a natural weight and a value in β.

structure Item (β : Type u) where
  /-- The weight counted against the constraint. -/
  weight : ℕ
  /-- The value collected when the item is chosen. -/
  value : β
deriving DecidableEq, Repr

Used by 13

Used byCovering recurrence for multiple-choice knapsack · Covering recurrence is bottom iff no selection reaches the target · Packing recurrence for multiple-choice knapsack · Packing recurrence is bottom iff no selection fits the capacity · Covering recurrence is attained by a covering selection · Packing recurrence is attained by a feasible selection · Multiple-choice knapsack selection · Covering recurrence bounds every covering selection's value · Packing recurrence bounds every feasible selection's value · Bottom-up packing table for multiple-choice knapsack · Packing table computes the packing recurrence · Total value of a knapsack selection · Total weight of a knapsack selection

DefinitionMultiple-choice knapsack selection#✓fully proved

A selection chooses exactly one item from each group, in group order.

def IsSelection (groups : List (List (Item β))) (choice : List (Item β)) : Prop :=
  List.Forall₂ (fun item group => item ∈ group) choice groups

Uses 1 · Used by 6

Statement usesKnapsack item with weight and value

Used byCovering recurrence is bottom iff no selection reaches the target · Packing recurrence is bottom iff no selection fits the capacity · Covering recurrence is attained by a covering selection · Packing recurrence is attained by a feasible selection · Covering recurrence bounds every covering selection's value · Packing recurrence bounds every feasible selection's value

DefinitionTotal weight of a knapsack selection#✓fully proved

The total weight of a selection.

def totalWeight (choice : List (Item β)) : ℕ := (choice.map Item.weight).sum

Uses 1 · Used by 6

Statement usesKnapsack item with weight and value

Used byCovering recurrence is bottom iff no selection reaches the target · Packing recurrence is bottom iff no selection fits the capacity · Covering recurrence is attained by a covering selection · Packing recurrence is attained by a feasible selection · Covering recurrence bounds every covering selection's value · Packing recurrence bounds every feasible selection's value

DefinitionTotal value of a knapsack selection#✓fully proved

The total value of a selection.

def totalValue [AddMonoid β] (choice : List (Item β)) : β := (choice.map Item.value).sum

Uses 1 · Used by 6

Statement usesKnapsack item with weight and value

Used byCovering recurrence is bottom iff no selection reaches the target · Packing recurrence is bottom iff no selection fits the capacity · Covering recurrence is attained by a covering selection · Packing recurrence is attained by a feasible selection · Covering recurrence bounds every covering selection's value · Packing recurrence bounds every feasible selection's value

DefinitionPacking recurrence for multiple-choice knapsack#✓fully proved

The packing recurrence: the best total value of a selection with total weight at most c, ⊥ if none exists.

def bestPacking : List (List (Item β)) → ℕ → WithBot β
  | [], _ => 0
  | group :: groups, c =>
      (group.map fun item =>
        if item.weight ≤ c then (item.value : WithBot β) + bestPacking groups (c - item.weight)
        else ⊥).foldr max ⊥

Uses 1 · Used by 4

Statement usesKnapsack item with weight and value

Used byPacking recurrence is bottom iff no selection fits the capacity · Packing recurrence is attained by a feasible selection · Packing recurrence bounds every feasible selection's value · Packing table computes the packing recurrence

DefinitionCovering recurrence for multiple-choice knapsack#✓fully proved

The covering recurrence: the best total value of a selection with total weight at least L, ⊥ if none exists. The residual target L - weight is truncated subtraction.

def bestCovering : List (List (Item β)) → ℕ → WithBot β
  | [], L => if L = 0 then 0 else ⊥
  | group :: groups, L =>
      (group.map fun item =>
        (item.value : WithBot β) + bestCovering groups (L - item.weight)).foldr max ⊥

Uses 1 · Used by 3

Statement usesKnapsack item with weight and value

Used byCovering recurrence is bottom iff no selection reaches the target · Covering recurrence is attained by a covering selection · Covering recurrence bounds every covering selection's value

TheoremPacking recurrence bounds every feasible selection's value#✓fully proved

The packing recurrence is an upper bound: every feasible selection's value is at most bestPacking.

theorem le_bestPacking [IsOrderedAddMonoid β] :
    ∀ {groups : List (List (Item β))} {choice : List (Item β)} {c : ℕ},
      IsSelection groups choice → totalWeight choice ≤ c →
        ((totalValue choice : β) : WithBot β) ≤ bestPacking groups c

Uses 5 · Used by 1

Statement usesMultiple-choice knapsack selection · Knapsack item with weight and value · Packing recurrence for multiple-choice knapsack · Total value of a knapsack selection · Total weight of a knapsack selection

Used byPacking recurrence is bottom iff no selection fits the capacity

TheoremPacking recurrence is attained by a feasible selection#✓fully proved

The packing recurrence is attained: a finite value is the value of a feasible selection.

theorem exists_eq_of_bestPacking_eq_coe :
    ∀ {groups : List (List (Item β))} {c : ℕ} {v : β}, bestPacking groups c = v →
      ∃ choice, IsSelection groups choice ∧ totalWeight choice ≤ c ∧ totalValue choice = v

Uses 5 · Used by 1

Statement usesMultiple-choice knapsack selection · Knapsack item with weight and value · Packing recurrence for multiple-choice knapsack · Total value of a knapsack selection · Total weight of a knapsack selection

Used byPacking recurrence is bottom iff no selection fits the capacity

TheoremPacking recurrence is bottom iff no selection fits the capacity#✓fully proved

The packing recurrence is ⊥ exactly when no selection fits the capacity.

theorem bestPacking_eq_bot_iff [IsOrderedAddMonoid β] {groups : List (List (Item β))} {c : ℕ} :
    bestPacking groups c = ⊥ ↔
      ¬ ∃ choice, IsSelection groups choice ∧ totalWeight choice ≤ c

Uses 7

Statement usesMultiple-choice knapsack selection · Knapsack item with weight and value · Packing recurrence for multiple-choice knapsack · Total weight of a knapsack selection

Proof usesPacking recurrence is attained by a feasible selection · Packing recurrence bounds every feasible selection's value · Total value of a knapsack selection

TheoremCovering recurrence bounds every covering selection's value#✓fully proved

The covering recurrence is an upper bound: every selection of total weight at least L has value at most bestCovering.

theorem le_bestCovering [IsOrderedAddMonoid β] :
    ∀ {groups : List (List (Item β))} {choice : List (Item β)} {L : ℕ},
      IsSelection groups choice → L ≤ totalWeight choice →
        ((totalValue choice : β) : WithBot β) ≤ bestCovering groups L

Uses 5 · Used by 1

Statement usesMultiple-choice knapsack selection · Knapsack item with weight and value · Covering recurrence for multiple-choice knapsack · Total value of a knapsack selection · Total weight of a knapsack selection

Used byCovering recurrence is bottom iff no selection reaches the target

TheoremCovering recurrence is attained by a covering selection#✓fully proved

The covering recurrence is attained: a finite value is the value of a selection of total weight at least L.

theorem exists_eq_of_bestCovering_eq_coe :
    ∀ {groups : List (List (Item β))} {L : ℕ} {v : β}, bestCovering groups L = v →
      ∃ choice, IsSelection groups choice ∧ L ≤ totalWeight choice ∧ totalValue choice = v

Uses 5 · Used by 1

Statement usesMultiple-choice knapsack selection · Knapsack item with weight and value · Covering recurrence for multiple-choice knapsack · Total value of a knapsack selection · Total weight of a knapsack selection

Used byCovering recurrence is bottom iff no selection reaches the target

TheoremCovering recurrence is bottom iff no selection reaches the target#✓fully proved

The covering recurrence is ⊥ exactly when no selection reaches the target.

theorem bestCovering_eq_bot_iff [IsOrderedAddMonoid β] {groups : List (List (Item β))} {L : ℕ} :
    bestCovering groups L = ⊥ ↔
      ¬ ∃ choice, IsSelection groups choice ∧ L ≤ totalWeight choice

Uses 7

Statement usesMultiple-choice knapsack selection · Knapsack item with weight and value · Covering recurrence for multiple-choice knapsack · Total weight of a knapsack selection

Proof usesCovering recurrence is attained by a covering selection · Covering recurrence bounds every covering selection's value · Total value of a knapsack selection

DefinitionBottom-up packing table for multiple-choice knapsack#✓fully proved

The bottom-up packing table: for each suffix of the groups, the row of best values at capacities 0, …, capacity, each row computed from the next one by one scan of its group per cell.

def packingTable (capacity : ℕ) : List (List (Item β)) → List (WithBot β)
  | [] => (List.range (capacity + 1)).map fun _ => 0
  | group :: groups =>
      let next := packingTable capacity groups
      (List.range (capacity + 1)).map fun c =>
        (group.map fun item =>
          if item.weight ≤ c then (item.value : WithBot β) + next.getD (c - item.weight) ⊥
          else ⊥).foldr max ⊥

Uses 1 · Used by 1

Statement usesKnapsack item with weight and value

Used byPacking table computes the packing recurrence

TheoremPacking table computes the packing recurrence#✓fully proved

The table computes the recurrence at every capacity 0, …, capacity.

theorem packingTable_eq (capacity : ℕ) :
    ∀ groups : List (List (Item β)),
      packingTable capacity groups = (List.range (capacity + 1)).map (bestPacking groups)

Uses 3

Statement usesKnapsack item with weight and value · Packing recurrence for multiple-choice knapsack · Bottom-up packing table for multiple-choice knapsack

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.