Maximum n-times coverage

AbbreviationInstance of maximum n-times coverage#✓fully proved

An instance: n, the coverage rows of the overlays, element weights, k, τ.

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

Used by 3

Used byFeasibility for maximum n-times coverage · Maximum n-times coverage decision problem · Well-formed maximum n-times coverage instance

DefinitionWell-formed maximum n-times coverage instance#✓fully proved

Well-formedness: every row has one entry per element.

def WellFormed (i : Instance) : Prop :=
  ∀ row ∈ i.2.1, row.length = i.2.2.1.length

Uses 1 · Used by 1

Statement usesInstance of maximum n-times coverage

Used byMaximum n-times coverage decision problem

DefinitionWeight covered at least n times#✓fully proved

The weight of the elements covered at least n times by the rows sub.

def coveredWeight (n : ℕ) (sub : List (List ℕ)) (weights : List ℕ) : ℕ :=
  ((List.range weights.length).filter fun e => n ≤ (sub.map fun row => row.getD e 0).sum).foldr
    (fun e acc => weights.getD e 0 + acc) 0

Used by 1

Used byFeasibility for maximum n-times coverage

DefinitionFeasibility for maximum n-times coverage#✓fully proved

At most k overlays cover weight at least τ at least n times.

def Feasible (i : Instance) : Prop :=
  ∃ sub : List (List ℕ), sub.Sublist i.2.1 ∧ sub.length ≤ i.2.2.2.1 ∧
    i.2.2.2.2 ≤ coveredWeight i.1 sub i.2.2.1

Uses 2 · Used by 1

Statement usesInstance of maximum n-times coverage · Weight covered at least n times

Used byMaximum n-times coverage decision problem

DefinitionMaximum n-times coverage decision problem#✓fully proved

MAXIMUM n-TIMES COVERAGE as a decision problem over bitstrings.

noncomputable def maxNTimesCoverageDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode (α := Instance) x with
  | some i => decide (WellFormed i ∧ Feasible 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 · Feasibility for maximum n-times coverage · Instance of maximum n-times coverage · Well-formed maximum n-times coverage instance · Decision problems

Used byMAXIMUM n-TIMES COVERAGE is NP-complete

TheoremMAXIMUM n-TIMES COVERAGE is NP-complete#●ready to prove

MAXIMUM n-TIMES COVERAGE is NP-complete (Liu, Dimitrakakis, Carter and Gifford 2022).

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

Uses 5

Statement usesPolynomial-time many-one reduction · Maximum n-times coverage decision problem · Complexity classes · Decision problems · The complexity class NP

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.