Betweenness

AbbreviationBETWEENNESS instances#✓fully proved

An instance of BETWEENNESS is a pair \((n, T)\) of a natural number \(n\) (the number of elements) and a list \(T\) of triples of natural numbers.

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

Used by 3

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

DefinitionWell-formed BETWEENNESS instances#✓fully proved

A BETWEENNESS instance \((n, T)\) is well formed when every triple \((a, b, c)\) in \(T\) satisfies \(a < n\), \(b < n\) and \(c < n\), and \(a\), \(b\), \(c\) are pairwise distinct.

def WellFormed (i : BetweennessInstance) : Prop :=
  ∀ t ∈ i.2, t.1 < i.1 ∧ t.2.1 < i.1 ∧ t.2.2 < i.1 ∧ t.1 ≠ t.2.1 ∧ t.1 ≠ t.2.2 ∧ t.2.1 ≠ t.2.2

Uses 1 · Used by 1

Statement usesBETWEENNESS instances

Used byThe BETWEENNESS decision problem

DefinitionBETWEENNESS feasibility#✓fully proved

A BETWEENNESS instance \((n, T)\) is feasible when there is an ordering of the numbers \(0, \dots, n-1\) such that for every triple \((a, b, c)\) in \(T\), either \(p(a) < p(b) < p(c)\) or \(p(c) < p(b) < p(a)\), 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 BetweennessFeasible
    (i : BetweennessInstance) : Prop :=
  ∃ ord : List ℕ, ord.Perm (List.range i.1) ∧
    ∀ t ∈ i.2, (ord.idxOf t.1 < ord.idxOf t.2.1 ∧ ord.idxOf t.2.1 < ord.idxOf t.2.2) ∨
      (ord.idxOf t.2.2 < ord.idxOf t.2.1 ∧ ord.idxOf t.2.1 < ord.idxOf t.1)

Uses 1 · Used by 1

Statement usesBETWEENNESS instances

Used byThe BETWEENNESS decision problem

DefinitionThe BETWEENNESS decision problem#✓fully proved

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

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

Used byBETWEENNESS is NP-complete

TheoremBETWEENNESS is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), BETWEENNESS; M. Opatrny, "Total ordering problem" (1979).

Uses 5

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