Graph bandwidth

AbbreviationBANDWIDTH instances#✓fully proved

An instance of BANDWIDTH is a triple \((n, E, K)\) of a natural number \(n\) (the number of vertices), a list \(E\) of ordered pairs of natural numbers (the edges) and a natural number \(K\) (the bound).

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

Used by 3

Used byThe BANDWIDTH decision problem · BANDWIDTH feasibility · Well-formed BANDWIDTH instances

DefinitionWell-formed BANDWIDTH instances#✓fully proved

A BANDWIDTH instance \((n, E, K)\) is well formed when the list \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), and its reverse \((v, u)\) does not occur in \(E\). Thus \(E\) lists the edges of a loopless undirected graph on the vertices \(0, \dots, n-1\), each edge exactly once.

def WellFormed (i : BandwidthInstance) : Prop :=
  i.2.1.Nodup ∧ ∀ e ∈ i.2.1, e.1 < i.1 ∧ e.2 < i.1 ∧ e.1 ≠ e.2 ∧ (e.2, e.1) ∉ i.2.1

Uses 1 · Used by 1

Statement usesBANDWIDTH instances

Used byThe BANDWIDTH decision problem

DefinitionBANDWIDTH feasibility#✓fully proved

A BANDWIDTH instance \((n, E, K)\) is feasible when there is an ordering of the numbers \(0, \dots, n-1\) such that \(|p(u) - p(v)| \le K\) for every pair \((u, v)\) in \(E\), where \(p(m)\) is the position of \(m\) in the ordering, counting from \(0\), and \(p(m) = n\) when \(m\) is not among \(0, \dots, n-1\).

def BandwidthFeasible
    (i : BandwidthInstance) : Prop :=
  ∃ perm : List ℕ, perm.Perm (List.range i.1) ∧
    ∀ e ∈ i.2.1, Nat.dist (perm.idxOf e.1) (perm.idxOf e.2) ≤ i.2.2

Uses 1 · Used by 1

Statement usesBANDWIDTH instances

Used byThe BANDWIDTH decision problem

DefinitionThe BANDWIDTH decision problem#✓fully proved

BANDWIDTH accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of triples \((n, E, K)\) of a natural number, a list of pairs of natural numbers and a natural number, to a BANDWIDTH instance that is both well formed and feasible. Bitstrings that do not decode to such a triple are rejected.

noncomputable def bandwidthDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := BandwidthInstance) x with
  | some i => decide (WellFormed i ∧ BandwidthFeasible 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 · BANDWIDTH feasibility · BANDWIDTH instances · Well-formed BANDWIDTH instances · Decision problems

Used byBANDWIDTH is NP-complete

TheoremBANDWIDTH is NP-complete#●ready to prove

The BANDWIDTH decision problem belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), BANDWIDTH; C. H. Papadimitriou, "The NP-completeness of the bandwidth minimization problem" (1976).

Uses 5

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