diff --git a/Examples.lean b/Examples.lean
index b2763d8..8b94678 100644
--- a/Examples.lean
+++ b/Examples.lean
@@ -4,6 +4,7 @@ import LeanHoG.Widgets
 import LeanHoG.Tactic.SearchDSL
 import LeanHoG.Tactic.Basic
 import LeanHoG.Invariant.HamiltonianPath.Tactic
+import LeanHoG.Invariant.HamiltonianCycle.Tactic
 
 namespace LeanHoG
 
@@ -95,6 +96,17 @@ load_graph hog_896 "build/graphs/896.json"
 #check_traceable hog_896
 #show_hamiltonian_path hog_896
 
+-------------------------------------------
+-- Hamiltonian cycles
+-------------------------------------------
+-- NOTE: Non-Hamiltonicity not yet implemented
+
+#check_hamiltonian Cycle7
+
+theorem foo : Cycle7.isHamiltonian := by
+  check_hamiltonian Cycle7
+  decide
+
 ---------------------------------------
 -- Tactics
 ---------------------------------------
@@ -113,7 +125,7 @@ load_graph hog_896 "build/graphs/896.json"
 
 -- set_option leanHoG.solverCmd "cadical"
 -- set_option leanHoG.proofCheckerCmd "cake_lpr"
-example : ∃ (G : Graph), G.traceable ∧ G.vertexSize > 3 ∧ (G.minimumDegree < G.vertexSize / 2) := by
+example : ∃ (G : Graph), G.isHamiltonian ∧ G.vertexSize > 3 ∧ (G.minimumDegree < G.vertexSize / 2) := by
   find_example
 
 end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianCycle/Basic.lean b/LeanHoG/Invariant/HamiltonianCycle/Basic.lean
new file mode 100644
index 0000000..25a81aa
--- /dev/null
+++ b/LeanHoG/Invariant/HamiltonianCycle/Basic.lean
@@ -0,0 +1,45 @@
+
+import LeanHoG.Graph
+import LeanHoG.Walk
+
+namespace LeanHoG
+
+@[simp] def Cycle.isHamiltonian {g : Graph} {u : g.vertex} (c : Cycle g u) : Bool :=
+  ∀ (v : g.vertex), List.contains c.cycle.vertices v
+
+class HamiltonianCycle (g : Graph)  where
+  u : g.vertex
+  cycle : Cycle g u
+  isHamiltonian : cycle.isHamiltonian = true
+
+def Graph.isHamiltonian (g : Graph) : Prop :=
+  ∃ (u : g.vertex) (c : Cycle g u), c.isHamiltonian
+
+@[simp] def Graph.isNonHamiltonian (g : Graph) : Prop := ¬ g.isHamiltonian
+
+@[simp] def Graph.isNonHamiltonian' {g : Graph} : Prop :=
+  ∀ (u : g.vertex) (c : Cycle g u), ¬c.isHamiltonian
+
+namespace HamiltonianCycle
+
+instance {g : Graph} : Repr (HamiltonianCycle g) where
+  reprPrec p n := reprPrec p.cycle n
+
+instance {g : Graph} : Repr (HamiltonianCycle g) where
+  reprPrec p n := reprPrec p.2.cycle n
+
+@[simp] theorem cycle_of_cert {g : Graph} [hp : HamiltonianCycle g] : g.isHamiltonian := by
+  let ⟨u, p, cond⟩ := hp
+  apply Exists.intro u
+  apply Exists.intro p
+  apply cond
+
+instance {G : Graph} [HamiltonianCycle G] : Decidable (G.isHamiltonian) :=
+  .isTrue cycle_of_cert
+
+theorem equivNonHamiltonianDefs (g : Graph) :
+  g.isNonHamiltonian ↔ g.isNonHamiltonian' :=
+  by simp [Graph.isHamiltonian]
+
+end HamiltonianCycle
+end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianCycle/Certificate.lean b/LeanHoG/Invariant/HamiltonianCycle/Certificate.lean
new file mode 100644
index 0000000..9c80b7b
--- /dev/null
+++ b/LeanHoG/Invariant/HamiltonianCycle/Certificate.lean
@@ -0,0 +1,47 @@
+import Qq
+import LeanHoG.Edge
+import LeanHoG.Graph
+import LeanHoG.Util.RB
+import LeanHoG.Util.Quote
+import LeanHoG.Invariant.HamiltonianCycle.Basic
+import LeanHoG.Invariant.HamiltonianCycle.JsonData
+
+namespace LeanHoG
+
+open Qq
+def hamiltonianCycleOfData (G : Q(Graph)) (D : HamiltonianCycleData) : Q(HamiltonianCycle $G) :=
+  -- Helper function to compute a Walk from a list of vertices
+  let rec fold (t : Q(Graph.vertex $G)) : List Q(Graph.vertex $G) →
+    ((s : Q(Graph.vertex $G)) ×' Q(Walk $G $s $t)) := fun vs =>
+    match vs with
+    | [] => panic! "given empty path, cannot construct Hamiltonian cycle"
+    | [v] =>
+      let h : Q($v = $t) := (q(Eq.refl $v) : Lean.Expr)
+      ⟨v, q($h ▸ .here $v)⟩
+    | u :: v :: vs =>
+      let ⟨s, w⟩ := fold t (v :: vs)
+      let h : Q(decide (@Graph.adjacent $G $u $s) = true) := (q(Eq.refl true) : Lean.Expr)
+      let w' := q(.step (of_decide_eq_true $h) $w)
+      ⟨u, w'⟩
+
+  have n : Q(Nat) := q(Graph.vertexSize $G)
+  let vertices : List Q(Graph.vertex $G) := D.cycle.map (finOfData n)
+  -- Construct the Hamiltonian cycle from the path
+  match vertices.getLast? with
+  | none => panic! "no vertices"
+  | some t =>
+    let ⟨s, w⟩ : ((s : Q(Graph.vertex $G)) ×' Q(Walk $G $s $t)) := fold t vertices
+    -- Check that w starts and end in the same vertex
+    -- Note: Have to use definitional equality instead of propositional
+    -- otherwise the types aren't correct.
+    have _isClosed : $s =Q $t := ⟨⟩
+    -- Declare w to actually be a closed walk, we know this from above
+    have cw : Q(ClosedWalk $G $s) := w
+    have _eq : $cw =Q $w := ⟨⟩
+    -- Check that it is a cycle, i.e. no repeating vertices
+    have isCycle : Q(decide (ClosedWalk.isCycle $cw) = true) := (q(Eq.refl true) : Lean.Expr)
+    let c : Q(Cycle $G $s) := q(@Cycle.mk $G $s $cw (of_decide_eq_true ($isCycle)))
+    have isHamiltonian : Q(decide (Cycle.isHamiltonian $c) = true) := (q(Eq.refl true) : Lean.Expr)
+    have hc : Q(HamiltonianCycle $G) :=
+      q(@HamiltonianCycle.mk $G $s (Cycle.mk $cw (of_decide_eq_true ($isCycle))) (of_decide_eq_true $isHamiltonian))
+    hc
diff --git a/LeanHoG/Invariant/HamiltonianCycle/JsonData.lean b/LeanHoG/Invariant/HamiltonianCycle/JsonData.lean
new file mode 100644
index 0000000..5300bf3
--- /dev/null
+++ b/LeanHoG/Invariant/HamiltonianCycle/JsonData.lean
@@ -0,0 +1,16 @@
+import Lean
+import LeanHoG.Graph
+
+namespace LeanHoG
+
+/--
+  JSON encoding of a Hamiltonian path.
+-/
+structure HamiltonianCycleData : Type where
+  /-- Hamiltonian cycle -/
+  cycle : List Nat
+
+deriving Lean.FromJson
+
+
+end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianCycle/SatEncoding.lean b/LeanHoG/Invariant/HamiltonianCycle/SatEncoding.lean
new file mode 100644
index 0000000..cb92dd3
--- /dev/null
+++ b/LeanHoG/Invariant/HamiltonianCycle/SatEncoding.lean
@@ -0,0 +1,196 @@
+import LeanHoG.Graph
+import LeanHoG.Walk
+import LeanHoG.Invariant.ConnectedComponents.Basic
+import LeanHoG.Invariant.HamiltonianCycle.Basic
+import Lean
+
+import LeanSAT
+
+namespace LeanHoG
+namespace HamiltonianCycle
+
+open Lean LeanSAT Encode VEncCNF Meta Model PropFun
+
+/-- `Var i j = true` means: "at position j on the cycle is vertex i".
+-/
+structure Var (n : Nat) where
+  vertex : Fin n
+  pos : Fin (n + 1)
+deriving DecidableEq, LeanColls.IndexType
+
+@[simp] def vertexAtPos {n : Nat} (i : Fin n) (j : Fin (n+1)) : PropFun (Var n) :=
+  Var.mk i j
+
+@[simp] def positionHasAVertex {n : Nat} (j : Fin (n+1)) : PropPred (Var n) := fun τ =>
+  ∃ (i : Fin n), τ ⊨ vertexAtPos i j
+
+@[simp] def eachPositionHasAVertex {n : Nat} : PropPred (Var n) := fun τ =>
+  ∀ (j : Fin (n+1)), positionHasAVertex j τ
+
+@[simp] def vertexIsAtSomePosition {n : Nat} (i : Fin n) : PropPred (Var n) := fun τ =>
+  ∃ (j : Fin (n+1)), τ ⊨ vertexAtPos i j
+
+@[simp] def eachVertexIsAtSomePosition {n : Nat} : PropPred (Var n) := fun τ =>
+  ∀ (i : Fin n), vertexIsAtSomePosition i τ
+
+/-- The first and last position of the cycle should actually have the same vertex. -/
+@[simp] def vertexInAtMostOnePositionExceptEndpoints {n : Nat} (i : Fin n) : PropPred (Var n) := fun τ =>
+  ∀ (j k : Fin (n+1)), j ≠ k ∧ j.val < n ∧ k.val < n → τ ⊨ (vertexAtPos i j)ᶜ ⊔ (vertexAtPos i k)ᶜ
+
+/-- The first and last position of the cycle should actually have the same vertex. -/
+@[simp] def eachVertexInAtMostOnePositionExceptEndpoints {n : Nat} : PropPred (Var n) := fun τ =>
+  ∀ (i : Fin n), vertexInAtMostOnePositionExceptEndpoints i τ
+
+@[simp] def atMostOneVertexAtPosition {n : Nat} (j : Fin (n+1)) : PropPred (Var n) := fun τ =>
+  ∀ (i k : Fin n), i ≠ k → τ ⊨ (vertexAtPos i j)ᶜ ⊔ (vertexAtPos k j)ᶜ
+
+@[simp] def atMostOneVertexInEachPosition {n : Nat} : PropPred (Var n) := fun τ =>
+  ∀ (j : Fin (n+1)), atMostOneVertexAtPosition j τ
+
+/-- Encode that if two vertices are consecutive on the cycle, they are adjacent. -/
+@[simp] def nonAdjacentVerticesNotConsecutive {G : Graph} : PropPred (Var G.vertexSize) := fun τ =>
+  ∀ (k k': Fin (G.vertexSize+1)), k.val + 1 = k'.val →
+    ∀ (i j : Fin G.vertexSize), ¬G.adjacent i j →
+      (τ ⊨ ((vertexAtPos i k)ᶜ ⊔ (vertexAtPos j k')ᶜ))
+
+-- These constraints are just because of efficiency
+-- We declare that the starting and ending vertex must be vertex 0,
+-- since we know that the cycle must go through it anyway, we can do it
+-- without loss of generality.
+
+@[simp] def cycleStartsAtVertex0 (G : Graph) (h : 0 < G.vertexSize) : PropPred (Var G.vertexSize) := fun τ =>
+  τ ⊨ (vertexAtPos ⟨0, h⟩ 0)
+
+@[simp] def cycleEndsAtVertex0 (G : Graph) (h : 0 < G.vertexSize) : PropPred (Var G.vertexSize) := fun τ =>
+  τ ⊨ (vertexAtPos ⟨0, h⟩ G.vertexSize)
+
+@[simp] def vertexConstraints (G : Graph) : PropPred (Var G.vertexSize) := fun τ =>
+  (τ |> eachVertexIsAtSomePosition) ∧
+  (τ |> eachVertexInAtMostOnePositionExceptEndpoints)
+
+@[simp] def positionConstraints (G : Graph) : PropPred (Var G.vertexSize) := fun τ =>
+  (τ |> eachPositionHasAVertex) ∧
+  (τ |> atMostOneVertexInEachPosition)
+
+@[simp] def edgeConstraints (G : Graph) : PropPred (Var G.vertexSize) := fun τ =>
+  (τ |> nonAdjacentVerticesNotConsecutive)
+
+@[simp] def firstAndLastConstraints (G : Graph) (h : 0 < G.vertexSize) : PropPred (Var G.vertexSize) := fun τ =>
+  (τ |> cycleStartsAtVertex0 G h) ∧ (τ |> cycleEndsAtVertex0 G h)
+
+@[simp] def hamiltonianCycleConstraints (G : Graph) (h : 0 < G.vertexSize) : PropPred (Var G.vertexSize) := fun τ =>
+  (τ |> vertexConstraints G) ∧ (τ |> positionConstraints G) ∧ (τ |> edgeConstraints G) ∧ (τ |> firstAndLastConstraints G h)
+
+----------------------------------------------------------------------------------------
+-- Express the problem as a CNF
+
+open Encode VEncCNF LitVar
+
+abbrev VCnf (n : Nat) := VEncCNF (Var n) Unit
+
+@[simp] def verticesAtPosition {n : Nat} (j : Fin (n+1)) : List (Literal <| Var n) :=
+  List.finRange n |>.map (mkPos <| Var.mk · j)
+
+@[simp] def vertexAtPositions {n : Nat} (i : Fin n) : List (Literal <| Var n) :=
+  List.finRange (n+1) |>.map (mkPos <| Var.mk i ·)
+
+def vertexClauses (G : Graph) : VCnf G.vertexSize (vertexConstraints G) :=
+  ( let U := Array.finRange G.vertexSize
+    let V := Array.finRange (G.vertexSize+1)
+    seq[
+      for_all U fun i =>
+        addClause (List.toArray (vertexAtPositions i)),
+      for_all U fun i =>
+      for_all V fun j =>
+      for_all V fun k =>
+        VEncCNF.guard (j ≠ k ∧ j.val < (G.vertexSize) ∧ k.val < (G.vertexSize)) fun _ =>
+          addClause (#[mkNeg <| Var.mk i j, mkNeg <| Var.mk i k])
+  ])
+  |> mapProp (by
+    ext τ
+    simp [Clause.toPropFun]
+    intro _
+    apply Iff.intro
+    intro h' i j k j_neq_k j_lt k_lt
+    have h'' := h' i j k
+    simp [j_neq_k, j_lt, k_lt] at h''
+    exact h''
+    intro h' i j k
+    have := h' i j k
+    simp_all only [not_false_eq_true, implies_true]
+    split
+    · simp_all only [not_false_eq_true]
+    · simp_all only [not_and, not_lt, Pi.top_apply, top]
+  )
+
+def positionClauses (G : Graph) : VCnf G.vertexSize (positionConstraints G) :=
+  ( let U := Array.finRange G.vertexSize
+    let V := Array.finRange (G.vertexSize+1)
+    seq[
+      for_all V fun j =>
+        addClause (List.toArray (verticesAtPosition j)),
+      for_all V fun j =>
+      for_all U fun i =>
+      for_all U fun k =>
+        VEncCNF.guard (i ≠ k) fun _ =>
+          addClause (#[mkNeg <| Var.mk i j, mkNeg <| Var.mk k j])
+  ])
+  |> mapProp (by
+    ext τ
+    simp [Clause.toPropFun]
+    intro _
+    apply Iff.intro
+    intro h' i j k j_neq_k
+    have := h' i j k
+    simp [j_neq_k] at this
+    exact this
+    intro h' j i k
+    split
+    simp
+    have := h' j i k
+    next h'' => simp [h'', this]
+  )
+
+def edgeClauses (G : Graph) : VCnf G.vertexSize (edgeConstraints G) :=
+  ( let U := Array.finRange G.vertexSize
+    let V := Array.finRange (G.vertexSize+1)
+    for_all V fun k =>
+    for_all V fun k' =>
+      VEncCNF.guard (k.val + 1 = k'.val) fun _ =>
+        for_all U fun i =>
+        for_all U fun j =>
+          VEncCNF.guard (¬G.adjacent i j) fun _ =>
+            addClause (#[mkNeg <| Var.mk i k, mkNeg <| Var.mk j k'])
+  )
+  |> mapProp (by
+    ext τ
+    simp [Clause.toPropFun]
+    apply Iff.intro
+    intro h k k' h'' i j h'''
+    have := h k k'
+    simp [h''] at this
+    have := this i j
+    simp [h''] at this
+    rename_i this_1
+    simp_all only [↓reduceIte]
+    aesop
+  )
+
+def firstAndLastVertexClauses (G : Graph) (h : 0 < G.vertexSize) : VCnf G.vertexSize (firstAndLastConstraints G h) :=
+  (seq[
+    addClause #[mkPos <| Var.mk ⟨0, h⟩ 0],
+    addClause #[mkPos <| Var.mk ⟨0, h⟩ G.vertexSize]
+  ])
+  |> mapProp (by
+    ext τ
+    simp [Clause.toPropFun]
+  )
+
+def hamiltonianCycleCNF (G : Graph) (h : 0 < G.vertexSize) : VCnf G.vertexSize (hamiltonianCycleConstraints G h) :=
+  (seq[
+    vertexClauses G, positionClauses G, edgeClauses G, firstAndLastVertexClauses G h
+  ])
+  |> mapProp (by aesop)
+
+end HamiltonianCycle
+end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean b/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean
new file mode 100644
index 0000000..31dcf5d
--- /dev/null
+++ b/LeanHoG/Invariant/HamiltonianCycle/Tactic.lean
@@ -0,0 +1,137 @@
+import Lean
+import Qq
+import LeanHoG.LoadGraph
+import LeanHoG.Invariant.HamiltonianCycle.SatEncoding
+import LeanHoG.Invariant.HamiltonianCycle.Certificate
+import LeanHoG.Tactic.Options
+import LeanHoG.Util.LeanSAT
+
+import LeanSAT
+
+namespace LeanHoG
+
+open HamiltonianCycle Lean Elab Qq
+
+open LeanSAT Model in
+unsafe def searchForHamiltonianCycleAux (graph : Q(Graph)) :
+  TermElabM (Option Expr) := do
+  let G ← Meta.evalExpr' Graph ``Graph graph
+  if h : 0 < G.vertexSize then
+    let enc := (hamiltonianCycleCNF G h).val
+    let opts ← getOptions
+    let solverExe := opts.get leanHoG.solverCmd.name leanHoG.solverCmd.defValue
+    let checkerExe := opts.get leanHoG.proofCheckerCmd.name leanHoG.proofCheckerCmd.defValue
+    let solver := SolverWithCakeLpr.SolverWithCakeLpr solverExe #["--no-binary", "--lrat=true"] checkerExe
+    let cnf := Encode.EncCNF.toICnf enc
+    let (_, s) := Encode.EncCNF.run enc
+    let res ← solver.solve cnf
+    match res with
+    | .sat assn =>
+      -- Build a Hamiltonian cycle from the solution given by the SAT solver
+      let mut cycle : Array Nat := Array.mkArray (G.vertexSize+1) 0
+      for i in List.fins G.vertexSize do
+        for j in List.fins (G.vertexSize+1) do
+          match assn.find? (s.vMap (Var.mk i j))  with
+          | none => throwError "invalid index ({i},{j})"
+          | some true => cycle := cycle.set! j i
+          | some false => continue
+      let hpQ := hamiltonianCycleOfData graph ⟨cycle.toList⟩
+      return some hpQ
+    | .unsat =>
+      -- TODO: Not yet implemented
+      return none
+    | .error => throwError "SAT solver exited with error"
+  else
+    throwError "cannot construct Hamiltonian cycle for empty graph"
+
+
+------------------------------------------
+-- Find Hamiltonian cycle command
+------------------------------------------
+
+unsafe def checkHamiltonianCycleAux (graphName : Name) (graph : Q(Graph)) : TermElabM Bool := do
+  -- Check if there already exists an instance of a Hamiltonian cycle for g
+  let inst ← Qq.trySynthInstanceQ q(HamiltonianCycle $graph)
+  match inst with
+  | .some _ =>
+    logInfo "Hamiltonian cycle found"
+    return true
+  | _ =>
+    let hpQOpt ← searchForHamiltonianCycleAux graph
+    match hpQOpt with
+    | some hpQ =>
+      let hamiltonianCycleName := certificateName graphName "HamiltonianCycleI"
+      Lean.addAndCompile <| .defnDecl {
+        name := hamiltonianCycleName
+        levelParams := []
+        type := q(HamiltonianCycle $graph)
+        value := hpQ
+        hints := .regular 0
+        safety := .safe
+      }
+      Lean.Meta.addInstance hamiltonianCycleName .scoped 42
+      logInfo "Hamiltonian cycle found"
+      return true
+    | none =>
+      logWarning s!"Hamiltonian cycle not found after exhaustive search"
+      return false
+
+syntax (name := checkHamiltonian) "#check_hamiltonian " ident : command
+/-- `#check_hamiltonian G` runs a SAT solver on the encoding of the Hamiltonian cycle problem
+    on the graph `G` and if the SAT solver says the problem is unsat it runs the produced proof
+    through a verified proof checker cake_lpr. If the checker agrees with the proof, we add an axiom
+    saying there exists no satisfying assignmment for the encoding.
+-/
+@[command_elab checkHamiltonian]
+unsafe def checkHamiltonianImpl : Command.CommandElab
+  | `(#check_hamiltonian $g) => Command.liftTermElabM do
+    let graphName := g.getId
+    let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
+    let _ ← checkHamiltonianCycleAux graphName graph
+
+  | _ => throwUnsupportedSyntax
+
+------------------------------------------
+-- Find Hamiltonian cycle tactic
+------------------------------------------
+-- TODO: Remove code duplication once I figure out how to do it corectly.
+
+unsafe def checkHamiltonianTacticAux (graphName : Name) (graph : Q(Graph)) (hypName : Name) :
+  Tactic.TacticM Unit := do
+  let isHamiltonian ← checkHamiltonianCycleAux graphName graph
+  if isHamiltonian then
+    let existsHamPath ← Meta.mkAppM ``LeanHoG.HamiltonianPath.path_of_cert #[]
+    let existsType := q(Graph.traceable $graph)
+    Tactic.liftMetaTactic fun mvarId => do
+      let mvarIdNew ← mvarId.assert hypName existsHamPath existsType
+      let (_, mvarIdNew) ← mvarIdNew.intro1P
+      return [mvarIdNew]
+  else
+    throwError "cannot prove non-Hamiltonicity, not implemented!"
+
+syntax (name := checkHamiltonianTactic) "check_hamiltonian " ident (" with" (ppSpace colGt ident))? : tactic
+open LeanSAT Model in
+/-- `#check_hamiltonian G` runs a SAT solver on the encoding of the Hamiltonian cycle problem
+    on the graph `G` and if the SAT solver says the problem is unsatisfiable it runs the produced proof
+    through a verified proof checker cake_lpr. If the checker agrees with the proof, we add an axiom
+    saying there exists no satisfying assignmment for the encoding. The tactic uses the new axiom to
+    deduce that there is no Hamiltonian cycle in the graph by using theorem and adds it
+    as a hypothesis to the current context.
+-/
+@[tactic checkHamiltonianTactic]
+unsafe def checkHamiltonianTacticImpl : Tactic.Tactic
+  | `(tactic|check_hamiltonian $g) =>
+    Tactic.withMainContext do
+      let graphName := g.getId
+      let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
+      checkHamiltonianTacticAux graphName graph .anonymous
+
+  | `(tactic|check_hamiltonian $g with $h) =>
+    Tactic.withMainContext do
+      let graphName := g.getId
+      let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
+      checkHamiltonianTacticAux graphName graph h.getId
+
+  | _ => throwUnsupportedSyntax
+
+end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianPath/Basic.lean b/LeanHoG/Invariant/HamiltonianPath/Basic.lean
index 3cc3e9e..215fde4 100644
--- a/LeanHoG/Invariant/HamiltonianPath/Basic.lean
+++ b/LeanHoG/Invariant/HamiltonianPath/Basic.lean
@@ -106,30 +106,5 @@ example {α : Type} [DecidableEq α] (l : List α) (d : l.Nodup) : Finset.card (
 
 end HamiltonianPath
 
-@[simp] def Cycle.isHamiltonian {g : Graph} {u : g.vertex} (c : Cycle g u) : Bool :=
-  ∀ (v : g.vertex), List.contains c.cycle.vertices v
-
-class HamiltonianCycle (g : Graph)  where
-  u : g.vertex
-  cycle : Cycle g u
-  isHamiltonian : cycle.isHamiltonian = true
-
-instance {g : Graph} : Repr (HamiltonianCycle g) where
-  reprPrec p n := reprPrec p.cycle n
-
-instance {g : Graph} : Repr (HamiltonianCycle g) where
-  reprPrec p n := reprPrec p.2.cycle n
-
-@[simp] def Graph.isHamiltonian (g : Graph) : Prop :=
-  ∃ (u : g.vertex) (c : Cycle g u), c.isHamiltonian
-
-@[simp] def Graph.isNonHamiltonian (g : Graph) : Prop := ¬ g.isHamiltonian
-
-@[simp] def Graph.isNonHamiltonian' {g : Graph} : Prop :=
-  ∀ (u : g.vertex) (c : Cycle g u), ¬c.isHamiltonian
-
-theorem equivNonHamiltonianDefs (g : Graph) :
-  g.isNonHamiltonian ↔ g.isNonHamiltonian' :=
-  by simp
 
 end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianPath/Certificate.lean b/LeanHoG/Invariant/HamiltonianPath/Certificate.lean
index c4e2e7e..5fac11f 100644
--- a/LeanHoG/Invariant/HamiltonianPath/Certificate.lean
+++ b/LeanHoG/Invariant/HamiltonianPath/Certificate.lean
@@ -13,7 +13,7 @@ def hamiltonianPathOfData (G : Q(Graph)) (D : HamiltonianPathData) : Q(Hamiltoni
   let rec fold (t : Q(Graph.vertex $G)) :
     List Q(Graph.vertex $G) → ((s : Q(Graph.vertex $G)) ×' Q(Walk $G $s $t)) := fun vs =>
     match vs with
-    | [] => panic! "Shouldn't be here"
+    | [] => panic! "given empty path, cannot construct Hamiltonian path"
     | [v] =>
       let h : Q($v = $t) := (q(Eq.refl $v) : Lean.Expr)
       ⟨v, q($h ▸ .here $v)⟩
diff --git a/LeanHoG/Invariant/HamiltonianPath/SatEncoding.lean b/LeanHoG/Invariant/HamiltonianPath/SatEncoding.lean
index d5980dd..03b88da 100644
--- a/LeanHoG/Invariant/HamiltonianPath/SatEncoding.lean
+++ b/LeanHoG/Invariant/HamiltonianPath/SatEncoding.lean
@@ -8,6 +8,7 @@ import Lean
 import LeanSAT
 
 namespace LeanHoG
+namespace HamiltonianPath
 
 open Lean LeanSAT Encode VEncCNF Meta Model PropFun
 
@@ -299,4 +300,5 @@ def tryFindHamiltonianPath [Solver IO] (G : Graph) :
     else
       return none
 
+end HamiltonianPath
 end LeanHoG
diff --git a/LeanHoG/Invariant/HamiltonianPath/Tactic.lean b/LeanHoG/Invariant/HamiltonianPath/Tactic.lean
index c36292e..8457a10 100644
--- a/LeanHoG/Invariant/HamiltonianPath/Tactic.lean
+++ b/LeanHoG/Invariant/HamiltonianPath/Tactic.lean
@@ -11,9 +11,9 @@ namespace LeanHoG
 
 open Lean Elab Qq
 
-open LeanSAT Model in
-unsafe def searchForHamiltonianPathAux (graphName : Name) (graph : Q(Graph)) :
-  TermElabM (Expr × Expr × Solver.Res) := do
+open LeanSAT Model HamiltonianPath in
+unsafe def searchForHamiltonianPathAux (graph : Q(Graph)) :
+  TermElabM (Option Expr) := do
   let G ← Meta.evalExpr' Graph ``Graph graph
   let enc := (hamiltonianPathCNF G).val
   let opts ← getOptions
@@ -34,42 +34,51 @@ unsafe def searchForHamiltonianPathAux (graphName : Name) (graph : Q(Graph)) :
         | some true => path := path.set! j i
         | some false => continue
     let hpQ := hamiltonianPathOfData graph ⟨path.toList⟩
-    -- Add a Hamiltonian path instance from the constructed path
-    let hamiltonianPathName := certificateName graphName "HamiltonianPathI"
-    Lean.addAndCompile <| .defnDecl {
-      name := hamiltonianPathName
-      levelParams := []
-      type := q(HamiltonianPath $graph)
-      value := hpQ
-      hints := .regular 0
-      safety := .safe
-    }
-    Lean.Meta.addInstance hamiltonianPathName .scoped 42
-    let existsHamPath ← Meta.mkAppM ``LeanHoG.HamiltonianPath.path_of_cert #[]
-    let existsType := q(Graph.traceable $graph)
-    return (existsType, existsHamPath, res)
+    return hpQ
 
-  | .unsat =>
-    -- The formula is UNSAT, add an axiom saying so
-    let declName : Name := .str graphName "noHamiltonianPathCertificateExists"
-    let type : Q(Prop) := q(¬ (∃ (τ : PropAssignment (Var (Graph.vertexSize $graph))), τ |> hamiltonianPathConstraints $graph))
-    let decl := Declaration.axiomDecl {
-      name        := declName,
-      levelParams := [],
-      type        := type,
-      isUnsafe    := false
-    }
-    trace[Elab.axiom] "{declName} : {type}"
-    Term.ensureNoUnassignedMVars decl
-    addDecl decl
-    logWarning m!"added axiom {declName} : {type}"
-    let noExistsCert ← Qq.elabTermEnsuringTypeQ (mkIdent declName) type
-    let noExistsHamPath ← Meta.mkAppM ``LeanHoG.no_assignment_implies_no_hamiltonian_path' #[noExistsCert]
-    let noExistsType := q(¬ ∃ (u v : Graph.vertex $graph) (p : Path $graph u v), p.isHamiltonian)
-    return (noExistsType, noExistsHamPath, res)
+  | .unsat => return none
 
   | .error => throwError "SAT solver exited with error"
 
+open LeanSAT Model HamiltonianPath in
+unsafe def checkHamiltonianPathAux (graphName : Name) (graph : Q(Graph)) : TermElabM Bool := do
+  -- Check if there already exists an instance of a Hamiltonian cycle for g
+  let inst ← Qq.trySynthInstanceQ q(HamiltonianPath $graph)
+  match inst with
+  | .some _ =>
+    logInfo "Hamiltonian path found"
+    return true
+  | _ =>
+    let hpQOpt ← searchForHamiltonianPathAux graph
+    match hpQOpt with
+    | some hpQ =>
+      let hamiltonianPathName := certificateName graphName "HamiltonianPathI"
+      Lean.addAndCompile <| .defnDecl {
+        name := hamiltonianPathName
+        levelParams := []
+        type := q(HamiltonianPath $graph)
+        value := hpQ
+        hints := .regular 0
+        safety := .safe
+      }
+      Lean.Meta.addInstance hamiltonianPathName .scoped 42
+      logInfo "Hamiltonian cycle found"
+      return true
+    | none => -- Graph is non Hamiltonian
+      logInfo s!"Hamiltonian path not found after exhaustive search"
+      let declName : Name := .str graphName "noHamiltonianPathCertificateExists"
+      let type : Q(Prop) := q(¬ (∃ (τ : PropAssignment (Var (Graph.vertexSize $graph))), τ |> hamiltonianPathConstraints $graph))
+      let decl := Declaration.axiomDecl {
+        name        := declName,
+        levelParams := [],
+        type        := type,
+        isUnsafe    := false
+      }
+      trace[Elab.axiom] "{declName} : {type}"
+      Term.ensureNoUnassignedMVars decl
+      addDecl decl
+      logWarning m!"added axiom {declName} : {type}"
+      return false
 
 ------------------------------------------
 -- Find Hamiltonian path command
@@ -86,11 +95,7 @@ unsafe def checkTraceableImpl : Command.CommandElab
   | `(#check_traceable $g) => Command.liftTermElabM do
     let graphName := g.getId
     let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
-    let (declName, _, res) ← searchForHamiltonianPathAux graphName graph
-    match res with
-    | .sat _ => logInfo m!"found Hamiltonian path {declName}"
-    | .unsat => logInfo m!"no Hamiltonian path found after exhaustive search"
-    | .error => throwError "SAT solver exited with error"
+    let _ ← checkHamiltonianPathAux graphName graph
 
   | _ => throwUnsupportedSyntax
 
@@ -99,8 +104,30 @@ unsafe def checkTraceableImpl : Command.CommandElab
 ------------------------------------------
 -- TODO: Remove code duplication once I figure out how to do it corectly.
 
+open LeanSAT Model HamiltonianPath in
+unsafe def checkTraceableTacticAux (graphName : Name) (graph : Q(Graph)) (hypName : Name) :
+  Tactic.TacticM Unit := do
+  let isTraceable ← checkHamiltonianPathAux graphName graph
+  if isTraceable then
+    let existsHamPath ← Meta.mkAppM ``LeanHoG.HamiltonianPath.path_of_cert #[]
+    let existsType := q(Graph.traceable $graph)
+    Tactic.liftMetaTactic fun mvarId => do
+      let mvarIdNew ← mvarId.assert hypName existsHamPath existsType
+      let (_, mvarIdNew) ← mvarIdNew.intro1P
+      return [mvarIdNew]
+  else
+    let type : Q(Prop) := q(¬ (∃ (τ : PropAssignment (Var (Graph.vertexSize $graph))), τ |> hamiltonianPathConstraints $graph))
+    let declName : Name := .str graphName "noHamiltonianPathCertificateExists"
+    let noExistsCert ← Qq.elabTermEnsuringTypeQ (mkIdent declName) type
+    let noExistsHamPath ← Meta.mkAppM ``LeanHoG.HamiltonianPath.no_assignment_implies_no_hamiltonian_path' #[noExistsCert]
+    let noExistsType := q(¬ ∃ (u v : Graph.vertex $graph) (p : Path $graph u v), p.isHamiltonian)
+    Tactic.liftMetaTactic fun mvarId => do
+      let mvarIdNew ← mvarId.assert hypName noExistsType noExistsHamPath
+      let (_, mvarIdNew) ← mvarIdNew.intro1P
+      return [mvarIdNew]
+
 syntax (name := checkTraceableTactic) "check_traceable " ident (" with" (ppSpace colGt ident))? : tactic
-open LeanSAT Model in
+open LeanSAT Model HamiltonianPath in
 /-- `#check_traceable G` runs a SAT solver on the encoding of the Hamiltonian path problem
     on the graph `G` and if the SAT solver says the problem is unsatisfiable it runs the produced proof
     through a verified proof checker cake_lpr. If the checker agrees with the proof, we add an axiom
@@ -116,21 +143,13 @@ unsafe def checkTraceableTacticImpl : Tactic.Tactic
     Tactic.withMainContext do
       let graphName := g.getId
       let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
-      let (val, type, _) ← searchForHamiltonianPathAux graphName graph
-      Tactic.liftMetaTactic fun mvarId => do
-        let mvarIdNew ← mvarId.assert .anonymous val type
-        let (_, mvarIdNew) ← mvarIdNew.intro1P
-        return [mvarIdNew]
+      checkTraceableTacticAux graphName graph .anonymous
 
   | `(tactic|check_traceable $g with $ident) =>
     Tactic.withMainContext do
       let graphName := g.getId
       let graph ← Qq.elabTermEnsuringTypeQ g q(Graph)
-      let (val, type, _) ← searchForHamiltonianPathAux graphName graph
-      Tactic.liftMetaTactic fun mvarId => do
-        let mvarIdNew ← mvarId.assert ident.getId val type
-        let (_, mvarIdNew) ← mvarIdNew.intro1P
-        return [mvarIdNew]
+      checkTraceableTacticAux graphName graph ident.getId
 
   | _ => throwUnsupportedSyntax
 
diff --git a/LeanHoG/Tactic/Basic.lean b/LeanHoG/Tactic/Basic.lean
index 10cfe97..bd4aa24 100644
--- a/LeanHoG/Tactic/Basic.lean
+++ b/LeanHoG/Tactic/Basic.lean
@@ -9,6 +9,7 @@ import LeanHoG.Tactic.Options
 import LeanHoG.Tactic.ParseExpr
 import LeanHoG.Invariant.HamiltonianPath.Basic
 import LeanHoG.Invariant.HamiltonianPath.Tactic
+import LeanHoG.Invariant.HamiltonianCycle.Tactic
 
 namespace LeanHoG
 
@@ -56,6 +57,13 @@ unsafe def downloadHoGImpl : Elab.Command.CommandElab
 -- Search tactic
 -----------------------------------------------------------------
 
+open Lean Qq in
+unsafe def solveBoolInvariantWith : BoolInvariant →
+  Meta.MetaM (Name → Q(Graph) → Name → Elab.Tactic.TacticM Unit)
+  | .Traceable => return checkTraceableTacticAux
+  | .Hamiltonian => return checkHamiltonianTacticAux
+  | inv => throwError s!"tactic for solving {inv} not implemented"
+
 syntax (name := findExample) "find_example" : tactic
 
 open Lean Qq Elab Tactic in
@@ -80,7 +88,10 @@ unsafe def findExampleImpl : Tactic.Tactic
       let exists_intro ← Term.mkConst ``Exists.intro
       try
         let enqs ← decomposeExistsQ goalType
-        let mentionsTracability := enqs.any (fun enq => enq.mentionsTracability)
+        -- Find all the invariants the query mentions, for which we need special tactics
+        let mentions := List.foldl (fun ms inv =>
+          if enqs.any (fun enq => enq.mentionsBoolInv inv) then inv :: ms else ms
+        ) [] [.Traceable, .Hamiltonian]
         let hash := hash enqs
         let query := HoGQuery.build enqs
         let graphs ← liftCommandElabM (queryDatabaseForExamplesAux [query] hash)
@@ -110,37 +121,18 @@ unsafe def findExampleImpl : Tactic.Tactic
               goal.withContext do
                 let r ← Lean.Elab.Tactic.elabTermEnsuringType graphIdent goalType
                 goal.assign r
-                -- Now try to simp which will among other things look for instance for e.g. HamiltonianPath
-                if mentionsTracability then
-                  -- If we want to prove things about tracability we need to search for a Hamiltonian path
-                  let (val, type, res) ← LeanHoG.searchForHamiltonianPathAux graphIdent.getId r
-                  match res with
-                  | .unsat =>
-                    Tactic.liftMetaTactic fun mvarId => do
-                      let mvarIdNew ← mvarId.assert .anonymous val type
-                      let (_, mvarIdNew) ← mvarIdNew.intro1P
-                      return [mvarIdNew]
-                    let ctx ← mkSimpContext (← `(tactic|simp_all only [LeanHoG.Graph.no_path_not_traceable, not_false_eq_true])) false
-                    let (result?, _) ← Meta.simpAll (← getMainGoal) ctx.ctx (simprocs := ctx.simprocs)
-                    match result? with
-                    | none => replaceMainGoal []
-                    | some mvarId => replaceMainGoal [mvarId]
-                    Tactic.evalDecide stx
-                  | _ =>
-                    let ctx ← mkSimpContext (← `(tactic|simp_all only [LeanHoG.Graph.no_path_not_traceable, not_false_eq_true])) false
-                    let (result?, _) ← Meta.simpAll (← getMainGoal) ctx.ctx (simprocs := ctx.simprocs)
-                    match result? with
-                    | none => replaceMainGoal []
-                    | some mvarId => replaceMainGoal [mvarId]
-                    Tactic.evalDecide stx
-                else
-                  let ctx ← mkSimpContext (← `(tactic|simp_all)) false
-                  let (result?, _) ← Meta.simpAll (← getMainGoal) ctx.ctx (simprocs := ctx.simprocs)
-                  match result? with
-                  | none => replaceMainGoal []
-                  | some mvarId =>
-                    replaceMainGoal [mvarId]
-                    Tactic.evalDecide stx
+                -- Now run the appropriate tactic for each kind of invariant we're trying to solve
+                for inv in mentions do
+                  let tac ← solveBoolInvariantWith inv
+                  tac graphIdent.getId r .anonymous
+                -- Run `simp` and `decide` on the new goal after using G as the existence target
+                let ctx ← mkSimpContext (← `(tactic|simp_all [LeanHoG.Graph.no_path_not_traceable, not_false_eq_true])) false
+                let (result?, _) ← Meta.simpAll (← getMainGoal) ctx.ctx (simprocs := ctx.simprocs)
+                match result? with
+                | none => replaceMainGoal []
+                | some mvarId =>
+                  replaceMainGoal [mvarId]
+                  Tactic.evalDecide stx
                 Lean.logInfo s!"Closed goal using {graphIdent.getId}"
               -- Visualize the graph we used to close the goal
               -- TODO: Make this an option
diff --git a/LeanHoG/Tactic/ParseExpr.lean b/LeanHoG/Tactic/ParseExpr.lean
index 36049c0..9447093 100644
--- a/LeanHoG/Tactic/ParseExpr.lean
+++ b/LeanHoG/Tactic/ParseExpr.lean
@@ -3,6 +3,7 @@ import LeanHoG.Graph
 import LeanHoG.Tactic.SearchDSL
 import LeanHoG.Tactic.Options
 import LeanHoG.Invariant.HamiltonianPath.Basic
+import LeanHoG.Invariant.HamiltonianCycle.Basic
 import Qq
 
 import Aesop.Util.Basic
diff --git a/LeanHoG/Tactic/SearchDSL.lean b/LeanHoG/Tactic/SearchDSL.lean
index 204d0c8..eeb2de3 100644
--- a/LeanHoG/Tactic/SearchDSL.lean
+++ b/LeanHoG/Tactic/SearchDSL.lean
@@ -25,7 +25,7 @@ inductive BoolInvariant where
   | Regular
   | Traceable
   | TwinFree
-deriving Repr, Hashable
+deriving Repr, Hashable, DecidableEq
 
 instance : ToString BoolInvariant where
   toString := fun i =>
@@ -50,7 +50,7 @@ inductive NumericalInvariant where
   | LaplacianLargestEigenvalue
   | SecondLargestEigenvalue
   | SmallestEigenvalue
-deriving Repr, Hashable
+deriving Repr, Hashable, DecidableEq
 
 instance : ToString NumericalInvariant where
   toString := fun i =>
@@ -343,12 +343,11 @@ instance : ToString HoGEnquiry where
     | .IntegralEnquiry i => toString i
     | .FormulaEnquiry f => toString f
 
-def HoGEnquiry.mentionsTracability : HoGEnquiry → Bool
-  | .BoolEnquiry ⟨.Traceable, _⟩ => true
-  | .BoolEnquiry _ => false
-  | .NumericalEnquiry _ => false
-  | .IntegralEnquiry _ => false
-  | .FormulaEnquiry _ => false
+def HoGEnquiry.mentionsBoolInv : HoGEnquiry → BoolInvariant → Bool
+  | .BoolEnquiry ⟨inv, _⟩, inv' => inv = inv'
+  | .NumericalEnquiry _, _ => false
+  | .IntegralEnquiry _, _ => false
+  | .FormulaEnquiry _, _ => false
 
 structure InvariantQuery where
   invariantId : Nat