Diamond graphs

The diamond construction of Sipser, Theorem 7.46 reduces satisfiability to directed Hamiltonian paths. This file treats it for an arbitrary layout of the rows, so that reductions can choose how many nodes each row has. A diamond graph (Cslib.Complexity.Diamond.graph) has

• N diamonds, diamond i with a top node, a bottom node (the top of diamond i + 1), and a row of 3 * slots i + 3 nodes joined both ways in a line; the top has arcs to both ends of the row, and both ends have arcs to the bottom. Slot s < slots i of row i is the pair of row nodes 3 * s + 2 and 3 * s + 3, and the nodes 3 * s + 1 separate the pairs;
• M clause nodes;
• a list of detours (Cslib.Complexity.Diamond.Detour), each through clause d.clause across d.slot of d.row: left to right when d.leftToRight is true, right to left when it is false.

When the detours across each slot all belong to one clause (Cslib.Complexity.Diamond.WellFormed), the graph has a Hamiltonian path from the first top to the last bottom exactly when the rows can be given directions so that every clause has a detour in the direction of its row (Cslib.Complexity.Diamond.mem_DirHamPath_iff). In a Hamiltonian path every separator has its two row neighbours as predecessor and successor, a detour must return to the slot it left, so all separators of a row point the same way, and the node of a clause is entered from a slot whose row points the way of the detour. Conversely, rows traversed in the given directions, each clause visited by one detour in the direction of its row, form a Hamiltonian path.

Sipser's construction is the layout with one slot for each clause in every row; giving each row only the slots of the detours through it makes the graph linear in the size of the formula.

Node labels, detours, graphs, and the WellFormed and Satisfiable predicates are defined in CslibFrontier.Computability.Complexity.Problems.Hamiltonian.Diamond.Defs, and Hamiltonian-path soundness (satisfiable_of_mem_DirHamPath) is proved in CslibFrontier.Computability.Complexity.Problems.Hamiltonian.Diamond.Soundness; both are re-exported here alongside completeness, the equivalences mem_DirHamPath_iff and mem_DirHamCycle_iff, and polynomial-time computability.

Main definitions

• Cslib.Complexity.Diamond.encDetour: the encoding of detours used for polynomial-time computability.

Main results

• Cslib.Complexity.Diamond.mem_DirHamPath_iff: Hamiltonian paths of a diamond graph are directions of its rows satisfying every clause.
• Cslib.Complexity.Diamond.mem_DirHamCycle_iff: Hamiltonian cycles of a closed diamond graph likewise.
• Cslib.Complexity.Diamond.computableInPolyTime_graph, Cslib.Complexity.Diamond.computableInPolyTime_cycleGraph: diamond graphs are computable in polynomial time from layouts computable in polynomial time.

References

• M. Sipser, Introduction to the Theory of Computation

Directions satisfying every clause give Hamiltonian paths

Steps of a row traversal

theorem Cslib.Complexity.Diamond.mem_DirHamPath_iff {N : ℕ} {slots : ℕ → ℕ} {M : ℕ} {D : List Detour} (hD : WellFormed N slots M D) : { graph := graph N slots M D, source := topNode 0, target := topNode N } ∈ DirHamPath ↔ Satisfiable M D

Hamiltonian paths of diamond graphs. A well-formed diamond graph has a Hamiltonian path from the top of the first diamond to the bottom of the last exactly when its rows can be given directions so that every clause has a detour in the direction of its row.

theorem Cslib.Complexity.Diamond.mem_DirHamCycle_iff {N M : ℕ} {slots : ℕ → ℕ} {D : List Detour} (hD : WellFormed N slots M D) : cycleGraph N slots M D ∈ DirHamCycle ↔ Satisfiable M D

Hamiltonian cycles of closed diamond graphs. A well-formed closed diamond graph has a Hamiltonian cycle exactly when its rows can be given directions so that every clause has a detour in the direction of its row.

Polynomial time

theorem Cslib.Complexity.Diamond.encDetour_clause_inO : Turing.MultiTapeTM.ComputableInO Detour.clause encDetour Turing.MultiTapeTM.encUnary (fun (a : Detour) => (encDetour a).length) fun (a : Detour) => (encDetour a).length

theorem Cslib.Complexity.Diamond.encDetour_leftToRight_deg : Turing.MultiTapeTM.ComputableInDegree Detour.leftToRight encDetour Turing.MultiTapeTM.encBool 1 1

theorem Cslib.Complexity.Diamond.encDetour_row_deg : Turing.MultiTapeTM.ComputableInDegree Detour.row encDetour Turing.MultiTapeTM.encUnary 1 1

def Cslib.Complexity.Diamond.encDetour : Detour ↪ List Bool

Detours encoded with unary clause, row and slot indices.

theorem Cslib.Complexity.Diamond.encDetour_row_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Detour} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encDetour S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).row) encIn✝ Turing.MultiTapeTM.encUnary S✝

theorem Cslib.Complexity.Diamond.encDetour_slot_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Detour} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encDetour → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).slot) encIn✝ Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.Diamond.encDetour_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 x1 x2 : γ → ℕ} {x3 : γ → Bool} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encUnary) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encUnary) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn Turing.MultiTapeTM.encUnary) (h3 : Turing.MultiTapeTM.ComputableInPolyTime x3 encIn Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { clause := x0 x, row := x1 x, slot := x2 x, leftToRight := x3 x }) encIn encDetour

theorem Cslib.Complexity.Diamond.encDetour_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : Detour) => (a.clause, a.row, a.slot, a.leftToRight)) encDetour encDetourFields 1 1

theorem Cslib.Complexity.Diamond.encDetour_row_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Detour} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encDetour → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).row) encIn✝ Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.Diamond.encDetour_slot_inO : Turing.MultiTapeTM.ComputableInO Detour.slot encDetour Turing.MultiTapeTM.encUnary (fun (a : Detour) => (encDetour a).length) fun (a : Detour) => (encDetour a).length

theorem Cslib.Complexity.Diamond.encDetour_slot_deg : Turing.MultiTapeTM.ComputableInDegree Detour.slot encDetour Turing.MultiTapeTM.encUnary 1 1

theorem Cslib.Complexity.Diamond.encDetour_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : ℕ × ℕ × ℕ × Bool) => { clause := p.1, row := p.2.1, slot := p.2.2.1, leftToRight := p.2.2.2 }) encDetourFields encDetour 1 1

theorem Cslib.Complexity.Diamond.encDetour_leftToRight_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Detour} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encDetour → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).leftToRight) encIn✝ Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.Diamond.encDetour_clause_deg : Turing.MultiTapeTM.ComputableInDegree Detour.clause encDetour Turing.MultiTapeTM.encUnary 1 1

theorem Cslib.Complexity.Diamond.encDetour_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 x1 T1 S1 x2 T2 S2 : γ → ℕ} {x3 : γ → Bool} {T3 S3 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encUnary T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encUnary T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn Turing.MultiTapeTM.encUnary T2 S2) (h3 : Turing.MultiTapeTM.ComputableInO x3 encIn Turing.MultiTapeTM.encBool T3 S3) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { clause := x0 x, row := x1 x, slot := x2 x, leftToRight := x3 x }) encIn encDetour (fun (x : γ) => T0 x + (T1 x + (T2 x + T3 x))) fun (x : γ) => S0 x + (S1 x + (S2 x + S3 x))

@[reducible, inline]

abbrev Cslib.Complexity.Diamond.encDetourFields : ℕ × ℕ × ℕ × Bool ↪ List Bool

The tuple of the fields of encDetour.

theorem Cslib.Complexity.Diamond.encDetour_clause_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Detour} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encDetour → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).clause) encIn✝ Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.Diamond.encDetour_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 x1 x2 : γ → ℕ} {x3 : γ → Bool} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encUnary budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encUnary budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn Turing.MultiTapeTM.encUnary budget) (h3 : Turing.MultiTapeTM.ComputableInSpace x3 encIn Turing.MultiTapeTM.encBool budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { clause := x0 x, row := x1 x, slot := x2 x, leftToRight := x3 x }) encIn encDetour budget

theorem Cslib.Complexity.Diamond.encDetour_leftToRight_inO : Turing.MultiTapeTM.ComputableInO Detour.leftToRight encDetour Turing.MultiTapeTM.encBool (fun (a : Detour) => (encDetour a).length) fun (a : Detour) => (encDetour a).length

theorem Cslib.Complexity.Diamond.encDetour_row_inO : Turing.MultiTapeTM.ComputableInO Detour.row encDetour Turing.MultiTapeTM.encUnary (fun (a : Detour) => (encDetour a).length) fun (a : Detour) => (encDetour a).length

@[simp]

theorem Cslib.Complexity.Diamond.encDetour_apply (a : Detour) : encDetour a = encDetourFields (a.clause, a.row, a.slot, a.leftToRight)

theorem Cslib.Complexity.Diamond.encDetour_leftToRight_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Detour} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encDetour S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).leftToRight) encIn✝ Turing.MultiTapeTM.encBool S✝

theorem Cslib.Complexity.Diamond.encDetour_clause_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Detour} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encDetour S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).clause) encIn✝ Turing.MultiTapeTM.encUnary S✝

theorem Cslib.Complexity.Diamond.encDetour_slot_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Detour} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encDetour S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).slot) encIn✝ Turing.MultiTapeTM.encUnary S✝

theorem Cslib.Complexity.Diamond.computableInPolyTime_topNode : Turing.MultiTapeTM.ComputableInPolyTime (fun (i : ℕ) => topNode i) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat

The top nodes are computable in polynomial time from unary indices.

theorem Cslib.Complexity.Diamond.computableInPolyTime_rowNode : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => rowNode p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encNat

The row nodes are computable in polynomial time from unary indices.

theorem Cslib.Complexity.Diamond.computableInPolyTime_clauseNode : Turing.MultiTapeTM.ComputableInPolyTime (fun (j : ℕ) => clauseNode j) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat

The clause nodes are computable in polynomial time from unary indices.

theorem Cslib.Complexity.Diamond.computableInPolyTime_graph {α : Type} {encIn : α ↪ List Bool} {N M : α → ℕ} {slots : α → ℕ → ℕ} {D : α → List Detour} (hN : Turing.MultiTapeTM.ComputableInPolyTime N encIn Turing.MultiTapeTM.encUnary) (hslots : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : α × ℕ) => slots p.1 p.2) (Turing.MultiTapeTM.encPair encIn Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary) (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hD : Turing.MultiTapeTM.ComputableInPolyTime D encIn (Turing.MultiTapeTM.encList encDetour)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => graph (N a) (slots a) (M a) (D a)) encIn encGraph

A diamond graph is computable in polynomial time from a layout computable in polynomial time, with the numbers of diamonds, slots and clauses in unary.

theorem Cslib.Complexity.Diamond.computableInPolyTime_cycleGraph {α : Type} {encIn : α ↪ List Bool} {N M : α → ℕ} {slots : α → ℕ → ℕ} {D : α → List Detour} (hN : Turing.MultiTapeTM.ComputableInPolyTime N encIn Turing.MultiTapeTM.encUnary) (hslots : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : α × ℕ) => slots p.1 p.2) (Turing.MultiTapeTM.encPair encIn Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary) (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hD : Turing.MultiTapeTM.ComputableInPolyTime D encIn (Turing.MultiTapeTM.encList encDetour)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => cycleGraph (N a) (slots a) (M a) (D a)) encIn encGraph

A closed diamond graph is computable in polynomial time from a layout computable in polynomial time, with the numbers of diamonds, slots and clauses in unary.