Directed s–t connectivity

An instance of directed s–t connectivity (Cslib.Complexity.STCONInstance) is a directed graph on Fin n, given by its adjacency matrix, together with two vertices s and t; it belongs to Cslib.Complexity.STCON when the graph has a directed path from s to t, of any length, including the empty path when s = t. This is the problem PATH of Sipser, Section 7.2 and Example 8.19, also called REACHABILITY Papadimitriou, Section 1.1. The adjacency matrix need not be symmetric and may have loops.

Instances are encoded (Cslib.Complexity.encSTCON) by the unary header 1^n 0 1^s 0 1^t 0 followed by the adjacency matrix, row by row: 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 every number a machine reads from the header has logarithmically many binary digits in the length of the encoding. This is the encoding of undirected connectivity (Cslib.Complexity.encUSTCON), which is defined through it.

Main definitions

• Cslib.Complexity.STCONInstance: instances of directed s–t connectivity.
• Cslib.Complexity.STCONInstance.Adj: the arcs of an instance.
• Cslib.Complexity.encSTCON: the encoding of instances.
• Cslib.Complexity.STCON: the instances with a directed path from s to t.

Main results

• Cslib.Complexity.STCONInstance.getD_encode_n, .getD_encode_s, .getD_encode_t, .getD_encode_matrix: the bits of the header and of the matrix in the encoding; .getElem?_encode_n, .getElem?_encode_s, .getElem?_encode_t, .getElem?_encode_matrix: the same bits, read by position.
• Cslib.Complexity.STCONInstance.length_encode: the length of the encoding.
• Cslib.Complexity.STCONInstance.matrix_eq_flatMap: the matrix as the concatenation of its rows.
• Cslib.Complexity.STCONInstance.encode_injective: the encoding is injective.
• Cslib.Complexity.STCONInstance.size_n_le_log2: the number of vertices has logarithmically many binary digits in the length of the encoding.

References

• M. Sipser, Introduction to the Theory of Computation
• C. H. Papadimitriou, Computational Complexity

structure Cslib.Complexity.STCONInstance : Type

An instance of directed s–t connectivity: a directed graph on Fin n, given by its adjacency matrix, and two vertices s and t.

• n : ℕ

  The number of vertices.

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

  The adjacency matrix: adj a b when there is an arc from a to b.

• s : Fin self.n

  The source.

• t : Fin self.n

  The target.

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

An instance has a vertex, its source.

def Cslib.Complexity.STCONInstance.Adj (I : STCONInstance) (a b : Fin I.n) : Prop

The arcs of an instance: there is an arc from a to b when the entry of the row a and the column b of the adjacency matrix is set.

theorem Cslib.Complexity.STCONInstance.mod_lt_of_lt_mul {i n : ℕ} (h : i < n * n) : i % n < n

The column of an index below n * n is below n.

def Cslib.Complexity.STCONInstance.matrix (I : STCONInstance) : List Bool

The adjacency matrix, row by row: its bit at i is the entry of the row i / n and the column i % n.

@[simp]

theorem Cslib.Complexity.STCONInstance.length_matrix (I : STCONInstance) : I.matrix.length = I.n * I.n

The adjacency matrix has n ^ 2 entries.

theorem Cslib.Complexity.STCONInstance.mul_add_lt (I : STCONInstance) (a b : Fin I.n) : ↑a * I.n + ↑b < I.n * I.n

The position a * n + b of an entry lies within the matrix.

theorem Cslib.Complexity.STCONInstance.getD_matrix (I : STCONInstance) (a b : Fin I.n) : I.matrix.getD (↑a * I.n + ↑b) false = I.adj a b

The entry of the row a and the column b is the bit at a * n + b of the matrix.

theorem Cslib.Complexity.STCONInstance.matrix_eq_flatMap (I : STCONInstance) (g : ℕ → ℕ → Bool) (hg : ∀ (a b : Fin I.n), I.adj a b = g ↑a ↑b) : I.matrix = List.flatMap (fun (u : ℕ) => List.map (g u) (List.range I.n)) (List.range I.n)

The matrix row by row: the rows 0, …, n - 1, each listing its entries in the columns 0, …, n - 1, for any function g on natural numbers giving the entries.

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

The encoding of an instance: the unary header 1^n 0 1^s 0 1^t 0, then the adjacency matrix row by row.

theorem Cslib.Complexity.STCONInstance.length_encode (I : STCONInstance) : I.encode.length = I.n + ↑I.s + ↑I.t + 3 + I.n * I.n

The length of the encoding: the header and the n ^ 2 entries of the matrix.

theorem Cslib.Complexity.STCONInstance.n_le_length_encode (I : STCONInstance) : I.n ≤ I.encode.length

The number of vertices is at most the length of the encoding.

theorem Cslib.Complexity.STCONInstance.size_n_le_log2 (I : STCONInstance) : 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.STCONInstance.getD_encode_n (I : STCONInstance) {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.STCONInstance.getD_encode_s (I : STCONInstance) {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.STCONInstance.getD_encode_t (I : STCONInstance) {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.STCONInstance.getD_encode_matrix (I : STCONInstance) (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.STCONInstance.getElem?_encode_n (I : STCONInstance) {i : ℕ} (h : i ≤ I.n) : I.encode[i]? = some (decide (i < I.n))

The header of the number of vertices, read by position.

theorem Cslib.Complexity.STCONInstance.getElem?_encode_s (I : STCONInstance) {i : ℕ} (h : i ≤ ↑I.s) : I.encode[I.n + 1 + i]? = some (decide (i < ↑I.s))

The header of the source, read by position.

theorem Cslib.Complexity.STCONInstance.getElem?_encode_t (I : STCONInstance) {i : ℕ} (h : i ≤ ↑I.t) : I.encode[I.n + 1 + ↑I.s + 1 + i]? = some (decide (i < ↑I.t))

The header of the target, read by position.

theorem Cslib.Complexity.STCONInstance.getElem?_encode_matrix (I : STCONInstance) {a b : ℕ} (ha : a < I.n) (hb : b < I.n) : I.encode[I.n + ↑I.s + ↑I.t + 3 + (a * I.n + b)]? = some (I.adj ⟨a, ha⟩ ⟨b, hb⟩)

The entries of the matrix, read by position.

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

The encoding is injective.

def Cslib.Complexity.encSTCON : STCONInstance ↪ List Bool

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

@[simp]

theorem Cslib.Complexity.encSTCON_apply (I : STCONInstance) : encSTCON I = I.encode

def Cslib.Complexity.STCON : Set STCONInstance

Directed s–t connectivity: the instances whose graph has a directed path from s to t, the problem PATH of Sipser, Example 8.19.

theorem Cslib.Complexity.mem_STCON {I : STCONInstance} : I ∈ STCON ↔ Relation.ReflTransGen I.Adj I.s I.t