Nonmetric k-median

Abbreviationk-median instances#✓fully proved

A k-median instance is a triple \((d, K, B)\) of a cost matrix \(d\), given as a list of rows of natural numbers (one row per client, one entry per location; the rows need not have equal length), a natural number \(K\) bounding the number of open locations, and a natural-number budget \(B\).

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

Used by 3

Used byThe k-MEDIAN decision problem · Feasible k-median instances · Well-formed k-median instances

DefinitionWell-formed k-median instances#✓fully proved

A k-median instance \((d, K, B)\) is well formed when all rows of its cost matrix \(d\) have the same length.

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

Uses 1 · Used by 1

Statement usesk-median instances

Used byThe k-MEDIAN decision problem

DefinitionFeasible k-median instances#✓fully proved

Let \((d, K, B)\) be a k-median instance whose cost matrix \(d\) has rows \(d_0, \dots, d_{n-1}\), one per client, and let \(m\) be the length of \(d_0\), or \(m = 0\) when \(n = 0\). The instance is feasible when there are a set \(S \subseteq \{0, \dots, m-1\}\) of at most \(K\) locations and a choice of \(a(c) \in S\) for each client \(c < n\) such that \(\sum_{c < n} d_c(a(c)) \le B\), where \(d_c(j)\) is the entry of \(d_c\) at index \(j\) (counting from \(0\)), read as \(0\) when \(d_c\) has fewer than \(j + 1\) entries.

def KMedianFeasible
    (i : KMedianInstance) : 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) ∧
      (Finset.range i.1.length).sum
        (fun c => (i.1.getD c []).getD (assign.getD c 0) 0) ≤ i.2.2

Uses 1 · Used by 1

Statement usesk-median instances

Used byThe k-MEDIAN decision problem

DefinitionThe k-MEDIAN decision problem#✓fully proved

The k-MEDIAN decision problem. k-MEDIAN (generalized, nonmetric) is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a k-median instance \((d, K, B)\) that is well formed and feasible. That is, \(d\) has rows \(d_0, \dots, d_{n-1}\) (the clients) of a common length \(m\) (the locations), and there are a set \(S \subseteq \{0, \dots, m-1\}\) of at most \(K\) locations and a choice of \(a(c) \in S\) for each client \(c < n\) with \(\sum_{c < n} d_{c, a(c)} \le B\). Bitstrings that do not decode are rejected.

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

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

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

The k-MEDIAN decision problem is in NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• O. Kariv and S. L. Hakimi, "An algorithmic approach to network location problems. II: The p-medians", SIAM Journal on Applied Mathematics 37 (1979), 539-560.

Uses 5

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