The 0-1 knapsack problem

Knapsack is the decision version of the 0-1 knapsack problem: an instance x : KnapsackInstance (Cslib.Complexity.encKnapsack) gives a list of items x.items (Cslib.Complexity.Knapsack.Item), each with a weight and a value, a capacity x.capacity, and a goal x.goal, and asks whether some sub-multiset of the items has total weight at most x.capacity and total value at least x.goal [GJ79]. All numbers are encoded in binary (encNat); the verifier compares the sums in binary (ComputableInPolyTime.binary_le).

Giving every number of a subset sum instance equal weight and value, and taking the target as both capacity and goal, reduces SubsetSum to Knapsack. Karp's KNAPSACK [Kar72] is the subset sum form of the problem.

Main definitions

• Cslib.Complexity.Knapsack.Item, Cslib.Complexity.Knapsack.encItem: knapsack items with weight and value, and their binary encoding.
• Cslib.Complexity.KnapsackInstance, Cslib.Complexity.encKnapsack: knapsack instances and their binary encoding.
• Cslib.Complexity.Knapsack, Cslib.Complexity.Knapsack.verifier.
• Cslib.Complexity.SubsetSum.toKnapsack.

Main results

• Cslib.Complexity.mem_Knapsack_iff_sublist: solutions are subsequences of the items.
• Cslib.Complexity.Knapsack.mem_NP: Knapsack ∈ NP encKnapsack.
• Cslib.Complexity.SubsetSum.toKnapsack_mem_iff: correctness of the reduction.
• Cslib.Complexity.polyTimeReducible_SubsetSum_Knapsack, Cslib.Complexity.Knapsack_npHard, Cslib.Complexity.Knapsack_npComplete: Knapsack is NP-complete.

References

• R. M. Karp, Reducibility among combinatorial problems
• M. R. Garey and D. S. Johnson, Computers and Intractability
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

structure Cslib.Complexity.Knapsack.Item : Type

An item in Knapsack, with a natural-number weight and value.

• weight : ℕ

  The weight of the item.

• value : ℕ

  The value of the item.

theorem Cslib.Complexity.Knapsack.Item.ext {x y : Item} (weight : x.weight = y.weight) (value : x.value = y.value) : x = y

theorem Cslib.Complexity.Knapsack.Item.ext_iff {x y : Item} : x = y ↔ x.weight = y.weight ∧ x.value = y.value

def Cslib.Complexity.Knapsack.instDecidableEqItem.decEq (x✝ x✝¹ : Item) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.Knapsack.instDecidableEqItem : DecidableEq Item

@[instance_reducible]

instance Cslib.Complexity.Knapsack.instReprItem : Repr Item

def Cslib.Complexity.Knapsack.instReprItem.repr : Item → ℕ → Std.Format

theorem Cslib.Complexity.Knapsack.encItem_value_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Item} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encItem → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).value) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.Knapsack.encItem_weight_inO : Turing.MultiTapeTM.ComputableInO Item.weight encItem Turing.MultiTapeTM.encNat (fun (a : Item) => (encItem a).length) fun (a : Item) => (encItem a).length

def Cslib.Complexity.Knapsack.encItem : Item ↪ List Bool

Binary encoding of a Knapsack.Item as (weight, value).

theorem Cslib.Complexity.Knapsack.encItem_weight_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Item} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encItem → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).weight) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.Knapsack.encItem_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encNat budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { weight := x0 x, value := x1 x }) encIn encItem budget

@[reducible, inline]

abbrev Cslib.Complexity.Knapsack.encItemFields : ℕ × ℕ ↪ List Bool

The tuple of the fields of encItem.

theorem Cslib.Complexity.Knapsack.encItem_value_inO : Turing.MultiTapeTM.ComputableInO Item.value encItem Turing.MultiTapeTM.encNat (fun (a : Item) => (encItem a).length) fun (a : Item) => (encItem a).length

theorem Cslib.Complexity.Knapsack.encItem_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : ℕ × ℕ) => { weight := p.1, value := p.2 }) encItemFields encItem 1 1

theorem Cslib.Complexity.Knapsack.encItem_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 x1 T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encNat T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { weight := x0 x, value := x1 x }) encIn encItem (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.Knapsack.encItem_value_deg : Turing.MultiTapeTM.ComputableInDegree Item.value encItem Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.Knapsack.encItem_value_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Item} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encItem S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).value) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.Knapsack.encItem_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : Item) => (a.weight, a.value)) encItem encItemFields 1 1

theorem Cslib.Complexity.Knapsack.encItem_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encNat) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { weight := x0 x, value := x1 x }) encIn encItem

theorem Cslib.Complexity.Knapsack.encItem_weight_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Item} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encItem S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).weight) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.Knapsack.encItem_weight_deg : Turing.MultiTapeTM.ComputableInDegree Item.weight encItem Turing.MultiTapeTM.encNat 1 1

@[simp]

theorem Cslib.Complexity.Knapsack.encItem_apply (a : Item) : encItem a = encItemFields (a.weight, a.value)

structure Cslib.Complexity.KnapsackInstance : Type

An instance of the 0-1 knapsack problem Garey and Johnson: a list of items items, a weight capacity capacity, and a value goal goal.

• items : List Knapsack.Item

  The available items, each with a weight and a value.

• capacity : ℕ

  The maximum total weight allowed.

• goal : ℕ

  The minimum total value required.

theorem Cslib.Complexity.KnapsackInstance.ext_iff {x y : KnapsackInstance} : x = y ↔ x.items = y.items ∧ x.capacity = y.capacity ∧ x.goal = y.goal

theorem Cslib.Complexity.KnapsackInstance.ext {x y : KnapsackInstance} (items : x.items = y.items) (capacity : x.capacity = y.capacity) (goal : x.goal = y.goal) : x = y

def Cslib.Complexity.instDecidableEqKnapsackInstance.decEq (x✝ x✝¹ : KnapsackInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqKnapsackInstance : DecidableEq KnapsackInstance

@[instance_reducible]

instance Cslib.Complexity.instReprKnapsackInstance : Repr KnapsackInstance

def Cslib.Complexity.instReprKnapsackInstance.repr : KnapsackInstance → ℕ → Std.Format

theorem Cslib.Complexity.encKnapsack_capacity_deg : Turing.MultiTapeTM.ComputableInDegree KnapsackInstance.capacity encKnapsack Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encKnapsack_items_inO : Turing.MultiTapeTM.ComputableInO KnapsackInstance.items encKnapsack (Turing.MultiTapeTM.encList Knapsack.encItem) (fun (a : KnapsackInstance) => (encKnapsack a).length) fun (a : KnapsackInstance) => (encKnapsack a).length

theorem Cslib.Complexity.encKnapsack_items_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → KnapsackInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encKnapsack → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).items) encIn✝ (Turing.MultiTapeTM.encList Knapsack.encItem)

theorem Cslib.Complexity.encKnapsack_capacity_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → KnapsackInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encKnapsack → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).capacity) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encKnapsack_goal_inO : Turing.MultiTapeTM.ComputableInO KnapsackInstance.goal encKnapsack Turing.MultiTapeTM.encNat (fun (a : KnapsackInstance) => (encKnapsack a).length) fun (a : KnapsackInstance) => (encKnapsack a).length

theorem Cslib.Complexity.encKnapsack_capacity_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → KnapsackInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encKnapsack S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).capacity) encIn✝ Turing.MultiTapeTM.encNat S✝

@[reducible, inline]

abbrev Cslib.Complexity.encKnapsackFields : List Knapsack.Item × ℕ × ℕ ↪ List Bool

The tuple of the fields of encKnapsack.

theorem Cslib.Complexity.encKnapsack_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List Knapsack.Item} {x1 x2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn (Turing.MultiTapeTM.encList Knapsack.encItem)) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { items := x0 x, capacity := x1 x, goal := x2 x }) encIn encKnapsack

theorem Cslib.Complexity.encKnapsack_goal_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → KnapsackInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encKnapsack → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).goal) encIn✝ Turing.MultiTapeTM.encNat

def Cslib.Complexity.encKnapsack : KnapsackInstance ↪ List Bool

Binary encoding of KnapsackInstance as (items, (capacity, goal)).

theorem Cslib.Complexity.encKnapsack_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : List Knapsack.Item × ℕ × ℕ) => { items := p.1, capacity := p.2.1, goal := p.2.2 }) encKnapsackFields encKnapsack 1 1

theorem Cslib.Complexity.encKnapsack_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List Knapsack.Item} {T0 S0 x1 T1 S1 x2 T2 S2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn (Turing.MultiTapeTM.encList Knapsack.encItem) T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn Turing.MultiTapeTM.encNat T2 S2) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { items := x0 x, capacity := x1 x, goal := x2 x }) encIn encKnapsack (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

@[simp]

theorem Cslib.Complexity.encKnapsack_apply (a : KnapsackInstance) : encKnapsack a = encKnapsackFields (a.items, a.capacity, a.goal)

theorem Cslib.Complexity.encKnapsack_goal_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → KnapsackInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encKnapsack S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).goal) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.encKnapsack_goal_deg : Turing.MultiTapeTM.ComputableInDegree KnapsackInstance.goal encKnapsack Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encKnapsack_items_deg : Turing.MultiTapeTM.ComputableInDegree KnapsackInstance.items encKnapsack (Turing.MultiTapeTM.encList Knapsack.encItem) 1 1

theorem Cslib.Complexity.encKnapsack_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → List Knapsack.Item} {x1 x2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn (Turing.MultiTapeTM.encList Knapsack.encItem) budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { items := x0 x, capacity := x1 x, goal := x2 x }) encIn encKnapsack budget

theorem Cslib.Complexity.encKnapsack_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : KnapsackInstance) => (a.items, a.capacity, a.goal)) encKnapsack encKnapsackFields 1 1

theorem Cslib.Complexity.encKnapsack_capacity_inO : Turing.MultiTapeTM.ComputableInO KnapsackInstance.capacity encKnapsack Turing.MultiTapeTM.encNat (fun (a : KnapsackInstance) => (encKnapsack a).length) fun (a : KnapsackInstance) => (encKnapsack a).length

theorem Cslib.Complexity.encKnapsack_items_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → KnapsackInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encKnapsack S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).items) encIn✝ (Turing.MultiTapeTM.encList Knapsack.encItem) S✝

def Cslib.Complexity.Knapsack : Set KnapsackInstance

The 0-1 knapsack problem: instances x : KnapsackInstance for which some sub-multiset of x.items has total weight at most x.capacity and total value at least x.goal Garey and Johnson.

theorem Cslib.Complexity.mem_Knapsack_iff_sublist {x : KnapsackInstance} : x ∈ Knapsack ↔ ∃ (s : List Knapsack.Item), s.Sublist x.items ∧ (List.map Knapsack.Item.weight s).sum ≤ x.capacity ∧ x.goal ≤ (List.map Knapsack.Item.value s).sum

Knapsack asks for a subsequence of the items.

def Cslib.Complexity.Knapsack.verifier : KnapsackInstance × List Bool → Bool

The verifier for Knapsack, a mask verifier (Cslib.Complexity.maskVerifier): the items selected by the certificate mask fit the capacity and reach the goal.

theorem Cslib.Complexity.Knapsack.isVerifier : IsVerifier encKnapsack Polynomial.X verifier Knapsack

Knapsack.verifier verifies Knapsack with certificates as long as the encoded instance.

theorem Cslib.Complexity.Knapsack.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encKnapsack Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The Knapsack verifier is polynomial-time: the sums and comparisons are in binary.

theorem Cslib.Complexity.Knapsack.mem_NP : Knapsack ∈ NP encKnapsack

Knapsack belongs to NP.

def Cslib.Complexity.SubsetSum.toKnapsack (x : SubsetSumInstance) : KnapsackInstance

The reduction from SubsetSum to Knapsack: each number becomes an item with equal weight and value, and the target becomes both the capacity and the goal.

theorem Cslib.Complexity.SubsetSum.toKnapsack_mem_iff (x : SubsetSumInstance) : toKnapsack x ∈ Knapsack ↔ x ∈ SubsetSum

Correctness of the reduction to Knapsack.

theorem Cslib.Complexity.SubsetSum.computableInPolyTime_toKnapsack : Turing.MultiTapeTM.ComputableInPolyTime toKnapsack encSubsetSum encKnapsack

The reduction to Knapsack is polynomial-time.

theorem Cslib.Complexity.polyTimeReducible_SubsetSum_Knapsack : PolyTimeReducible encSubsetSum encKnapsack SubsetSum Knapsack

SubsetSum reduces to Knapsack in polynomial time.

theorem Cslib.Complexity.Knapsack_npHard : NPHard encKnapsack Knapsack

Knapsack is NP-hard.

theorem Cslib.Complexity.Knapsack_npComplete : NPComplete encKnapsack Knapsack

The 0-1 knapsack problem is NP-complete, with all numbers in binary Garey and Johnson.