Zero-one knapsack problem

StructureKnapsack item#✓fully proved

A zero-one knapsack item consists of a weight \(w \in \mathbb{N}\) and a value \(v \in \mathbb{N}\).

structure Item where
  /-- Weight consumed when the item is selected. -/
  weight : Nat
  /-- Value contributed when the item is selected. -/
  value : Nat
deriving DecidableEq, Repr

Used by 8

Used byFeasible knapsack selection · Knapsack result · Bottom-up zero-one knapsack algorithm · Correctness of the zero-one knapsack algorithm · Exact cost of the knapsack algorithm · Pseudo-polynomial cost bound for knapsack · Total value of a knapsack selection · Total weight of a knapsack selection

StructureKnapsack result#✓fully proved

For a list of \(n\) knapsack items, a knapsack result consists of a set \(S \subseteq \{0, \dots, n - 1\}\) of item indices, the chosen items, and a natural number, the reported total value.

structure Result (items : List Item) where
  /-- Selected original item indices. -/
  chosen : Finset (Fin items.length)
  /-- Reported total value. -/
  value : Nat
deriving DecidableEq

Uses 1 · Used by 4

Statement usesKnapsack item

Used byBottom-up zero-one knapsack algorithm · Correctness of the zero-one knapsack algorithm · Exact cost of the knapsack algorithm · Pseudo-polynomial cost bound for knapsack

DefinitionTotal weight of a knapsack selection#✓fully proved

For knapsack items \(x_0, \dots, x_{n-1}\) with weights \(w_i\) and a set \(S \subseteq \{0, \dots, n - 1\}\) of item indices, the total weight of \(S\) is \(\sum_{i \in S} w_i\).

def totalWeight (items : List Item) (chosen : Finset (Fin items.length)) : Nat :=
  chosen.sum fun i => (items.get i).weight

Uses 1 · Used by 2

Statement usesKnapsack item

Used byFeasible knapsack selection · Correctness of the zero-one knapsack algorithm

DefinitionTotal value of a knapsack selection#✓fully proved

For knapsack items \(x_0, \dots, x_{n-1}\) with values \(v_i\) and a set \(S \subseteq \{0, \dots, n - 1\}\) of item indices, the total value of \(S\) is \(\sum_{i \in S} v_i\).

def totalValue (items : List Item) (chosen : Finset (Fin items.length)) : Nat :=
  chosen.sum fun i => (items.get i).value

Uses 1 · Used by 1

Statement usesKnapsack item

Used byCorrectness of the zero-one knapsack algorithm

DefinitionFeasible knapsack selection#✓fully proved

For knapsack items \(x_0, \dots, x_{n-1}\) with weights \(w_i\) and a capacity \(W \in \mathbb{N}\), a set \(S \subseteq \{0, \dots, n - 1\}\) of item indices is feasible when its total weight \(\sum_{i \in S} w_i\) is at most \(W\).

def Feasible (items : List Item) (capacity : Nat)
    (chosen : Finset (Fin items.length)) : Prop :=
  totalWeight items chosen ≤ capacity

Uses 2 · Used by 1

Statement usesKnapsack item · Total weight of a knapsack selection

Used byCorrectness of the zero-one knapsack algorithm

DefinitionBottom-up zero-one knapsack algorithm#✓fully proved

Given knapsack items \(x_0, \dots, x_{n-1}\) with weights \(w_i\) and values \(v_i\) and a capacity \(W \in \mathbb{N}\), the algorithm fills a table \(V(i, c)\) for \(0 \le i \le n\) and \(0 \le c \le W\) by \(V(0, c) = 0\) and, for \(i < n\), \(V(i + 1, c) = \max(V(i, c), V(i, c - w_i) + v_i)\) if \(w_i \le c\) and \(V(i + 1, c) = V(i, c)\) otherwise. Starting from \(c = W\), it then inspects the rows \(i = n, n - 1, \dots, 1\): if \(V(i, c) = V(i - 1, c)\) it skips item \(i - 1\), and otherwise it selects index \(i - 1\) and replaces \(c\) by \(c - w_{i-1}\). It returns the selected index set together with the value \(V(n, W)\). Each of the \(n(W + 1)\) cells of rows \(1, \dots, n\) costs one tick, and each of the \(n\) inspected rows costs one tick.

Cslib.Algorithms.Lean.TimeM.Knapsack.solve · 64 lines

def solve (items : List Item) (capacity : Nat) : TimeM Nat (Result items) :=
  let Row (n : Nat) := Subtype (fun row : Array Nat => row.size = n + 1)
  let rec @[reducible] buildRow (item : Item) (up : Row capacity) :
      (c : Nat) → c ≤ capacity → TimeM Nat (Row c)
    | 0, _ => do
        TimeM.tick 1
        let without := up.1[0]'(by rw [up.2]; omega)
        let value := if item.weight ≤ 0 then
          max without (up.1[0 - item.weight]'(by rw [up.2]; omega) + item.value)
        else
          without
        pure ⟨#[value], by simp⟩
    | c + 1, hc => do
        let row ← buildRow item up c (by omega)
        TimeM.tick 1
        let without := up.1[c + 1]'(by rw [up.2]; omega)
        let value := if item.weight ≤ c + 1 then
          max without (up.1[c + 1 - item.weight]'(by rw [up.2]; omega) + item.value)
        else
          without
        pure ⟨row.1.push value, by simp [row.2]⟩
  let Table (m : Nat) := Subtype (fun data : Array (Array Nat) =>
    data.size = m + 1 ∧ ∀ i (hi : i < data.size), data[i].size = capacity + 1)
  let cell {m : Nat} (table : Table m) (i c : Nat) (hi : i ≤ m) (hc : c ≤ capacity) : Nat :=
    (table.1[i]'(by rw [table.2.1]; omega))[c]'(by rw [table.2.2]; omega)
  let rec @[reducible] buildTable (values : Array Item) :
      (i : Nat) → i ≤ values.size → TimeM Nat (Table i)
    | 0, _ => pure ⟨#[Array.replicate (capacity + 1) 0], by simp, by
        intro i hi
        have : i = 0 := by simpa using hi
        subst i
        simp⟩
    | i + 1, hi => do
        let table ← buildTable values i (by omega)
        let up : Row capacity :=
          ⟨table.1[i]'(by rw [table.2.1]; omega),
            table.2.2 i (by rw [table.2.1]; omega)⟩
        let row ← buildRow (values[i]'(by omega)) up capacity (by omega)
        pure ⟨table.1.push row.1, by simp [table.2.1], by
          intro k hk
          rw [Array.getElem_push]
          split
          · exact table.2.2 _ _
          · exact row.2⟩
  let rec @[reducible] reconstruct (values : Array Item) (hvalues : values.size = items.length)
      (table : Table values.size) :
      (i c : Nat) → i ≤ values.size → c ≤ capacity →
        TimeM Nat (Finset (Fin items.length))
    | 0, _, _, _ => pure ∅
    | i + 1, c, hi, hc => do
        TimeM.tick 1
        if cell table (i + 1) c hi hc = cell table i c (by omega) hc then
          reconstruct values hvalues table i c (by omega) hc
        else
          return insert ⟨i, by omega⟩
            (← reconstruct values hvalues table i (c - values[i].weight) (by omega) (by omega))
  let values := items.toArray
  do
    let table ← buildTable values values.size (by omega)
    let chosen ← reconstruct values (by simp [values]) table values.size capacity
      (by omega) (by omega)
    pure {
      chosen := chosen
      value := cell table values.size capacity (by omega) (by omega) }

Uses 2 · Used by 3

Statement usesKnapsack item · Knapsack result

Used byCorrectness of the zero-one knapsack algorithm · Exact cost of the knapsack algorithm · Pseudo-polynomial cost bound for knapsack

TheoremCorrectness of the zero-one knapsack algorithm#✓fully proved

For every list of knapsack items and every capacity \(W \in \mathbb{N}\), let \(S\) and \(v\) be the index set and the reported value returned by the bottom-up knapsack algorithm. Then \(S\) is feasible for \(W\), \(v\) is the total value of \(S\), and every feasible set \(T\) of item indices has total value at most \(v\).

theorem solve_correct (items : List Item) (capacity : Nat) :
    let result := (solve items capacity).ret
    Feasible items capacity result.chosen ∧
      result.value = totalValue items result.chosen ∧
      ∀ chosen : Finset (Fin items.length),
        Feasible items capacity chosen → totalValue items chosen ≤ result.value

Uses 6

Statement usesFeasible knapsack selection · Knapsack item · Knapsack result · Bottom-up zero-one knapsack algorithm · Total value of a knapsack selection

Proof usesTotal weight of a knapsack selection

TheoremExact cost of the knapsack algorithm#✓fully proved

For every list of \(n\) knapsack items and every capacity \(W \in \mathbb{N}\), the bottom-up knapsack algorithm costs exactly \(n(W + 1) + n\) ticks: one for each of the \(n(W + 1)\) table cells it computes and one for each of the \(n\) item rows it inspects during reconstruction.

theorem solve_time (items : List Item) (capacity : Nat) :
    (solve items capacity).time =
      items.length * (capacity + 1) + items.length

Uses 3 · Used by 1

Statement usesKnapsack item · Knapsack result · Bottom-up zero-one knapsack algorithm

Used byPseudo-polynomial cost bound for knapsack

TheoremPseudo-polynomial cost bound for knapsack#✓fully proved

For every list of \(n\) knapsack items and every capacity \(W \in \mathbb{N}\) with \(W \ge 1\), the bottom-up knapsack algorithm costs at most \(3nW\) ticks.

theorem solve_time_le_three_mul (items : List Item) (capacity : Nat)
    (hcapacity : 0 < capacity) :
    (solve items capacity).time ≤ 3 * (items.length * capacity)

Uses 4

Statement usesKnapsack item · Knapsack result · Bottom-up zero-one knapsack algorithm

Proof usesExact cost of the knapsack algorithm

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.