Set packing

AbbreviationSet-packing instances#✓fully proved

A set-packing instance is a triple \((n, C, K)\) consisting of a natural number \(n\), the size of the universe, a finite list \(C\) of finite lists of natural numbers, the subsets, and a natural number \(K\), the bound.

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

Used by 3

Used byThe SET PACKING decision problem · Feasible set-packing instances · Well-formed set-packing instances

DefinitionWell-formed set-packing instances#✓fully proved

A set-packing instance \((n, C, K)\) is well formed when every list \(s\) in \(C\) has no repeated entries and every entry of \(s\) is less than \(n\), that is, each member of \(C\) lists the elements of a subset of \(\{0, \dots, n - 1\}\) without repetition.

def WellFormed (i : SetPackingInstance) : Prop :=
  ∀ s ∈ i.2.1, s.Nodup ∧ ∀ x ∈ s, x < i.1

Uses 1 · Used by 1

Statement usesSet-packing instances

Used byThe SET PACKING decision problem

DefinitionFeasible set-packing instances#✓fully proved

A set-packing instance \((n, C, K)\) is feasible when there is a sublist \(D\) of \(C\) (a list obtained from \(C\) by deleting entries while keeping their order) with no repeated entries and at least \(K\) entries such that any two distinct entries of \(D\) have no element in common.

In particular two copies of the same list, even of the empty list, cannot both be chosen.

def SetPackingFeasible
    (i : SetPackingInstance) : Prop :=
  ∃ sub : List (List ℕ), sub.Sublist i.2.1 ∧ sub.Nodup ∧ i.2.2 ≤ sub.length ∧
    ∀ s1 ∈ sub, ∀ s2 ∈ sub, s1 ≠ s2 → ∀ x, x ∈ s1 → x ∉ s2

Uses 1 · Used by 1

Statement usesSet-packing instances

Used byThe SET PACKING decision problem

DefinitionThe SET PACKING decision problem#✓fully proved

SET PACKING is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a set-packing instance \((n, C, K)\) that is both well formed and feasible: every list in \(C\) has no repeated entries and only entries less than \(n\), and some sublist of \(C\) with no repeated entries and at least \(K\) entries has no element in common between any two of its distinct entries. Bitstrings that do not decode to a set-packing instance are rejected.

noncomputable def setPackingDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := SetPackingInstance) x with
  | some i => decide (WellFormed i ∧ SetPackingFeasible i)
  | none => false

Uses 12 · 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 set-packing instances · Set-packing instances · Well-formed set-packing instances · Decision problems

Used bySET PACKING is NP-complete

TheoremSET PACKING is NP-complete#●ready to prove

The SET PACKING decision problem lies in NP, and every decision problem \(L\) in NP has a polynomial-time many-one reduction to SET PACKING.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), SET PACKING; R. M. Karp, "Reducibility among combinatorial problems" (1972).

Uses 5

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

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.