Set cover

AbbreviationSet-cover instances#✓fully proved

A set-cover 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 SetCoverInstance := ℕ × List (List ℕ) × ℕ

Used by 3

Used byThe SET COVER decision problem · Feasible set-cover instances · Well-formed set-cover instances

DefinitionWell-formed set-cover instances#✓fully proved

A set-cover 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 : SetCoverInstance) : Prop :=
  ∀ s ∈ i.2.1, s.Nodup ∧ ∀ x ∈ s, x < i.1

Uses 1 · Used by 1

Statement usesSet-cover instances

Used byThe SET COVER decision problem

DefinitionFeasible set-cover instances#✓fully proved

A set-cover 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 at most \(K\) entries such that every natural number \(x < n\) belongs to some list in \(D\).

def SetCoverFeasible
    (i : SetCoverInstance) : Prop :=
  ∃ sub : List (List ℕ), sub.Sublist i.2.1 ∧ sub.length ≤ i.2.2 ∧
    ∀ x < i.1, ∃ s ∈ sub, x ∈ s

Uses 1 · Used by 1

Statement usesSet-cover instances

Used byThe SET COVER decision problem

DefinitionThe SET COVER decision problem#✓fully proved

SET COVER is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a set-cover 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 at most \(K\) entries contains every natural number \(y < n\) in one of its lists. Bitstrings that do not decode to a set-cover instance are rejected.

noncomputable def setCoverDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := SetCoverInstance) x with
  | some i => decide (WellFormed i ∧ SetCoverFeasible 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-cover instances · Set-cover instances · Well-formed set-cover instances · Decision problems

Used bySET COVER is NP-complete

TheoremSET COVER is NP-complete#●ready to prove

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

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

Sources

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

Uses 5

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