Facility location

AbbreviationFacility location instances#✓fully proved

A facility location instance is a triple \((o, D, B)\) made of a finite list \(o\) of natural numbers (the opening costs of the facilities), a finite list \(D\) of finite lists of natural numbers (the \(c\)-th list holds the costs of assigning client \(c\) to each facility), and a natural number \(B\) (the budget).

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

Used by 3

Used byThe FACILITY LOCATION decision problem · Feasible facility location instances · Well-formed facility location instances

DefinitionWell-formed facility location instances#✓fully proved

A facility location instance \((o, D, B)\), with opening costs \(o\) and assignment-cost rows \(D\), is well-formed when every row of \(D\) has the same length as \(o\).

def WellFormed (i : FacilityLocationInstance) : Prop :=
  ∀ row ∈ i.2.1, row.length = i.1.length

Uses 1 · Used by 1

Statement usesFacility location instances

Used byThe FACILITY LOCATION decision problem

DefinitionFeasible facility location instances#✓fully proved

Let \((o, D, B)\) be a facility location instance with opening costs \(o = (o_0, \dots, o_{n-1})\), assignment-cost rows \(D = (D_0, \dots, D_{m-1})\) and budget \(B\), and write \(D_{c,j}\) for the \(j\)-th entry of the row \(D_c\), read as \(0\) when \(D_c\) has no \(j\)-th entry. The instance is feasible when there is a map \(\sigma\) from the clients \(\{0, \dots, m-1\}\) to the facilities \(\{0, \dots, n-1\}\) such that the opening costs of the facilities in the image of \(\sigma\) plus the assignment costs stay within the budget: \(\sum_{j \in \sigma(\{0, \dots, m-1\})} o_j + \sum_{c=0}^{m-1} D_{c,\sigma(c)} \le B\).

def FacilityLocationFeasible
    (i : FacilityLocationInstance) : Prop :=
  ∃ assign : List ℕ, assign.length = i.2.1.length ∧
    (∀ c < i.2.1.length, assign.getD c 0 < i.1.length) ∧
    ∃ used : List ℕ, used.Nodup ∧
      (∀ f ∈ used, ∃ c < i.2.1.length, assign.getD c 0 = f) ∧
      (∀ c < i.2.1.length, assign.getD c 0 ∈ used) ∧
      (used.map (fun f => i.1.getD f 0)).sum +
        (Finset.range i.2.1.length).sum
          (fun c => (i.2.1.getD c []).getD (assign.getD c 0) 0) ≤ i.2.2

Uses 1 · Used by 1

Statement usesFacility location instances

Used byThe FACILITY LOCATION decision problem

DefinitionThe FACILITY LOCATION decision problem#✓fully proved

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

noncomputable def facilityLocationDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := FacilityLocationInstance) x with
  | some i => decide (WellFormed i ∧ FacilityLocationFeasible 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 facility location instances · Facility location instances · Well-formed facility location instances · Decision problems

Used byFACILITY LOCATION is NP-complete

TheoremFACILITY LOCATION is NP-complete#●ready to prove

FACILITY LOCATION belongs to NP, and every decision problem \(L\) in NP reduces to FACILITY LOCATION by a polynomial-time many-one reduction: there is a polynomial-time computable map \(f\) on bitstrings such that, for every bitstring \(x\), \(L\) accepts \(x\) exactly when FACILITY LOCATION accepts \(f(x)\).

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

Sources

• G. Cornuéjols, G. L. Nemhauser, and L. A. Wolsey, "The uncapacitated facility location problem", in P. B. Mirchandani and R. L. Francis, eds., Discrete Location Theory, Wiley, 1990, 119-171.

Uses 5

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