Quadratic assignment problem

AbbreviationInstances of QUADRATIC ASSIGNMENT#✓fully proved

An instance of quadratic assignment is a tuple \((n, F, D, K)\) consisting of a natural number \(n\) (the size), a flow matrix \(F\) and a distance matrix \(D\), each given as a list of rows that are lists of natural numbers, and a natural number \(K\) (the cost bound).

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

Used by 3

Used byQUADRATIC ASSIGNMENT as a decision problem · Feasible quadratic assignment instances · Well-formed quadratic assignment instances

DefinitionWell-formed quadratic assignment instances#✓fully proved

An instance \((n, F, D, K)\) of quadratic assignment is well formed when the flow matrix \(F\) and the distance matrix \(D\) each have exactly \(n\) rows and every row of each has length \(n\).

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

Uses 1 · Used by 1

Statement usesInstances of QUADRATIC ASSIGNMENT

Used byQUADRATIC ASSIGNMENT as a decision problem

DefinitionFeasible quadratic assignment instances#✓fully proved

An instance \((n, F, D, K)\) of quadratic assignment is feasible when there is a permutation \(\pi\) of the numbers \(0, \dots, n - 1\) such that

\[ \sum_{a < n} \sum_{b < n} F_{a b} \, D_{\pi(a) \pi(b)} \le K. \]

Here \(F_{a b}\) is entry \(b\) of row \(a\) of \(F\), and likewise for \(D\); an entry that is missing, because the matrix has too few rows or the row is too short, is read as \(0\).

def QuadraticAssignmentFeasible
    (i : QuadraticAssignmentInstance) : Prop :=
  ∃ perm : List ℕ, perm.Perm (List.range i.1) ∧
    (Finset.range i.1).sum (fun a => (Finset.range i.1).sum (fun b =>
      (i.2.1.getD a []).getD b 0 *
        (i.2.2.1.getD (perm.getD a 0) []).getD (perm.getD b 0) 0)) ≤ i.2.2.2

Uses 1 · Used by 1

Statement usesInstances of QUADRATIC ASSIGNMENT

Used byQUADRATIC ASSIGNMENT as a decision problem

DefinitionQUADRATIC ASSIGNMENT as a decision problem#✓fully proved

The decision problem QUADRATIC ASSIGNMENT accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a quadratic assignment instance that is well formed and feasible; bitstrings that do not decode are rejected.

noncomputable def quadraticAssignmentDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := QuadraticAssignmentInstance) x with
  | some i => decide (WellFormed i ∧ QuadraticAssignmentFeasible 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 quadratic assignment instances · Instances of QUADRATIC ASSIGNMENT · Well-formed quadratic assignment instances · Decision problems

Used byQUADRATIC ASSIGNMENT is NP-complete

TheoremQUADRATIC ASSIGNMENT is NP-complete#●ready to prove

The decision problem QUADRATIC ASSIGNMENT lies in NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), QUADRATIC ASSIGNMENT PROBLEM; S. Sahni and T. Gonzalez, "P-complete approximation problems" (1976).

Uses 5

Statement usesPolynomial-time many-one reduction · QUADRATIC ASSIGNMENT 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.