Achromatic number

AbbreviationInstances of ACHROMATIC NUMBER#✓fully proved

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

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

Used by 3

Used byACHROMATIC NUMBER as a decision problem · Feasible ACHROMATIC NUMBER instances · Well-formed ACHROMATIC NUMBER instances

DefinitionWell-formed ACHROMATIC NUMBER instances#✓fully proved

An instance \((n, E, K)\) of ACHROMATIC NUMBER is well-formed when the list \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin E\).

def WellFormed (i : AchromaticNumberInstance) : 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 usesInstances of ACHROMATIC NUMBER

Used byACHROMATIC NUMBER as a decision problem

DefinitionFeasible ACHROMATIC NUMBER instances#✓fully proved

An instance \((n, E, K)\) of ACHROMATIC NUMBER is feasible when there are a natural number \(q \ge K\) and a list \(c = (c_0, \dots, c_{n-1})\) of \(n\) natural numbers, with \(c_u\) read as \(0\) for \(u \ge n\), such that \(c_v < q\) for every \(v < n\), every \(a < q\) equals \(c_v\) for some \(v < n\), \(c_u \ne c_v\) for every pair \((u, v)\) in \(E\), and for all distinct \(a, b < q\) some pair \((u, v)\) in \(E\) has \((c_u, c_v) = (a, b)\) or \((c_u, c_v) = (b, a)\).

def AchromaticNumberFeasible
    (i : AchromaticNumberInstance) : Prop :=
  ∃ q : ℕ, i.2.2 ≤ q ∧
    ∃ coloring : List ℕ, coloring.length = i.1 ∧ (∀ v < i.1, coloring.getD v 0 < q) ∧
    (∀ c < q, ∃ v < i.1, coloring.getD v 0 = c) ∧
    (∀ e ∈ i.2.1, coloring.getD e.1 0 ≠ coloring.getD e.2 0) ∧
    ∀ a < q, ∀ b < q, a ≠ b → ∃ e ∈ i.2.1,
      (coloring.getD e.1 0 = a ∧ coloring.getD e.2 0 = b) ∨
      (coloring.getD e.1 0 = b ∧ coloring.getD e.2 0 = a)

Uses 1 · Used by 1

Statement usesInstances of ACHROMATIC NUMBER

Used byACHROMATIC NUMBER as a decision problem

DefinitionACHROMATIC NUMBER as a decision problem#✓fully proved

The ACHROMATIC NUMBER decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of instances \((n, E, K)\), to an instance of ACHROMATIC NUMBER that is well-formed and feasible; it rejects every bitstring that does not decode to an instance.

noncomputable def achromaticNumberDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := AchromaticNumberInstance) x with
  | some i => decide (WellFormed i ∧ AchromaticNumberFeasible 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 ACHROMATIC NUMBER instances · Instances of ACHROMATIC NUMBER · Well-formed ACHROMATIC NUMBER instances · Decision problems

Used byACHROMATIC NUMBER is NP-complete

TheoremACHROMATIC NUMBER is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), ACHROMATIC NUMBER; M. Farber et al., "The achromatic number of graphs" (1986).

Uses 5

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