Directed s-t connectivity

DefinitionDirected \(s\)-\(t\) connectivity#✓fully proved

The decision problem of directed \(s\)-\(t\) connectivity accepts a bitstring \(x\) exactly when decoding \(x\) with the canonical bitstring encoding of tuples \((n, E, s, t)\), where \(n\), \(s\) and \(t\) are natural numbers and \(E\) is a list of pairs of natural numbers, succeeds and gives a tuple such that \(s < n\), \(t < n\), and there are pairwise distinct natural numbers \(v_0, \dots, v_k\), all less than \(n\), with \(v_0 = s\), \(v_k = t\) and \((v_j, v_{j+1}) \in E\) for every \(j < k\). Bitstrings that do not decode are rejected.

noncomputable def stconDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ℕ × List (ℕ × ℕ) × ℕ × ℕ) x with
  | some i => decide (i.2.2.1 < i.1 ∧ i.2.2.2 < i.1 ∧
      ∃ path : List ℕ, path.Nodup ∧
      path.getD 0 0 = i.2.2.1 ∧
      path.getD (path.length - 1) 0 = i.2.2.2 ∧
      (∀ v ∈ path, v < i.1) ∧
      ∀ j, j + 1 < path.length →
        (path.getD j 0, path.getD (j + 1) 0) ∈ i.2.1)
  | none => false

Uses 9 · 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 · Decision problems

Used byST-connectivity is NL-complete

TheoremST-connectivity is NL-complete#●ready to prove

Directed \(s\)-\(t\) connectivity is in NL, and every decision problem in NL is log-space many-one reducible to directed \(s\)-\(t\) connectivity.

public theorem_wanted stcon_nl_complete :
    stconDec ∈ NL ∧ ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ NL → LogSpaceRed L stconDec

Sources

• S. A. Cook, "A hierarchy for nondeterministic time complexity" (1973) and the standard NL-completeness of directed reachability; see S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Chapter 4, and C. H. Papadimitriou, Computational Complexity, 1994, Theorem 7.3.

Uses 5

Statement usesLog-space many-one reductions · The complexity class NL · Directed \(s\)-\(t\) connectivity · Complexity classes · Decision problems

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.