Unbounded knapsack problem

AbbreviationUnbounded knapsack instances#✓fully proved

An instance of the unbounded knapsack problem is a triple \((I, C, K)\) of a finite list \(I = ((s_1, v_1), \dots, (s_m, v_m))\) of items, where item \(j\) has weight \(s_j \in \mathbb{N}\) and value \(v_j \in \mathbb{N}\), a capacity \(C \in \mathbb{N}\) and a target value \(K \in \mathbb{N}\).

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

Used by 2

Used byUnbounded knapsack as a decision problem · Feasible unbounded knapsack instances

DefinitionFeasible unbounded knapsack instances#✓fully proved

An unbounded knapsack instance with items \((s_1, v_1), \dots, (s_m, v_m)\), capacity \(C\) and target value \(K\) is feasible when there are multiplicities \(c_1, \dots, c_m \in \mathbb{N}\) with \(\sum_{j=1}^{m} c_j s_j \le C\) and \(\sum_{j=1}^{m} c_j v_j \ge K\).

def UnboundedKnapsackFeasible
    (i : UnboundedKnapsackInstance) : Prop :=
  ∃ mult : List ℕ, mult.length = i.1.length ∧
    (Finset.range i.1.length).sum
      (fun j => mult.getD j 0 * (i.1.getD j (0, 0)).1) ≤ i.2.1 ∧
    i.2.2 ≤ (Finset.range i.1.length).sum
      (fun j => mult.getD j 0 * (i.1.getD j (0, 0)).2)

Uses 1 · Used by 1

Statement usesUnbounded knapsack instances

Used byUnbounded knapsack as a decision problem

DefinitionUnbounded knapsack as a decision problem#✓fully proved

The unbounded knapsack problem is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of unbounded knapsack instances, to a feasible instance. Bitstrings that fail to decode are rejected.

noncomputable def unboundedKnapsackDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := UnboundedKnapsackInstance) x with
  | some i => decide (UnboundedKnapsackFeasible 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 unbounded knapsack instances · Unbounded knapsack instances · Decision problems

Used byUNBOUNDED KNAPSACK is NP-complete

TheoremUNBOUNDED KNAPSACK is NP-complete#●ready to prove

The unbounded knapsack decision problem belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

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

Uses 5

Statement usesPolynomial-time many-one reduction · Unbounded 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.