Multiple knapsack problem

AbbreviationMultiple-knapsack instances#✓fully proved

A multiple-knapsack instance consists of a finite list of items, each a pair \((w, v)\) of natural numbers giving its weight \(w\) and value \(v\), a finite list of natural-number knapsack capacities, and a natural-number target value.

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

Used by 2

Used byMULTIPLE KNAPSACK as a decision problem · Feasible multiple-knapsack instances

DefinitionFeasible multiple-knapsack instances#✓fully proved

Let a multiple-knapsack instance have items \((w_0, v_0), \dots, (w_{k-1}, v_{k-1})\) (weight, value), knapsack capacities \(c_0, \dots, c_{m-1}\) and target \(V\). The instance is feasible when there are \(a_0, \dots, a_{k-1} \in \{0, \dots, m\}\), where \(a_j = b < m\) puts item \(j\) in knapsack \(b\) and \(a_j = m\) leaves item \(j\) out, such that for every \(b < m\) the total weight \(\sum_{j : a_j = b} w_j\) is at most \(c_b\), and the total value \(\sum_{j : a_j < m} v_j\) is at least \(V\).

def MultipleKnapsackFeasible
    (i : MultipleKnapsackInstance) : Prop :=
  ∃ assign : List ℕ, assign.length = i.1.length ∧
    (∀ j < i.1.length, assign.getD j 0 ≤ i.2.1.length) ∧
    (∀ b < i.2.1.length,
      (Finset.range i.1.length).sum (fun j =>
        if assign.getD j 0 = b then (i.1.getD j (0, 0)).1 else 0) ≤
        i.2.1.getD b 0) ∧
    i.2.2 ≤ (Finset.range i.1.length).sum (fun j =>
      if assign.getD j 0 < i.2.1.length then (i.1.getD j (0, 0)).2 else 0)

Uses 1 · Used by 1

Statement usesMultiple-knapsack instances

Used byMULTIPLE KNAPSACK as a decision problem

DefinitionMULTIPLE KNAPSACK as a decision problem#✓fully proved

The decision problem MULTIPLE KNAPSACK accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a feasible multiple-knapsack instance. Bitstrings that do not decode are rejected.

noncomputable def multipleKnapsackDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MultipleKnapsackInstance) x with
  | some i => decide (MultipleKnapsackFeasible 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 multiple-knapsack instances · Multiple-knapsack instances · Decision problems

Used byMULTIPLE KNAPSACK is NP-complete

TheoremMULTIPLE KNAPSACK is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), MULTIPLE KNAPSACK.

Uses 5

Statement usesPolynomial-time many-one reduction · MULTIPLE KNAPSACK as a 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.