Diamond graph definitions, membership, and size bounds

This file defines the diamond graph (Cslib.Complexity.Diamond.graph) and closed diamond graph (Cslib.Complexity.Diamond.cycleGraph) used in the reduction of satisfiability to directed Hamiltonian paths and cycles Sipser, Theorem 7.46, along with vertex and arc membership characterizations and size formulas.

Main definitions

• Cslib.Complexity.Diamond.Detour: a detour through a clause node across a slot of a row.
• Cslib.Complexity.Diamond.topNode, Cslib.Complexity.Diamond.rowNode, Cslib.Complexity.Diamond.clauseNode: vertex labels of a diamond graph.
• Cslib.Complexity.Diamond.graph, Cslib.Complexity.Diamond.cycleGraph: diamond graphs and closed diamond graphs.
• Cslib.Complexity.Diamond.WellFormed, Cslib.Complexity.Diamond.Satisfiable.

Main results

• Cslib.Complexity.Diamond.mem_vertices, Cslib.Complexity.Diamond.mem_arcs: membership in the vertex and arc lists.
• Cslib.Complexity.Diamond.length_vertices, Cslib.Complexity.Diamond.length_arcs: the size of a diamond graph.
• Cslib.Complexity.Diamond.notMem_arcs_topNode_zero: no arc enters the top of the first diamond.

References

• M. Sipser, Introduction to the Theory of Computation

Diamond graphs

structure Cslib.Complexity.Diamond.Detour : Type

A detour through the node of clause clause, across slot of row, left to right when leftToRight is true and right to left otherwise.

• clause : ℕ

  The clause index visited by the detour.

• row : ℕ

  The row index containing the slot.

• slot : ℕ

  The slot index within the row.

• leftToRight : Bool

  Whether the detour traverses the slot from left to right.

theorem Cslib.Complexity.Diamond.Detour.ext_iff {x y : Detour} : x = y ↔ x.clause = y.clause ∧ x.row = y.row ∧ x.slot = y.slot ∧ x.leftToRight = y.leftToRight

theorem Cslib.Complexity.Diamond.Detour.ext {x y : Detour} (clause : x.clause = y.clause) (row : x.row = y.row) (slot : x.slot = y.slot) (leftToRight : x.leftToRight = y.leftToRight) : x = y

def Cslib.Complexity.Diamond.instDecidableEqDetour.decEq (x✝ x✝¹ : Detour) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.Diamond.instDecidableEqDetour : DecidableEq Detour

@[instance_reducible]

instance Cslib.Complexity.Diamond.instInhabitedDetour : Inhabited Detour

def Cslib.Complexity.Diamond.topNode (i : ℕ) : ℕ

The top of diamond i, which is also the bottom of diamond i - 1.

def Cslib.Complexity.Diamond.rowNode (i a : ℕ) : ℕ

Node a of the row of diamond i.

def Cslib.Complexity.Diamond.clauseNode (j : ℕ) : ℕ

The node of clause j.

def Cslib.Complexity.Diamond.rowLength (slots : ℕ → ℕ) (i : ℕ) : ℕ

The number of nodes in row i: a pair of nodes for each slot, separators between and around the pairs, and the two ends.

def Cslib.Complexity.Diamond.diamondArcs (slots : ℕ → ℕ) (i : ℕ) : List (ℕ × ℕ)

The arcs of diamond i: from its top to both ends of its row, from both ends to its bottom, and both ways between consecutive row nodes.

def Cslib.Complexity.Diamond.detourArcs (d : Detour) : List (ℕ × ℕ)

The arcs of the detour d.

def Cslib.Complexity.Diamond.arcs (N : ℕ) (slots : ℕ → ℕ) (D : List Detour) : List (ℕ × ℕ)

The arcs of the diamond graph: the diamonds and the detours.

def Cslib.Complexity.Diamond.vertices (N : ℕ) (slots : ℕ → ℕ) (M : ℕ) : List ℕ

The vertices of the diamond graph: the tops, the rows and the clause nodes.

def Cslib.Complexity.Diamond.graph (N : ℕ) (slots : ℕ → ℕ) (M : ℕ) (D : List Detour) : Graph

The diamond graph with N diamonds whose rows have slots i slots, M clause nodes and the detours D.

def Cslib.Complexity.Diamond.cycleGraph (N : ℕ) (slots : ℕ → ℕ) (M : ℕ) (D : List Detour) : Graph

The diamond graph closed by an arc from the bottom of the last diamond to the top of the first.

structure Cslib.Complexity.Diamond.WellFormed (N : ℕ) (slots : ℕ → ℕ) (M : ℕ) (D : List Detour) : Prop

The detours go through declared nodes, and the detours across each slot all belong to one clause.

• clause_lt (d : Detour) : d ∈ D → d.clause < M
• row_lt (d : Detour) : d ∈ D → d.row < N
• slot_lt (d : Detour) : d ∈ D → d.slot < slots d.row
• clause_eq (d : Detour) : d ∈ D → ∀ d' ∈ D, d.row = d'.row → d.slot = d'.slot → d.clause = d'.clause

def Cslib.Complexity.Diamond.Satisfiable (M : ℕ) (D : List Detour) : Prop

Some directions of the rows give every clause j < M a detour in the direction of its row.

Vertices and arcs

@[simp]

theorem Cslib.Complexity.Diamond.topNode_inj {i i' : ℕ} : topNode i = topNode i' ↔ i = i'

@[simp]

theorem Cslib.Complexity.Diamond.rowNode_inj {i i' a a' : ℕ} : rowNode i a = rowNode i' a' ↔ i = i' ∧ a = a'

@[simp]

theorem Cslib.Complexity.Diamond.clauseNode_inj {j j' : ℕ} : clauseNode j = clauseNode j' ↔ j = j'

@[simp]

theorem Cslib.Complexity.Diamond.topNode_ne_rowNode (i i' a : ℕ) : topNode i ≠ rowNode i' a

@[simp]

theorem Cslib.Complexity.Diamond.rowNode_ne_topNode (i i' a : ℕ) : rowNode i' a ≠ topNode i

@[simp]

theorem Cslib.Complexity.Diamond.topNode_ne_clauseNode (i j : ℕ) : topNode i ≠ clauseNode j

@[simp]

theorem Cslib.Complexity.Diamond.clauseNode_ne_topNode (i j : ℕ) : clauseNode j ≠ topNode i

@[simp]

theorem Cslib.Complexity.Diamond.rowNode_ne_clauseNode (i a j : ℕ) : rowNode i a ≠ clauseNode j

@[simp]

theorem Cslib.Complexity.Diamond.clauseNode_ne_rowNode (i a j : ℕ) : clauseNode j ≠ rowNode i a

theorem Cslib.Complexity.Diamond.rowLength_sub_one (slots : ℕ → ℕ) (i : ℕ) : rowLength slots i - 1 = 3 * slots i + 2

theorem Cslib.Complexity.Diamond.mem_vertices {N : ℕ} {slots : ℕ → ℕ} {M v : ℕ} : v ∈ vertices N slots M ↔ (∃ i ≤ N, v = topNode i) ∨ (∃ i < N, ∃ a < rowLength slots i, v = rowNode i a) ∨ ∃ j < M, v = clauseNode j

theorem Cslib.Complexity.Diamond.mem_arcs {N : ℕ} {slots : ℕ → ℕ} {D : List Detour} {u v : ℕ} : (u, v) ∈ arcs N slots D ↔ (∃ i < N, u = topNode i ∧ (v = rowNode i 0 ∨ v = rowNode i (rowLength slots i - 1)) ∨ (u = rowNode i 0 ∨ u = rowNode i (rowLength slots i - 1)) ∧ v = topNode (i + 1) ∨ ∃ a < rowLength slots i - 1, u = rowNode i a ∧ v = rowNode i (a + 1) ∨ u = rowNode i (a + 1) ∧ v = rowNode i a) ∨ ∃ d ∈ D, d.leftToRight = true ∧ (u = rowNode d.row (3 * d.slot + 2) ∧ v = clauseNode d.clause ∨ u = clauseNode d.clause ∧ v = rowNode d.row (3 * d.slot + 3)) ∨ d.leftToRight = false ∧ (u = rowNode d.row (3 * d.slot + 3) ∧ v = clauseNode d.clause ∨ u = clauseNode d.clause ∧ v = rowNode d.row (3 * d.slot + 2))

theorem Cslib.Complexity.Diamond.length_vertices (N : ℕ) (slots : ℕ → ℕ) (M : ℕ) : (vertices N slots M).length = 4 * N + 3 * (List.map slots (List.range N)).sum + M + 1

The number of vertices of a diamond graph, counted as listed.

theorem Cslib.Complexity.Diamond.length_arcs (N : ℕ) (slots : ℕ → ℕ) (D : List Detour) : (arcs N slots D).length = 8 * N + 6 * (List.map slots (List.range N)).sum + 2 * D.length

The number of arcs of a diamond graph, counted as listed.

theorem Cslib.Complexity.Diamond.notMem_arcs_topNode_zero {N : ℕ} {slots : ℕ → ℕ} {D : List Detour} (u : ℕ) : (u, topNode 0) ∉ arcs N slots D

No arc enters the top of the first diamond.