Nonmetric k-center

Abbreviationk-center instances#✓fully proved

An instance of generalized nonmetric k-center is a triple \((D, K, B)\) of a finite list \(D\) of rows, each a finite list of natural numbers (row \(c\) lists the costs from client \(c\) to the locations), and natural numbers \(K\), the bound on the number of locations, and \(B\), the radius.

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

Used by 3

Used byGeneralized nonmetric k-center as a decision problem · Feasible k-center instances · Well-formed k-center instances

DefinitionWell-formed k-center instances#✓fully proved

A k-center instance \((D, K, B)\) is well formed when all rows of \(D\) have the same length.

def WellFormed (i : KCenterInstance) : Prop :=
  ∀ row ∈ i.1, ∀ row' ∈ i.1, row.length = row'.length

Uses 1 · Used by 1

Statement usesk-center instances

Used byGeneralized nonmetric k-center as a decision problem

DefinitionFeasible k-center instances#✓fully proved

Let \((D, K, B)\) be a k-center instance with rows \(D_0, \dots, D_{m-1}\), and let \(n\) be the length of \(D_0\), with \(n = 0\) if \(m = 0\). For \(c < m\) and a natural number \(f\), write \(D_c(f)\) for the entry of \(D_c\) at position \(f\), counting from \(0\), and set \(D_c(f) = 0\) if \(D_c\) has at most \(f\) entries. The instance is feasible when there is a set \(S\) of at most \(K\) locations \(f < n\) such that every client \(c < m\) has some \(f \in S\) with \(D_c(f) \le B\).

def KCenterFeasible
    (i : KCenterInstance) : Prop :=
  ∃ facilities : List ℕ, facilities.Nodup ∧ facilities.length ≤ i.2.1 ∧
    (∀ f ∈ facilities, f < (i.1.getD 0 []).length) ∧
    ∃ assign : List ℕ, assign.length = i.1.length ∧
      ∀ c < i.1.length, assign.getD c 0 ∈ facilities ∧
        (i.1.getD c []).getD (assign.getD c 0) 0 ≤ i.2.2

Uses 1 · Used by 1

Statement usesk-center instances

Used byGeneralized nonmetric k-center as a decision problem

DefinitionGeneralized nonmetric k-center as a decision problem#✓fully proved

This decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a k-center instance that is well formed and feasible; bitstrings that do not decode to an instance are rejected.

noncomputable def kCenterDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := KCenterInstance) x with
  | some i => decide (WellFormed i ∧ KCenterFeasible 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 k-center instances · k-center instances · Well-formed k-center instances · Decision problems

Used byk-CENTER (GENERALIZED, NONMETRIC) is NP-complete

Theoremk-CENTER (GENERALIZED, NONMETRIC) is NP-complete#●ready to prove

The decision problem of generalized nonmetric k-center on bitstrings is NP-complete: it belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• O. Kariv and S. L. Hakimi, "An algorithmic approach to network location problems. I: The p-centers", SIAM Journal on Applied Mathematics 37 (1979), 513-538.

Uses 5

Statement usesPolynomial-time many-one reduction · Generalized nonmetric k-center as a 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.