Knapsack problem

AbbreviationKnapsack instances#✓fully proved

A 0/1 knapsack instance is a triple \((I, C, T)\) of a list \(I\) of items, each a pair \((w, v)\) of natural numbers giving its weight \(w\) and value \(v\), a natural-number capacity \(C\), and a natural-number target value \(T\).

abbrev KnapsackInstance := List (ℕ × ℕ) × ℕ × ℕ

Used by 2

Used byThe KNAPSACK decision problem · Feasible knapsack instances

DefinitionFeasible knapsack instances#✓fully proved

A knapsack instance \((I, C, T)\), with item list \(I\), capacity \(C\) and target value \(T\), is feasible when some subsequence of \(I\), possibly empty, has total weight at most \(C\) and total value at least \(T\). Repeated items in \(I\) are distinct occurrences that can be selected separately.

def KnapsackFeasible
    (i : KnapsackInstance) : Prop :=
  ∃ chosen : List (ℕ × ℕ), chosen.Sublist i.1 ∧
    (chosen.map Prod.fst).sum ≤ i.2.1 ∧ i.2.2 ≤ (chosen.map Prod.snd).sum

Uses 1 · Used by 1

Statement usesKnapsack instances

Used byThe KNAPSACK decision problem

DefinitionThe KNAPSACK decision problem#✓fully proved

KNAPSACK is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a knapsack instance \((I, C, T)\) for which some subsequence of the item list \(I\), possibly empty, has total weight at most \(C\) and total value at least \(T\). Bitstrings that do not decode are rejected.

noncomputable def knapsackDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := KnapsackInstance) x with
  | some i => decide (KnapsackFeasible i)
  | none => false

Uses 11 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasible knapsack instances · Knapsack instances · Decision problems

Used byKNAPSACK is NP-complete

TheoremKNAPSACK is NP-complete#●ready to prove

The KNAPSACK decision problem is in NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

public theorem_wanted knapsack_npComplete :
    knapsackDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L knapsackDec

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness (1979), KNAPSACK (MP9).

Uses 5

Statement usesPolynomial-time many-one reduction · The KNAPSACK decision problem · Complexity classes · Decision problems · The complexity class NP

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.