Undirected s-t connectivity

DefinitionUndirected s-t connectivity as a decision problem#✓fully proved

A bitstring \(x\) is a yes-instance exactly when bitstring decoding of \(x\), as a tuple \((n, E, s, t)\) of natural numbers \(n\), \(s\), \(t\) and a finite list \(E\) of pairs of natural numbers, succeeds and returns \((n, E, s, t)\) 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, for every \(i < k\), \((v_i, v_{i+1}) \in E\) or \((v_{i+1}, v_i) \in E\).

noncomputable def ustconDec :
    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 ∨
          (path.getD (j + 1) 0, path.getD j 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 byUndirected ST-connectivity is in L (Reingold)

TheoremUndirected ST-connectivity is in L (Reingold)#●ready to prove

The undirected \(s\)-\(t\) connectivity decision problem lies in the class \(\mathsf{L}\) of decision problems decidable in deterministic logarithmic space.

public theorem_wanted ustcon_in_l :
    ustconDec ∈ LogSpace

Sources

• O. Reingold, "Undirected connectivity in log-space", Journal of the ACM 55 (2008), 1-24 (STOC 2005).

Uses 4

Statement usesDeterministic logarithmic space · Undirected s-t connectivity as a decision problem · Complexity classes · Decision problems

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.