Maximum coverage

AbbreviationMaximum-coverage instances#✓fully proved

A maximum-coverage instance is a tuple \((n, S, K, M)\) of a natural number \(n\) (the universe size), a list \(S\) of lists of natural numbers (the subsets), a natural number \(K\) (the set budget) and a natural number \(M\) (the coverage target).

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

Used by 3

Used byThe MAXIMUM COVERAGE decision problem · Feasible maximum-coverage instances · Well-formed maximum-coverage instances

DefinitionWell-formed maximum-coverage instances#✓fully proved

A maximum-coverage instance \((n, S, K, M)\) is well formed when every subset in the list \(S\) has no repeated elements and all of its elements are less than \(n\).

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

Uses 1 · Used by 1

Statement usesMaximum-coverage instances

Used byThe MAXIMUM COVERAGE decision problem

DefinitionFeasible maximum-coverage instances#✓fully proved

A maximum-coverage instance \((n, S, K, M)\), with universe size \(n\), list of subsets \(S\), set budget \(K\) and coverage target \(M\), is feasible when there are a sublist \(T\) of \(S\) with at most \(K\) entries and a list of at least \(M\) pairwise distinct natural numbers, each less than \(n\) and each belonging to some subset in \(T\).

def MaximumCoverageFeasible
    (i : MaximumCoverageInstance) : Prop :=
  ∃ T : List (List ℕ), T.Sublist i.2.1 ∧ T.length ≤ i.2.2.1 ∧
    ∃ covered : List ℕ, covered.Nodup ∧ i.2.2.2 ≤ covered.length ∧
      ∀ x ∈ covered, x < i.1 ∧ ∃ s ∈ T, x ∈ s

Uses 1 · Used by 1

Statement usesMaximum-coverage instances

Used byThe MAXIMUM COVERAGE decision problem

DefinitionThe MAXIMUM COVERAGE decision problem#✓fully proved

MAXIMUM COVERAGE is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a maximum-coverage instance \((n, S, K, M)\) that is well formed and feasible: every subset in the list \(S\) has no repeated elements and only elements less than \(n\), and some sublist of \(S\) with at most \(K\) entries covers at least \(M\) distinct elements less than \(n\). Bitstrings that do not decode are rejected.

noncomputable def maximumCoverageDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MaximumCoverageInstance) x with
  | some i => decide (WellFormed i ∧ MaximumCoverageFeasible 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 maximum-coverage instances · Maximum-coverage instances · Well-formed maximum-coverage instances · Decision problems

Used byMAXIMUM COVERAGE is NP-complete

TheoremMAXIMUM COVERAGE is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), SET COVER: maximum coverage with target M = n is exactly set cover (at most K sets covering all n elements).

Uses 5

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