Undirected s–t connectivity

An instance of undirected s–t connectivity (Cslib.Complexity.USTCONInstance) is a simple graph on Fin n, given by its adjacency matrix, symmetric and with zero diagonal, together with two vertices s and t; it belongs to Cslib.Complexity.USTCON when t is reachable from s Arora and Barak, Section 21.4 Reingold, Section 4.

Instances are encoded (Cslib.Complexity.encUSTCON) as their directed graphs (Cslib.Complexity.USTCONInstance.toSTCONInstance, encoded by Cslib.Complexity.encSTCON): the unary header 1^n 0 1^s 0 1^t 0 followed by the adjacency matrix, row by row, so that the bit at n + s + t + 3 + a * n + b is the entry of the row a and the column b. The matrix has n ^ 2 bits, so the header is no longer than the matrix plus three bits and every number a machine reads from it has logarithmically many binary digits; this is the adjacency matrix representation of Reingold's algorithm, with a header that a machine reading its input by address can parse by counting.

Main definitions

• Cslib.Complexity.USTCONInstance: instances of undirected s–t connectivity.
• Cslib.Complexity.USTCONInstance.graph: the simple graph of an instance.
• Cslib.Complexity.USTCONInstance.toSTCONInstance: the directed graph of an instance.
• Cslib.Complexity.USTCONInstance.edgeTwo, Cslib.Complexity.USTCONInstance.emptyTwo, Cslib.Complexity.USTCONInstance.ofBool: canonical two-vertex connected and disconnected instances.
• Cslib.Complexity.encUSTCON: the encoding of instances.
• Cslib.Complexity.USTCON: the instances in which t is reachable from s.

Main results

• Cslib.Complexity.USTCONInstance.getD_encode_n, .getD_encode_s, .getD_encode_t, .getD_encode_matrix: the bits of the header and of the matrix in the encoding.
• Cslib.Complexity.USTCONInstance.encode_injective: the encoding is injective.
• Cslib.Complexity.USTCONInstance.size_n_le_log2: the number of vertices has logarithmically many binary digits in the length of the encoding.
• Cslib.Complexity.USTCONInstance.edgeTwo_mem_USTCON, Cslib.Complexity.USTCONInstance.emptyTwo_notMem_USTCON, Cslib.Complexity.USTCONInstance.ofBool_mem_USTCON: membership of the canonical two-vertex instances in USTCON.

References

• O. Reingold, Undirected connectivity in log-space
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

structure Cslib.Complexity.USTCONInstance : Type

An instance of undirected s–t connectivity: a simple graph on Fin n, given by its adjacency matrix, symmetric and with zero diagonal, and two vertices s and t.

• n : ℕ

  The number of vertices.

• adj : Fin self.n → Fin self.n → Bool

  The adjacency matrix.

• symm (a b : Fin self.n) : self.adj a b = self.adj b a

  The adjacency matrix is symmetric.

• loopless (a : Fin self.n) : self.adj a a = false

  No vertex is adjacent to itself.

• s : Fin self.n

  The source.

• t : Fin self.n

  The target.

theorem Cslib.Complexity.USTCONInstance.n_pos (I : USTCONInstance) : 0 < I.n

An instance has a vertex, its source.

def Cslib.Complexity.USTCONInstance.graph (I : USTCONInstance) : SimpleGraph (Fin I.n)

The simple graph of an instance: a and b are adjacent when the entry of the row a and the column b of the adjacency matrix is set.

@[instance_reducible]

instance Cslib.Complexity.USTCONInstance.instDecidableRelFinNAdjGraph (I : USTCONInstance) : DecidableRel I.graph.Adj

Adjacency in the graph of an instance is decidable.

@[simp]

theorem Cslib.Complexity.USTCONInstance.graph_adj (I : USTCONInstance) {a b : Fin I.n} : I.graph.Adj a b ↔ I.adj a b = true

Adjacency in the graph of an instance is the entry of the adjacency matrix.

def Cslib.Complexity.USTCONInstance.toSTCONInstance (I : USTCONInstance) : STCONInstance

The directed graph of an instance, with its source and target: an arc in each direction for every edge.

theorem Cslib.Complexity.USTCONInstance.toSTCONInstance_injective : Function.Injective toSTCONInstance

Distinct instances have distinct directed graphs, since the adjacency matrix determines the proofs of symmetry and looplessness.

def Cslib.Complexity.USTCONInstance.encode (I : USTCONInstance) : List Bool

The encoding of an instance, that of its directed graph (Cslib.Complexity.encSTCON): the unary header 1^n 0 1^s 0 1^t 0, then the adjacency matrix row by row.

theorem Cslib.Complexity.USTCONInstance.size_n_le_log2 (I : USTCONInstance) : I.n.size ≤ I.encode.length.log2 + 1

The number of binary digits of n is logarithmic in the length of the encoding.

theorem Cslib.Complexity.USTCONInstance.getD_encode_n (I : USTCONInstance) {i : ℕ} (h : i ≤ I.n) : I.encode.getD i false = decide (i < I.n)

The header of the number of vertices: the bit at i ≤ n is set exactly when i < n.

theorem Cslib.Complexity.USTCONInstance.getD_encode_s (I : USTCONInstance) {i : ℕ} (h : i ≤ ↑I.s) : I.encode.getD (I.n + 1 + i) false = decide (i < ↑I.s)

The header of the source: the bit at n + 1 + i, for i ≤ s, is set exactly when i < s.

theorem Cslib.Complexity.USTCONInstance.getD_encode_t (I : USTCONInstance) {i : ℕ} (h : i ≤ ↑I.t) : I.encode.getD (I.n + 1 + ↑I.s + 1 + i) false = decide (i < ↑I.t)

The header of the target: the bit at n + 1 + s + 1 + i, for i ≤ t, is set exactly when i < t.

theorem Cslib.Complexity.USTCONInstance.getD_encode_matrix (I : USTCONInstance) (a b : Fin I.n) : I.encode.getD (I.n + ↑I.s + ↑I.t + 3 + (↑a * I.n + ↑b)) false = I.adj a b

The bits of the matrix: the bit at n + s + t + 3 + a * n + b of the encoding is the entry of the row a and the column b.

theorem Cslib.Complexity.USTCONInstance.encode_injective : Function.Injective encode

The encoding is injective.

def Cslib.Complexity.encUSTCON : USTCONInstance ↪ List Bool

The encoding of instances of undirected s–t connectivity: the unary header 1^n 0 1^s 0 1^t 0, then the adjacency matrix row by row.

def Cslib.Complexity.USTCON : Set USTCONInstance

Undirected s–t connectivity: the instances in which t is reachable from s Arora and Barak, Section 21.4, Reingold.

def Cslib.Complexity.USTCONInstance.edgeTwo : USTCONInstance

The single edge on two vertices 0 and 1, with source 0 and target 1.

def Cslib.Complexity.USTCONInstance.emptyTwo : USTCONInstance

The edgeless graph on two vertices 0 and 1, with source 0 and target 1.

def Cslib.Complexity.USTCONInstance.ofBool (b : Bool) : USTCONInstance

Canonical two-vertex USTCON instance encoding a Boolean truth value: edgeTwo for true and emptyTwo for false.

theorem Cslib.Complexity.USTCONInstance.edgeTwo_mem_USTCON : edgeTwo ∈ USTCON

The single edge on two vertices belongs to USTCON.

theorem Cslib.Complexity.USTCONInstance.emptyTwo_notMem_USTCON : emptyTwo ∉ USTCON

The edgeless graph on two vertices does not belong to USTCON.

@[simp]

theorem Cslib.Complexity.USTCONInstance.ofBool_mem_USTCON {b : Bool} : ofBool b ∈ USTCON ↔ b = true

USTCONInstance.ofBool b belongs to USTCON if and only if b = true.