The 0-1 knapsack problem #

Knapsack is the decision version of the 0-1 knapsack problem: given items, each with a weight and a value, a capacity and a goal, some sub-multiset of the items has total weight at most the capacity and total value at least the goal [GJ79]. All numbers are encoded in binary (encNat); the verifier compares the sums in binary (ComputableTidilyInPolyTime.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 #

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 #

source

def Cslib.Complexity.Knapsack :

Set (List (ℕ × ℕ) × ℕ × ℕ)

Instances (items, capacity, goal) of the 0-1 knapsack problem, items given as (weight, value): some sub-multiset of the items has total weight at most the capacity and total value at least the goal Garey and Johnson.

Instances For

source

@[reducible, inline]

abbrev Cslib.Complexity.encKnapsack :

List (ℕ × ℕ) × ℕ × ℕ ↪ List Bool

Knapsack instances, with all numbers in binary.

Instances For

source

theorem Cslib.Complexity.mem_Knapsack_iff_sublist {x : List (ℕ × ℕ) × ℕ × ℕ} :

x ∈ Knapsack ↔ ∃ (s : List (ℕ × ℕ)), s.Sublist x.1 ∧ (List.map Prod.fst s).sum ≤ x.2.1 ∧ x.2.2 ≤ (List.map Prod.snd s).sum

Knapsack asks for a subsequence of the items.

source

def Cslib.Complexity.Knapsack.verifier (x : (List (ℕ × ℕ) × ℕ × ℕ) × List Bool) :

Bool

The verifier for Knapsack: the items selected by the certificate mask fit the capacity and reach the goal.

Instances For

source

theorem Cslib.Complexity.Knapsack.isVerifier :

IsVerifier encKnapsack Polynomial.X verifier Knapsack

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

source

theorem Cslib.Complexity.Knapsack.computableTidilyInPolyTime_verifier :

Turing.MultiTapeTM.ComputableTidilyInPolyTime verifier (Turing.MultiTapeTM.encPair encKnapsack Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

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

source

theorem Cslib.Complexity.Knapsack.mem_NP :

Knapsack ∈ NP encKnapsack

Knapsack belongs to NP.

source

def Cslib.Complexity.SubsetSum.toKnapsack (x : List ℕ × ℕ) :

List (ℕ × ℕ) × ℕ × ℕ

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.

Instances For

source