The repeat scan of the Hamiltonian path verifier to HAMPATH is NP-complete

TheoremThe repeat scan of the Hamiltonian path verifier#✓fully proved

For a list \(p\) of natural numbers write \(\mathrm{enc}(p)\) for its witness encoding: each entry in unary (that many copies of true) followed by false. Let \(a\) be a natural number and \(q\), \(d\) lists of natural numbers. Suppose that the verifier's stacks hold, as bit symbols with the first bit on top, the bits of \(\mathrm{enc}(q)\) on \(\mathsf{W}\), the bits of \(\mathrm{enc}(d)\) in reverse order on \(\mathsf{Z}\), \(a\) copies of the bit true on \(\mathsf{A}\), and nothing on \(\mathsf{R}\), the other stacks being arbitrary. Started at label \(\mathrm{nd}\) with either value of its Boolean variable, the verifier reaches, within \(4|\mathrm{enc}(q)| + |\mathrm{enc}(d)| + 2\) steps, the label \(\mathrm{no}\) if \(a\) is an entry of \(q\) and the label \(\mathrm{incC}\) otherwise. In the second case its stacks are then the initial ones except that \(\mathsf{W}\) holds the bits of the encoding of \(d\) followed by \(q\), and \(\mathsf{Z}\) is empty.

theorem nd_run (a : ℕ) : ∀ (q done : List ℕ) (v : Bool) (St : ∀ _ : K, List Sym),
    St .W = (encW q).map Sym.bit → St .Z = (encW done).reverse.map Sym.bit →
    St .A = cnt (Sym.bit true) a → St .R = [] →
    ∃ v' S', RunLe prog (4 * (encW q).length + (encW done).length + 2) ⟨some .nd, v, St⟩
      ⟨some (if a ∈ q then .no else .incC), v', S'⟩ ∧
      (a ∉ q → S' = update (update St .W ((encW (done ++ q)).map Sym.bit)) .Z [])

Uses 13 · Used by 1

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Witness encoding · The Hamiltonian path verifier machine · Stack alphabet of the SAT verifier · Runs within a step budget · Unary counter

Proof usesHAMPATH-verifier unary comparison with the counter restored · The witness encoding respects concatenation · Witness encoding of a nonempty list · One step of the emptiness test · Moving a stack of bits · Exact-length runs of a TM2 machine

Used byThe rest of a vertex step in the Hamiltonian-path verifier

DefinitionStack layout between vertex steps#✓fully proved

For an edge list \(es\), numbers \(s, t, n, c, b\) and a list \(q\) of vertices, the stacks of the verifier between two vertex steps: \(X\) holds the bits of the edge list \(es\), \(W\) holds the bits of the witness encoding of \(q\), the counters \(S\), \(T\), \(N\), \(C\) and \(B\) hold \(s\), \(t\), \(n\), \(c\) and \(b\) in unary, and the stacks \(A\), \(E\), \(Z\), \(R\) and \(Q\) are empty.

def lay (es : List (ℕ × ℕ)) (s t n c b : ℕ) (q : List ℕ) : K → List Sym
  | .X => (Karp.edgeBits es).map Sym.bit
  | .W => (encW q).map Sym.bit
  | .S => cnt (Sym.bit true) s
  | .T => cnt (Sym.bit true) t
  | .N => cnt (Sym.bit true) n
  | .C => cnt (Sym.bit true) c
  | .A => []
  | .B => cnt (Sym.bit true) b
  | .E => []
  | .Z => []
  | .R => []
  | .Q => []

Uses 5 · Used by 6

Statement usesStacks of the Hamiltonian path verifier · Witness encoding · Bit encoding of an edge list · Stack alphabet of the SAT verifier · Unary counter

Used byRunning the head-or-edge check · Running the vertex loop · Stack layout during a vertex step · Correctness and running time of the Hamiltonian path verifier · One vertex step of the Hamiltonian-path verifier · The rest of a vertex step in the Hamiltonian-path verifier

DefinitionStack layout during a vertex step#✓fully proved

For an edge list \(es\), numbers \(s, t, n, c, b, a\) and a list \(q\) of vertices, the stacks of the verifier during the step on vertex \(a\): the layout between vertex steps for \(es, s, t, n, c, b, q\), except that stack \(A\) holds \(a\) in unary.

def mid (es : List (ℕ × ℕ)) (s t n c b a : ℕ) (q : List ℕ) : K → List Sym :=
  update (lay es s t n c b q) .A (cnt (Sym.bit true) a)

Uses 4 · Used by 3

Statement usesStacks of the Hamiltonian path verifier · Stack layout between vertex steps · Stack alphabet of the SAT verifier · Unary counter

Used byRunning the head-or-edge check · One vertex step of the Hamiltonian-path verifier · The rest of a vertex step in the Hamiltonian-path verifier

TheoremRunning the head-or-edge check#✓fully proved

Let \(es\) be an edge list, \(s, t, n, c, b, a\) numbers and \(q\) a list of vertices, and say the check passes when \(a = s\) in case \(c = 0\), and \((b, a) \in es\) in case \(c \neq 0\). Started at the head-or-edge dispatch, in any internal state, on the stack layout during the step on vertex \(a\) for \(es, s, t, n, c, b, a, q\), the verifier reaches within \(3a + 4\ell + 7\) steps, where \(\ell\) is the number of bits of \(es\), the repeat scan if the check passes and the reject label otherwise, in some internal state and with some stacks; if the check passes, these stacks are the ones it started on.

theorem hd_run (es : List (ℕ × ℕ)) (s t n c b a : ℕ) (q : List ℕ) (v : Bool) :
    ∃ v' S', RunLe prog (3 * a + 4 * (Karp.edgeBits es).length + 7)
      ⟨some .hd, v, mid es s t n c b a q⟩
      ⟨some (if (if c = 0 then decide (a = s) else decide ((b, a) ∈ es)) = true then .nd
        else .no), v', S'⟩ ∧
      ((if c = 0 then decide (a = s) else decide ((b, a) ∈ es)) = true →
        S' = mid es s t n c b a q)

Uses 19 · Used by 1

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Stack layout during a vertex step · The Hamiltonian path verifier machine · Bit encoding of an edge list · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesCounter comparisons of the HAMPATH verifier · First counter of a HAMPATH-verifier comparison · Second counter of a HAMPATH-verifier comparison · Run of a HAMPATH-verifier counter comparison · Exit labels of the counter comparisons · Outcome of a HAMPATH-verifier equality comparison · Witness encoding · One step of the emptiness test · Stack layout between vertex steps · The edge scan of the Hamiltonian path verifier · Exact-length runs of a TM2 machine · Unary counter

Used byOne vertex step of the Hamiltonian-path verifier

TheoremThe rest of a vertex step in the Hamiltonian-path verifier#✓fully proved

Let \(es\) be an edge list, \(s, t, n, c, b, a\) natural numbers and \(q\) a list of natural numbers. Start the verifier, with any flag value, at the label \(\mathsf{nd}\) (the repeat scan) with its stacks in the mid-step layout: the between-steps layout for \(es\), \(s\), \(t\), \(n\), count \(c\), previous vertex \(b\) and remaining vertices \(q\), with \(a\) in unary on the stack \(A\). Let \(w\) be the unary encoding of \(q\). Then within at most \(4|w| + a + b + 6\) steps it reaches the label \(\mathsf{no}\) if \(a \in q\) and the label \(\mathsf{loop}\) if \(a \notin q\). In the second case (\(a\) has been counted and become the previous vertex) the stacks end in the between-steps layout for \(es\), \(s\), \(t\), \(n\), count \(c + 1\), previous vertex \(a\) and remaining vertices \(q\).

theorem tail_run (es : List (ℕ × ℕ)) (s t n c b a : ℕ) (q : List ℕ) (v : Bool) :
    ∃ v' S', RunLe prog (4 * (encW q).length + a + b + 6) ⟨some .nd, v, mid es s t n c b a q⟩
      ⟨some (if a ∈ q then .no else .loop), v', S'⟩ ∧
      (a ∉ q → S' = lay es s t n (c + 1) a q)

Uses 17 · Used by 1

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Witness encoding · Stack layout between vertex steps · Stack layout during a vertex step · The Hamiltonian path verifier machine · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesThe repeat scan of the Hamiltonian path verifier · Bit encoding of an edge list · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Adding units to target stacks · Unary counter · Counter increment · Running a counter transfer

Used byOne vertex step of the Hamiltonian-path verifier

TheoremOne vertex step of the Hamiltonian-path verifier#✓fully proved

Let \(es\) be an edge list, \(s, t, n, c, b, a\) natural numbers and \(q\) a list of natural numbers. Start the verifier, with any flag value, at the label \(\mathsf{rdA}\) (read the next vertex) with its stacks in the between-steps layout for \(es\), \(s\), \(t\), \(n\), count \(c\), previous vertex \(b\) and remaining vertices \(a, q\). Let \(e\) be the bit encoding of \(es\) and \(w\) the unary encoding of \(q\). Then within at most \(8a + b + 4|e| + 4|w| + 20\) steps it reaches the label \(\mathsf{loop}\) if the step check on \(a\) passes and the label \(\mathsf{no}\) otherwise. The step check passes when \(a < n\), \(a = s\) in case \(c = 0\) and \((b, a) \in es\) in case \(c \ne 0\), and \(a \notin q\). When it passes, the stacks end in the between-steps layout for \(es\), \(s\), \(t\), \(n\), count \(c + 1\), previous vertex \(a\) and remaining vertices \(q\).

theorem step_run (es : List (ℕ × ℕ)) (s t n c b a : ℕ) (q : List ℕ) (v : Bool) :
    ∃ v' S', RunLe prog (8 * a + b + 4 * (Karp.edgeBits es).length + 4 * (encW q).length + 20)
      ⟨some .rdA, v, lay es s t n c b (a :: q)⟩
      ⟨some (if stepOk s n es c b a q then .loop else .no), v', S'⟩ ∧
      (stepOk s n es c b a q = true → S' = lay es s t n (c + 1) a q)

Uses 22 · Used by 1

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Witness encoding · Stack layout between vertex steps · The Hamiltonian path verifier machine · One step of the HAMPATH walk · Bit encoding of an edge list · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesCounter comparisons of the HAMPATH verifier · First counter of a HAMPATH-verifier comparison · Second counter of a HAMPATH-verifier comparison · Run of a HAMPATH-verifier counter comparison · Exit labels of the counter comparisons · Outcome of the HAMPATH verifier's vertex-range comparison · Witness encoding of a nonempty list · Running the head-or-edge check · Stack layout during a vertex step · The unary reader of the Hamiltonian path verifier reads a terminated number · The rest of a vertex step in the Hamiltonian-path verifier · Exact-length runs of a TM2 machine · Unary counter

Used byRunning the vertex loop

TheoremRunning the vertex loop#✓fully proved

Let \(es\) be an edge list, \(s, t, n\) numbers and \(L\) a bound with \(n \le L\), \(t \le L\) and at most \(L\) bits in the encoding of \(es\). For every list \(q\) of vertices whose witness encoding has at most \(L\) bits, every count \(c\), every previous vertex \(b \le L\) and every internal state, the verifier started at the vertex loop on the stack layout between vertex steps for \(es, s, t, n, c, b, q\) reaches within \((|q| + 1)(20L + 20)\) steps, with some internal state and stacks, the accept label if the walk check for \(s, t, n, es, c, b, q\) passes and the reject label otherwise.

theorem loop_run (es : List (ℕ × ℕ)) (s t n L : ℕ) (hn : n ≤ L) (ht : t ≤ L)
    (he : (Karp.edgeBits es).length ≤ L) : ∀ (q : List ℕ) (c b : ℕ) (v : Bool),
    (encW q).length ≤ L → b ≤ L →
    ∃ v' S', RunLe prog ((q.length + 1) * (20 * L + 20)) ⟨some .loop, v, lay es s t n c b q⟩
      ⟨some (if walkOk s t n es c b q then .yes else .no), v', S'⟩

Uses 19 · Used by 1

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Witness encoding · Stack layout between vertex steps · The Hamiltonian path verifier machine · The walk check of the HAMPATH verifier · Bit encoding of an edge list · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesCounter comparisons of the HAMPATH verifier · Run of a HAMPATH-verifier counter comparison · Exit labels of the counter comparisons · Outcome of a HAMPATH-verifier equality comparison · Witness encoding of a nonempty list · One step of the emptiness test · One step of the HAMPATH walk · One vertex step of the Hamiltonian-path verifier · Exact-length runs of a TM2 machine · Unary counter

Used byCorrectness and running time of the Hamiltonian path verifier

TheoremCorrectness and running time of the Hamiltonian path verifier#✓fully proved

Let \(x\) and \(w\) be bit lists. Start the verifier at its start label, with either value of its Boolean variable, with \(x\) on stack \(\mathsf{X}\) and \(w\) on stack \(\mathsf{W}\) (as bit symbols, first bit on top) and all other stacks empty. Then within \(100(|x| + |w| + 1)^4\) steps it reaches the label \(\mathrm{yes}\) if the Hamiltonian path check accepts \(x\) and \(w\), and the label \(\mathrm{no}\) otherwise.

The machine in fact takes quadratically many steps; the theorem states only the quartic bound.

theorem run (x w : List Bool) (v : Bool) (St : ∀ _ : K, List Sym)
    (hX : St .X = x.map Sym.bit) (hW : St .W = w.map Sym.bit)
    (h0 : ∀ k, k ≠ .X → k ≠ .W → St k = []) :
    ∃ v' S', RunLe prog (100 * (x.length + w.length + 1) ^ 4) ⟨some start, v, St⟩
      ⟨some (if hamCheck x w then .yes else .no), v', S'⟩

Uses 33 · Used by 1

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · The HAMPATH verifier · The Hamiltonian path verifier machine · Start label of the Hamiltonian-path verifier · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesWitness decoder · Witness encoding · The witness decoder succeeds only on encodings · The verifier on an encoded instance and witness · Instances that do not decode are rejected · Witnesses that do not decode are rejected · The Hamiltonian path check · Stack layout between vertex steps · A witness is at least as long as its vertex list · Running the vertex loop · Moving a stack of bits · The unary reader of the Hamiltonian path verifier rejects an unterminated number · The unary reader of the Hamiltonian path verifier reads a terminated number · The edge-list check of the Hamiltonian-path verifier · The witness check of the Hamiltonian-path verifier · The walk check of the HAMPATH verifier · The machine's walk is the check · Decoding a graph · Edge-list decoder · Bit encoding of an edge list · The edge-list decoder succeeds only on edge bits · Decoding a PATH instance · Encoding of a PATH instance · Reading a unary length prefix · Exact-length runs of a TM2 machine · Unary counter

Used byHAMPATH is in NP

AbbreviationThe HAMPATH verifier as a host component#✓fully proved

The component machine whose program and labels are those of the HAMPATH verifier machine, whose stacks are the twelve stacks of that machine (the input \(X\), the witness \(W\), the counters \(S, T, N, C, A, B\), the save stacks \(E, Z\) and the scratch stacks \(R, Q\)), each over the symbol alphabet of the SAT verifier.

abbrev hamVerifyComp : Host.Comp where
  K := HamVerify.K
  Γ := fun _ => SatVerifier.Sym
  finΓ := fun _ => SatVerifier.Sym.instFintype
  L := HamVerify.Lab
  prog := HamVerify.prog
  ks := [.X, .W, .S, .T, .N, .C, .A, .B, .E, .Z, .R, .Q]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide

Uses 6 · Used by 1

Statement usesComponent machine · Counter comparisons of the HAMPATH verifier · Stacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · The Hamiltonian path verifier machine · Stack alphabet of the SAT verifier

Used byHAMPATH is in NP

TheoremHAMPATH is in NP#✓fully proved

HAMPATH is in NP.

theorem hamPathDec_mem_NP : hamPathDec ∈ NP

Uses 27 · Used by 1

Statement usesThe HAMPATH problem · Complexity classes · Decision problems · The complexity class NP

Proof usesComponent machine · Verifier host, canonical form · Counter comparisons of the HAMPATH verifier · Stacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · The HAMPATH verifier · HAMPATH is verified with quadratic-size witnesses · The Hamiltonian path verifier machine · Correctness and running time of the Hamiltonian path verifier · Start label of the Hamiltonian-path verifier · The HAMPATH verifier as a host component · Stack alphabet of the SAT verifier · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions · Exact-length runs of a TM2 machine · Runs within a step budget

Used byHAMPATH is NP-complete

AbbreviationThe HAMPATH emitter#✓fully proved

The emitter whose stacks, alphabets, labels, program and start label are those of the HAMPATH emitter machine, which exits at the machine's label \(\mathsf{done}\), reads the tokens of a CNF formula from stack \(T\) and writes its output bits on stack \(O\) (both symbol maps being the identity), and has step bound \(B(n) = 2000 (n + 1)^5\) for \(n\) tokens. Its output for a CNF formula \(\varphi\) is Sipser's HAMPATH instance of \(\varphi\), and for an undecodable input the fixed HAMPATH no-instance (two vertices, no arcs, source and target \(0\)).

Cslib.Complexity.Karp.emitHam · 21 lines

abbrev emitHam : Emitter where
  K := EmitHam.K
  Γ := EmitHam.Γ
  L := EmitHam.Lab
  prog := EmitHam.prog
  start := EmitHam.start
  done := .done
  start_ne_done := by decide
  prog_done := rfl
  cT := .T
  cO := .O
  cT_ne_cO := by decide
  iT := Equiv.refl _
  eO := Equiv.refl _
  g := toHam
  noOut := noHam
  B n := 2000 * (n + 1) ^ 5
  B_mono a b h := by dsimp only; gcongr
  run φ v St hT hO h0 := by
    obtain ⟨v', S', r, h⟩ := EmitHam.run φ [] v St (by simpa using hT) hO h0
    exact ⟨v', S', r, by simpa using h⟩

Uses 14 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Copy sites of the HAMPATH emitter · The HAMPATH emitter machine · Correctness and running time of the HAMPATH emitter · Start label of the HAMPATH emitter · Stack alphabets of the HAMPATH emitter · Emitter · A fixed HAMPATH no-instance · Sipser's HAMPATH instance of a CNF formula · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · Runs within a step budget

Used bySAT ≤ HAMPATH is polynomial-time

TheoremSAT ≤ HAMPATH is polynomial-time#✓fully proved

The map on bit strings that sends a bit string decoding to a CNF formula \(\varphi\) to Sipser's HAMPATH instance for \(\varphi\), and every other bit string to the fixed no-instance with two vertices, no arcs and \(s = t = 0\), is computable in polynomial time.

theorem isPolyTime_reduceHam : IsPolyTime reduceHam

Uses 25 · Used by 1

Statement usesThe SAT-to-HAMPATH reduction map · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions

Proof usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Copy sites of the HAMPATH emitter · Copy sites of the HAMPATH emitter, listed · The four pairs of Booleans · Stack alphabets of the HAMPATH emitter · Emitter · Emitter reductions out of SAT are polynomial-time · Output of an emitter on a bit string · The HAMPATH emitter · A fixed HAMPATH no-instance · Sipser's HAMPATH instance of a CNF formula · Stack alphabet of the SAT verifier · Decoding a complete length-prefixed CNF formula · CNF formula

Used byHAMPATH is NP-hard

TheoremHAMPATH is NP-hard#✓fully proved

Every decision problem \(L\) in NP has a polynomial-time many-one reduction to HAMPATH: a polynomial-time computable map \(f\) on bit strings such that, for every bit string \(x\), \(L\) accepts \(x\) exactly when HAMPATH accepts \(f(x)\).

theorem hamPathDec_npHard : ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L hamPathDec

Uses 20 · Used by 1

Statement usesThe HAMPATH problem · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP

Proof usesEvery NP problem reduces to binary-index CNF-SAT · SAT ≤ HAMPATH is polynomial-time · NP-hardness transfers along reductions · The SAT-to-HAMPATH reduction map · SAT ≤ HAMPATH preserves membership · SAT as a decision problem · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions

Used byHAMPATH is NP-complete

TheoremHAMPATH is NP-complete#✓fully proved

HAMPATH lies in NP, and every decision problem \(L\) in NP has a polynomial-time many-one reduction to HAMPATH: a polynomial-time computable map \(f\) on bit strings such that, for every bit string \(x\), \(L\) accepts \(x\) exactly when HAMPATH accepts \(f(x)\).

theorem hamPathDec_npComplete :
    hamPathDec ∈ NP ∧ ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L hamPathDec

Sources

• Sipser, Theorem 7.46.

Uses 7

Statement usesThe HAMPATH problem · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP

Proof usesHAMPATH is in NP · HAMPATH is NP-hard

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.