Bin packing

AbbreviationBin packing instances#✓fully proved

An instance of BIN PACKING is a triple \((s, B, K)\) of a finite list \(s\) of natural numbers (the item sizes), a natural number \(B\) (the bin capacity) and a natural number \(K\) (the number of bins).

abbrev BinPackingInstance := List ℕ × ℕ × ℕ

Used by 2

Used byThe bin packing decision problem · Feasible bin packing instances

DefinitionFeasible bin packing instances#✓fully proved

An instance \((s, B, K)\) of BIN PACKING is feasible when there is a list of exactly \(K\) bins, each a finite list of natural numbers with sum at most \(B\), such that the concatenation of the bins is a permutation of \(s\).

Since bins may be empty, this says that the items fit into at most \(K\) bins of capacity \(B\).

def BinPackingFeasible
    (i : BinPackingInstance) : Prop :=
  ∃ bins : List (List ℕ), bins.length = i.2.2 ∧ bins.flatten.Perm i.1 ∧
    ∀ bin ∈ bins, bin.sum ≤ i.2.1

Uses 1 · Used by 1

Statement usesBin packing instances

Used byThe bin packing decision problem

DefinitionThe bin packing decision problem#✓fully proved

BIN PACKING is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of bin packing instances, to a feasible instance; it rejects every bitstring that fails to decode.

noncomputable def binPackingDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := BinPackingInstance) x with
  | some i => decide (BinPackingFeasible 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 bin packing instances · Bin packing instances · Decision problems

Used byBIN PACKING is NP-complete

TheoremBIN PACKING is NP-complete#●ready to prove

The bin packing decision problem belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), BIN PACKING; D. S. Johnson, "Fast algorithms for bin packing" (1974).

Uses 5

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