HAMPATH is verified with quadratic-size witnesses to The frame of a diamond

TheoremHAMPATH is verified with quadratic-size witnesses#✓fully proved

For every bit string \(x\), \(x\) is a yes-instance of HAMPATH if and only if there is a bit string \(w\) of length at most \((|x| + 1)^2\) such that the HAMPATH verifier accepts \((x, w)\).

theorem hamPathDec_iff (x : List Bool) :
    hamPathDec x = true ↔ ∃ w, w.length ≤ (x.length + 1) ^ 2 ∧ hamCheck x w = true

Uses 10 · Used by 1

Statement usesThe HAMPATH verifier · The HAMPATH problem

Proof usesWitness encoding · What the HAMPATH verifier accepts · Witness length bound · Length of an encoded PATH instance · Hamiltonian paths · Bit encoding of an edge list · Arcs of the PATH digraph · Encoding of a PATH instance

Used byHAMPATH is in NP

DefinitionOne step of the HAMPATH walk#✓fully proved

Given natural numbers \(s\) and \(n\), an edge list \(E\), a count \(c\) of vertices already seen, the previous vertex \(b\), the current vertex \(a\) and the list \(q\) of remaining vertices, the step check is true exactly when \(a < n\), \(a\) does not occur in \(q\), and either \(c = 0\) and \(a = s\), or \(c \neq 0\) and \((b, a) \in E\).

def stepOk (s n : ℕ) (es : List (ℕ × ℕ)) (c b a : ℕ) (q : List ℕ) : Bool :=
  decide (a < n) && (if c = 0 then decide (a = s) else decide ((b, a) ∈ es)) && !decide (a ∈ q)

Used by 5

Used byThe walk check of the HAMPATH verifier · The machine's walk is the check · The walk check after the first vertex · Running the vertex loop · One vertex step of the Hamiltonian-path verifier

DefinitionThe walk check of the HAMPATH verifier#✓fully proved

Fix natural numbers \(s, t, n\) and a list \(E\) of pairs of natural numbers. The walk check accepts a list \(q\) of natural numbers after \(c\) vertices, the last of which was \(b\), by recursion on \(q\). On the empty list it accepts if and only if \(c = n\), \(c \neq 0\) and \(b = t\). On a list with first entry \(a\) and remaining entries \(q'\) it accepts if and only if the step check passes and the walk check accepts \(q'\) after \(c + 1\) vertices, the last of which was \(a\). The step check requires \(a < n\); it requires \(a = s\) when \(c = 0\), and that \((b, a)\) is an entry of \(E\) when \(c \neq 0\); and it requires that \(a\) does not occur in \(q'\).

def walkOk (s t n : ℕ) (es : List (ℕ × ℕ)) : ℕ → ℕ → List ℕ → Bool
  | c, b, [] => decide (c = n) && decide (c ≠ 0) && decide (b = t)
  | c, b, a :: q => stepOk s n es c b a q && walkOk s t n es (c + 1) a q

Uses 1 · Used by 4

Statement usesOne step of the HAMPATH walk

Used byThe machine's walk is the check · The walk check after the first vertex · Running the vertex loop · Correctness and running time of the Hamiltonian path verifier

TheoremThe walk check after the first vertex#✓fully proved

Let \(s, t, n\) be natural numbers and \(E\) a list of pairs of natural numbers. For every list \(q = (q_1, \dots, q_k)\) of natural numbers and all natural numbers \(c \neq 0\) and \(b\), the walk check for \(s, t, n, E\) accepts \(q\) after \(c\) vertices the last of which was \(b\) if and only if every \(q_i\) is less than \(n\), every pair \((u, v)\) of consecutive entries of the list \((b, q_1, \dots, q_k)\) is an entry of \(E\), the entries of \(q\) are pairwise distinct, \(c + k = n\), and the last entry of \((b, q_1, \dots, q_k)\) is \(t\).

theorem walkOk_iff {s t n : ℕ} {es : List (ℕ × ℕ)} : ∀ (q : List ℕ) (c b : ℕ), c ≠ 0 →
    (walkOk s t n es c b q = true ↔ (∀ v ∈ q, v < n) ∧
      (b :: q).IsChain (fun u v => (u, v) ∈ es) ∧ q.Nodup ∧ c + q.length = n ∧
      (b :: q).getLast? = some t)

Uses 2 · Used by 1

Statement usesThe walk check of the HAMPATH verifier

Proof usesOne step of the HAMPATH walk

Used byThe machine's walk is the check

TheoremThe machine's walk is the check#✓fully proved

For all natural numbers \(s\), \(t\), \(n\), every edge list \(E\) and every list \(p\) of natural numbers, the walk over \(p\) started with count \(0\) and previous vertex \(0\) returns the same Boolean value as the Hamiltonian path check on \((n, E, s, t, p)\).

theorem walkOk_eq (s t n : ℕ) (es : List (ℕ × ℕ)) :
    ∀ p, walkOk s t n es 0 0 p = hamOk n es s t p

Uses 8 · Used by 1

Statement usesThe Hamiltonian path check · The walk check of the HAMPATH verifier

Proof usesArc check of a vertex list · The Hamiltonian path check is correct · One step of the HAMPATH walk · The walk check after the first vertex · Hamiltonian paths · Arcs of the PATH digraph

Used byCorrectness and running time of the Hamiltonian path verifier

TheoremTops of distinct diamonds are at least \(3m + 2\) apart#✓fully proved

In the vertex numbering of the Hamiltonian path construction with \(m\) clauses, where the top of diamond \(i\) is the vertex \(T(i) = m + i(3m + 2)\), any two indices \(i \ne i'\) satisfy \(T(i) + 3m + 2 \le T(i')\) or \(T(i') + 3m + 2 \le T(i)\).

theorem hpT_sep {m i i' : ℕ} (h : i ≠ i') :
    hpT m i + (3 * m + 2) ≤ hpT m i' ∨ hpT m i' + (3 * m + 2) ≤ hpT m i

Uses 1 · Used by 7

Statement usesTops of the diamonds

Used byOut-neighbours of a row vertex in Sipser's graph · In-neighbours of a row vertex in Sipser's graph · Arcs from a row into a clause vertex · Out-neighbours of a top · Every top but the last is followed by an end of its row · Entering a row and leaving it at once is impossible · A row entered at one end is run to the other end

TheoremArcs of the Hamiltonian path construction#✓fully proved

Let \(\varphi\) be a CNF formula with clauses \(C_0, \dots, C_{m-1}\) and distinct variables \(x_0, \dots, x_{k-1}\) (in the order the construction lists them), and write \(T(i) = m + i(3m + 2)\) for the top of diamond \(i\) and \(R(i, l) = T(i) + 1 + l\) for its row vertex \(l\). Then \((u, v)\) is an arc of the Hamiltonian path instance of \(\varphi\) if and only if there is an \(i < k\) such that \((u, v)\) is one of the frame arcs \((T(i), R(i, 0))\), \((T(i), R(i, 3m))\), \((R(i, 0), T(i + 1))\) and \((R(i, 3m), T(i + 1))\); or \((u, v)\) is a row arc \((R(i, l), R(i, l + 1))\) or \((R(i, l + 1), R(i, l))\) for some \(l < 3m\); or, for some \(j < m\), either \(C_j\) contains the literal \(x_i\) and \((u, v)\) is \((R(i, 3j + 1), j)\) or \((j, R(i, 3j + 2))\), or \(C_j\) contains the literal \(\lnot x_i\) and \((u, v)\) is \((R(i, 3j + 2), j)\) or \((j, R(i, 3j + 1))\).

theorem mem_hamEdges {φ : CNF} {u v : ℕ} :
    (u, v) ∈ hamEdges φ ↔ ∃ i < (hamVars φ).length,
      ((u = hpT φ.length i ∧ v = hpR φ.length i 0 ∨
          u = hpT φ.length i ∧ v = hpR φ.length i (3 * φ.length) ∨
          u = hpR φ.length i 0 ∧ v = hpT φ.length (i + 1) ∨
          u = hpR φ.length i (3 * φ.length) ∧ v = hpT φ.length (i + 1)) ∨
        ∃ l < 3 * φ.length,
          u = hpR φ.length i l ∧ v = hpR φ.length i (l + 1) ∨
          u = hpR φ.length i (l + 1) ∧ v = hpR φ.length i l) ∨
      ∃ j < φ.length,
        ((hamVars φ).getD i 0, true) ∈ φ.getD j [] ∧
          (u = hpR φ.length i (3 * j + 1) ∧ v = j ∨ u = j ∧ v = hpR φ.length i (3 * j + 2)) ∨
        ((hamVars φ).getD i 0, false) ∈ φ.getD j [] ∧
          (u = hpR φ.length i (3 * j + 2) ∧ v = j ∨ u = j ∧ v = hpR φ.length i (3 * j + 1))

Uses 6 · Used by 3

Statement usesArcs of the HAMPATH construction · Distinct variables of a formula · Row vertices of a diamond · Tops of the diamonds · CNF formula · CNF clause

Used byClassification of the arcs of Sipser's graph · Consecutive vertices of the contracted path are joined by arcs · Arcs from a row into a clause vertex

TheoremClassification of the arcs of Sipser's graph#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables, and write \(T_i = m + i(3m + 2)\) and \(R_{i,l} = T_i + 1 + l\). If \((u, v)\) is an arc of Sipser's construction for \(\varphi\), then there is \(i < k\) such that one of the following holds: \(u = T_i\) and \(v \in \{R_{i,0}, R_{i,3m}\}\); or \(u \in \{R_{i,0}, R_{i,3m}\}\) and \(v = T_{i+1}\); or there is \(l < 3m\) with \((u, v) = (R_{i,l}, R_{i,l+1})\) or \((u, v) = (R_{i,l+1}, R_{i,l})\); or there is \(j < m\) with \(u \in \{R_{i,3j+1}, R_{i,3j+2}\}\) and \(v = j\), or with \(u = j\) and \(v \in \{R_{i,3j+1}, R_{i,3j+2}\}\).

The last case does not record whether the detour comes from a positive or a negative literal.

theorem hamEdges_cases {φ : CNF} {u v : ℕ} (h : (u, v) ∈ hamEdges φ) :
    ∃ i < (hamVars φ).length,
      (u = hpT φ.length i ∧ (v = hpR φ.length i 0 ∨ v = hpR φ.length i (3 * φ.length))) ∨
      ((u = hpR φ.length i 0 ∨ u = hpR φ.length i (3 * φ.length)) ∧
        v = hpT φ.length (i + 1)) ∨
      (∃ l < 3 * φ.length, u = hpR φ.length i l ∧ v = hpR φ.length i (l + 1) ∨
        u = hpR φ.length i (l + 1) ∧ v = hpR φ.length i l) ∨
      (∃ j < φ.length,
        (u = hpR φ.length i (3 * j + 1) ∨ u = hpR φ.length i (3 * j + 2)) ∧ v = j ∨
        u = j ∧ (v = hpR φ.length i (3 * j + 1) ∨ v = hpR φ.length i (3 * j + 2)))

Uses 7 · Used by 5

Statement usesArcs of the HAMPATH construction · Distinct variables of a formula · Row vertices of a diamond · Tops of the diamonds · CNF formula · CNF clause

Proof usesArcs of the Hamiltonian path construction

Used byOut-neighbours of a clause vertex in Sipser's graph · Out-neighbours of a row vertex in Sipser's graph · In-neighbours of a clause vertex in Sipser's graph · In-neighbours of a row vertex in Sipser's graph · Out-neighbours of a top

TheoremIn-neighbours of a row vertex in Sipser's graph#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses, and write \(T_i = m + i(3m + 2)\) and \(R_{i,l} = T_i + 1 + l\). Let \(i\) and \(l \le 3m\) be natural numbers, and let \((v, R_{i,l})\) be an arc of Sipser's construction for \(\varphi\). Then \(l < 3m\) and \(v = R_{i,l+1}\); or \(0 < l\) and \(v = R_{i,l-1}\); or \(l \in \{0, 3m\}\) and \(v = T_i\); or \(v < m\) and \(l \in \{3v + 1, 3v + 2\}\).

theorem hamEdges_to_hpR {φ : CNF} {v i l : ℕ} (h : (v, hpR φ.length i l) ∈ hamEdges φ)
    (hl : l ≤ 3 * φ.length) :
    (l < 3 * φ.length ∧ v = hpR φ.length i (l + 1)) ∨ (0 < l ∧ v = hpR φ.length i (l - 1)) ∨
      ((l = 0 ∨ l = 3 * φ.length) ∧ v = hpT φ.length i) ∨
      (v < φ.length ∧ (l = 3 * v + 1 ∨ l = 3 * v + 2))

Uses 8 · Used by 4

Statement usesArcs of the HAMPATH construction · Row vertices of a diamond · Tops of the diamonds · CNF formula · CNF clause

Proof usesClassification of the arcs of Sipser's graph · Distinct variables of a formula · Tops of distinct diamonds are at least \(3m + 2\) apart

Used byA clause detour returns to its own pair (Sipser's separator argument) · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A separator is next to each of its row neighbours on a Hamiltonian path · In-neighbours of a row vertex outside the clause vertices

TheoremOut-neighbours of a row vertex in Sipser's graph#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses, and write \(T_i = m + i(3m + 2)\) and \(R_{i,l} = T_i + 1 + l\). Let \(i\) and \(l \le 3m\) be natural numbers, and let \((R_{i,l}, v)\) be an arc of Sipser's construction for \(\varphi\). Then \(l < 3m\) and \(v = R_{i,l+1}\); or \(0 < l\) and \(v = R_{i,l-1}\); or \(l \in \{0, 3m\}\) and \(v = T_{i+1}\); or \(v < m\) and \(l \in \{3v + 1, 3v + 2\}\).

theorem hamEdges_from_hpR {φ : CNF} {v i l : ℕ} (h : (hpR φ.length i l, v) ∈ hamEdges φ)
    (hl : l ≤ 3 * φ.length) :
    (l < 3 * φ.length ∧ v = hpR φ.length i (l + 1)) ∨ (0 < l ∧ v = hpR φ.length i (l - 1)) ∨
      ((l = 0 ∨ l = 3 * φ.length) ∧ v = hpT φ.length (i + 1)) ∨
      (v < φ.length ∧ (l = 3 * v + 1 ∨ l = 3 * v + 2))

Uses 8 · Used by 4

Statement usesArcs of the HAMPATH construction · Row vertices of a diamond · Tops of the diamonds · CNF formula · CNF clause

Proof usesClassification of the arcs of Sipser's graph · Distinct variables of a formula · Tops of distinct diamonds are at least \(3m + 2\) apart

Used byA clause detour returns to its own pair (Sipser's separator argument) · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A separator is next to each of its row neighbours on a Hamiltonian path · Out-neighbours of a row vertex outside the clause vertices

TheoremIn-neighbours of a clause vertex in Sipser's graph#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables, and write \(R_{i,l} = m + i(3m + 2) + 1 + l\) for row vertex \(l\) of diamond \(i\). If \(j < m\) and \((v, j)\) is an arc of Sipser's construction for \(\varphi\), then there is \(i < k\) with \(v = R_{i,3j+1}\) or \(v = R_{i,3j+2}\).

theorem hamEdges_to_clause {φ : CNF} {v j : ℕ} (h : (v, j) ∈ hamEdges φ) (hj : j < φ.length) :
    ∃ i < (hamVars φ).length,
      v = hpR φ.length i (3 * j + 1) ∨ v = hpR φ.length i (3 * j + 2)

Uses 7 · Used by 1

Statement usesArcs of the HAMPATH construction · Distinct variables of a formula · Row vertices of a diamond · CNF formula · CNF clause

Proof usesClassification of the arcs of Sipser's graph · Tops of the diamonds

Used byHamiltonian paths of Sipser's graph have normal detours

TheoremOut-neighbours of a clause vertex in Sipser's graph#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables, and write \(R_{i,l} = m + i(3m + 2) + 1 + l\) for row vertex \(l\) of diamond \(i\). If \(j < m\) and \((j, v)\) is an arc of Sipser's construction for \(\varphi\), then there is \(i < k\) with \(v = R_{i,3j+1}\) or \(v = R_{i,3j+2}\).

theorem hamEdges_from_clause {φ : CNF} {v j : ℕ} (h : (j, v) ∈ hamEdges φ) (hj : j < φ.length) :
    ∃ i < (hamVars φ).length,
      v = hpR φ.length i (3 * j + 1) ∨ v = hpR φ.length i (3 * j + 2)

Uses 7

Statement usesArcs of the HAMPATH construction · Distinct variables of a formula · Row vertices of a diamond · CNF formula · CNF clause

Proof usesClassification of the arcs of Sipser's graph · Tops of the diamonds

TheoremA Hamiltonian path visits every vertex#✓fully proved

If \(p\) is a Hamiltonian path from \(s\) to \(t\) in the digraph on the vertices \(0, \dots, n - 1\) with arc list \(E\), then every vertex \(v < n\) occurs in \(p\).

theorem mem_of_isHamPath {n s t : ℕ} {es : List (ℕ × ℕ)} {p : List ℕ}
    (h : IsHamPath n es s t p) {v : ℕ} (hv : v < n) : v ∈ p

Uses 2 · Used by 8

Statement usesHamiltonian paths

Proof usesArcs of the PATH digraph

Used byHamiltonian paths of Sipser's graph have normal detours · A clause detour returns to its own pair (Sipser's separator argument) · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A separator is next to each of its row neighbours on a Hamiltonian path · Consecutive vertices of the contracted path are joined by arcs · Every top but the last is followed by an end of its row · Entering a row and leaving it at once is impossible · A row entered at one end is run to the other end

TheoremConsecutive vertices of a Hamiltonian path of Sipser's graph form arcs#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables, let \(T_i = m + i(3m + 2)\), and let \(p\) be a Hamiltonian path from \(T_0\) to \(T_k\) in the digraph on the vertices \(0, \dots, T_k\) whose arcs are those of Sipser's construction for \(\varphi\). If \(v\) comes immediately after \(u\) in \(p\), then \((u, v)\) is an arc of the construction.

theorem hamEdges_of_infix {u v : ℕ} (hn : [u, v] <:+: p) : (u, v) ∈ hamEdges φ

Uses 7 · Used by 5

Statement usesHamiltonian paths · Arcs of the HAMPATH construction · Distinct variables of a formula · Tops of the diamonds · CNF formula · CNF clause

Proof usesArcs of the PATH digraph

Used byHamiltonian paths of Sipser's graph have normal detours · A clause detour returns to its own pair (Sipser's separator argument) · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A separator is next to each of its row neighbours on a Hamiltonian path · Backward direction of SAT ≤ HAMPATH for paths with normal detours

TheoremA Hamiltonian path of Sipser's graph does not cross a diamond through one row end#✓fully proved

Let \(\varphi\) be a CNF formula with \(m \ge 1\) clauses and \(k\) distinct variables, write \(T_i = m + i(3m + 2)\) and \(R_{i,l} = T_i + 1 + l\), and let \(p\) be a Hamiltonian path from \(T_0\) to \(T_k\) in the digraph on the vertices \(0, \dots, T_k\) whose arcs are those of Sipser's construction for \(\varphi\). For \(i < k\) and \(l \in \{0, 3m\}\), it is impossible that \(R_{i,l}\) comes immediately after \(T_i\) in \(p\) and \(T_{i+1}\) comes immediately after \(R_{i,l}\) in \(p\).

theorem hamPath_rowEnd_false {i l : ℕ} (hi : i < (hamVars φ).length) (hm : 0 < φ.length)
    (hl : l = 0 ∨ l = 3 * φ.length) (h₁ : [hpT φ.length i, hpR φ.length i l] <:+: p)
    (h₂ : [hpR φ.length i l, hpT φ.length (i + 1)] <:+: p) : False

Uses 12 · Used by 1

Statement usesHamiltonian paths · Arcs of the HAMPATH construction · Distinct variables of a formula · Row vertices of a diamond · Tops of the diamonds · CNF formula · CNF clause

Proof usesOut-neighbours of a row vertex in Sipser's graph · Consecutive vertices of a Hamiltonian path of Sipser's graph form arcs · In-neighbours of a row vertex in Sipser's graph · A Hamiltonian path visits every vertex · Arcs of the PATH digraph

Used byA separator is next to each of its row neighbours on a Hamiltonian path

TheoremA separator is next to each of its row neighbours on a Hamiltonian path#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables, write \(T_i = m + i(3m + 2)\) and \(R_{i,l} = T_i + 1 + l\), and let \(p\) be a Hamiltonian path from \(T_0\) to \(T_k\) in the digraph on the vertices \(0, \dots, T_k\) whose arcs are those of Sipser's construction for \(\varphi\). Let \(i < k\), let \(l \le 3m\) be a multiple of \(3\), and let \(l' \le 3m\) satisfy \(l' = l + 1\) or \(l' + 1 = l\). Then \(R_{i,l'}\) comes immediately before or immediately after \(R_{i,l}\) in \(p\).

theorem hamPath_separator_false {i l lw : ℕ} (hi : i < (hamVars φ).length) (hl3 : l % 3 = 0)
    (hl : l ≤ 3 * φ.length) (hw : lw = l + 1 ∨ lw + 1 = l) (hwm : lw ≤ 3 * φ.length)
    (h₁ : ¬ [hpR φ.length i lw, hpR φ.length i l] <:+: p)
    (h₂ : ¬ [hpR φ.length i l, hpR φ.length i lw] <:+: p) : False

Uses 13 · Used by 1

Statement usesHamiltonian paths · Arcs of the HAMPATH construction · Distinct variables of a formula · Row vertices of a diamond · Tops of the diamonds · CNF formula · CNF clause

Proof usesOut-neighbours of a row vertex in Sipser's graph · Consecutive vertices of a Hamiltonian path of Sipser's graph form arcs · In-neighbours of a row vertex in Sipser's graph · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A Hamiltonian path visits every vertex · Arcs of the PATH digraph

Used byA clause detour returns to its own pair (Sipser's separator argument)

TheoremA clause detour returns to its own pair (Sipser's separator argument)#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables, write \(T_i = m + i(3m + 2)\) and \(R_{i,l} = T_i + 1 + l\), and let \(p\) be a Hamiltonian path from \(T_0\) to \(T_k\) in the digraph on the vertices \(0, \dots, T_k\) whose arcs are those of Sipser's construction for \(\varphi\). Let \(i < k\) and \(j < m\), and let \((l_a, l_c)\) be \((3j + 1, 3j + 2)\) or \((3j + 2, 3j + 1)\). If the clause vertex \(j\) comes immediately after \(R_{i,l_a}\) in \(p\), then every vertex that comes immediately after \(j\) in \(p\) is \(R_{i,l_c}\).

theorem hamPath_pair_false {i j la lc b : ℕ} (hi : i < (hamVars φ).length) (hj : j < φ.length)
    (hlac : (la = 3 * j + 1 ∧ lc = 3 * j + 2) ∨ (la = 3 * j + 2 ∧ lc = 3 * j + 1))
    (ha : [hpR φ.length i la, j] <:+: p) (hb : [j, b] <:+: p) (hbc : b ≠ hpR φ.length i lc) :
    False

Uses 13 · Used by 1

Statement usesHamiltonian paths · Arcs of the HAMPATH construction · Distinct variables of a formula · Row vertices of a diamond · Tops of the diamonds · CNF formula · CNF clause

Proof usesOut-neighbours of a row vertex in Sipser's graph · Consecutive vertices of a Hamiltonian path of Sipser's graph form arcs · In-neighbours of a row vertex in Sipser's graph · A separator is next to each of its row neighbours on a Hamiltonian path · A Hamiltonian path visits every vertex · Arcs of the PATH digraph

Used byHamiltonian paths of Sipser's graph have normal detours

TheoremHamiltonian paths of Sipser's graph have normal detours#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables, and write \(T_i = m + i(3m + 2)\) and \(R_{i,l} = T_i + 1 + l\) for the top and the row vertices of diamond \(i\). Every Hamiltonian path from \(T_0\) to \(T_k\) in the digraph on the vertices \(0, \dots, T_k\) whose arcs are those of Sipser's construction for \(\varphi\) has normal detours: for every clause \(j < m\) there is \(i < k\) such that \(R_{i,3j+1}, j, R_{i,3j+2}\) or \(R_{i,3j+2}, j, R_{i,3j+1}\) occur in this order as consecutive vertices of the path.

theorem detoursNormal_of_isHamPath {φ : CNF} {p : List ℕ}
    (h : IsHamPath (hpT φ.length (hamVars φ).length + 1) (hamEdges φ)
      (hpT φ.length 0) (hpT φ.length (hamVars φ).length) p) :
    DetoursNormal φ p

Uses 13 · Used by 1

Statement usesNormal clause detours · Hamiltonian paths · Arcs of the HAMPATH construction · Distinct variables of a formula · Tops of the diamonds · CNF formula · CNF clause

Proof usesConsecutive vertices of a Hamiltonian path of Sipser's graph form arcs · In-neighbours of a clause vertex in Sipser's graph · A clause detour returns to its own pair (Sipser's separator argument) · Row vertices of a diamond · A Hamiltonian path visits every vertex · Arcs of the PATH digraph

Used byThe construction has a Hamiltonian path iff the formula is satisfiable

TheoremThe HAMPATH instance as unary blocks and arc bits#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables, and let \(t = m + k(3m + 2)\) be the top of diamond \(k\). Then the HAMPATH instance of \(\varphi\) is the bit string made of \(m\) ones and a zero (the start vertex \(s = m\)), then \(t\) ones and a zero (the target vertex \(t\)), then \(t + 1\) ones and a zero (the vertex count \(n = t + 1\)), followed by the arcs of the construction, each arc \((u, v)\) written as \(u\) ones, a zero, \(v\) ones and a zero.

theorem toHam_eq (φ : CNF) : toHam φ = List.replicate φ.length true ++ false ::
    (List.replicate (hpT φ.length (hamVars φ).length) true ++ false ::
      (List.replicate (hpT φ.length (hamVars φ).length + 1) true ++ false ::
        Karp.edgeBits (hamEdges φ)))

Uses 7 · Used by 1

Statement usesBit encoding of an edge list · Arcs of the HAMPATH construction · Distinct variables of a formula · Tops of the diamonds · Sipser's HAMPATH instance of a CNF formula · CNF formula · CNF clause

Used byCorrectness and running time of the HAMPATH emitter

DefinitionThe frame of a diamond#✓fully proved

For natural numbers \(m\) (the number of clauses) and \(i\), write \(t_i = m + i(3m + 2)\) for the top of diamond \(i\) and \(r_{i,l} = t_i + 1 + l\) for its row vertex \(l\). The frame of diamond \(i\) is the list of the four arcs \((t_i, r_{i,0})\), \((t_i, r_{i,3m})\), \((r_{i,0}, t_{i+1})\) and \((r_{i,3m}, t_{i+1})\): the top points to both row ends, and both row ends point to the top of the next diamond.

def frameE (m i : ℕ) : List (ℕ × ℕ) :=
  [(hpT m i, hpR m i 0), (hpT m i, hpR m i (3 * m)), (hpR m i 0, hpT m (i + 1)),
    (hpR m i (3 * m), hpT m (i + 1))]

Uses 2 · Used by 3

Statement usesRow vertices of a diamond · Tops of the diamonds

Used byFront of a diamond · One diamond · Correctness and running time of the HAMPATH emitter

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.