Soundness of diamond graphs: Hamiltonian paths give satisfying directions

In a well-formed diamond graph (Cslib.Complexity.Diamond.WellFormed), any directed Hamiltonian path from topNode 0 to topNode N traverses every separator of row i in a consistent direction and enters every clause node via a detour in the direction of its row, establishing Cslib.Complexity.Diamond.Satisfiable.

Main results

• Cslib.Complexity.Diamond.satisfiable_of_mem_DirHamPath: a Hamiltonian path of the diamond graph gives directions of the rows satisfying every clause.

References

• M. Sipser, Introduction to the Theory of Computation

Successors in a list

Hamiltonian paths give directions satisfying every clause

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

A Hamiltonian path of the diamond graph gives directions of the rows satisfying every clause.