Hamiltonian path in directed graphs

Hamiltonian paths to Witness encoding of a nonempty list

• Hamiltonian paths
• The HAMPATH problem
• Distinct variables of a formula
• Tops of the diamonds
• Row vertices of a diamond
• Arcs of a variable diamond
• Arcs of the HAMPATH construction
• Sipser's HAMPATH instance of a CNF formula
• A fixed HAMPATH no-instance
• The SAT-to-HAMPATH reduction map
• Normal clause detours
• Tops are monotone in the diamond index
• Row vertices lie below the next top
• Bits of an edge list, first edge first
• Edge bits of the empty edge list
• Bits of concatenated edge lists
• Witness encoding
• Witness decoder
• Witness encoding of the empty list
• Witness encoding of a nonempty list

The witness encoding respects concatenation to Length of an encoded PATH instance

• The witness encoding respects concatenation
• Decoding the empty witness
• Witness decoding fails on a cut-off first number
• Decoding peels off the first number
• Decoding inverts the witness encoding
• The witness decoder succeeds only on encodings
• The witness codec
• Witness length
• Witness length bound
• A witness is at least as long as its vertex list
• Arc check of a vertex list
• Checking a vertex list against the arcs
• The Hamiltonian path check
• The Hamiltonian path check is correct
• The HAMPATH verifier
• What the HAMPATH verifier accepts
• The verifier on an encoded instance and witness
• Instances that do not decode are rejected
• Witnesses that do not decode are rejected
• Length of an encoded PATH instance

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

• HAMPATH is verified with quadratic-size witnesses
• One step of the HAMPATH walk
• The walk check of the HAMPATH verifier
• The walk check after the first vertex
• The machine's walk is the check
• Tops of distinct diamonds are at least \(3m + 2\) apart
• Arcs of the Hamiltonian path construction
• Classification of the arcs of Sipser's graph
• In-neighbours of a row 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
• Out-neighbours of a clause vertex in Sipser's graph
• A Hamiltonian path visits every vertex
• Consecutive vertices of a Hamiltonian path of Sipser's graph form arcs
• 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
• A clause detour returns to its own pair (Sipser's separator argument)
• Hamiltonian paths of Sipser's graph have normal detours
• The HAMPATH instance as unary blocks and arc bits
• The frame of a diamond

The row arcs of a diamond to Label after a HAMPATH copy site

• The row arcs of a diamond
• Clause detours in a diamond
• The next diamond top follows the row
• Splitting off the middle clause of a concatenation
• Insert a variable if new
• Removing duplicates by insertion
• Consecutive row vertices
• Length bound for the bit encoding of an edge list
• Stacks of the HAMPATH emitter
• Stack alphabets of the HAMPATH emitter
• Counters read by HAMPATH copy sites
• Stack of a HAMPATH copy-site counter
• Unit symbol of an emitter counter
• Copy sites of the HAMPATH emitter
• Copy sites of the HAMPATH emitter, listed
• Counter read by a copy site
• Extra ones of a copy site
• Labels of the HAMPATH emitter
• The four pairs of Booleans
• Label after a HAMPATH copy site

End of a clause in the detour walk to HAMPATH emitter, phase A: copying a reversed name onto two stacks

• End of a clause in the detour walk
• The HAMPATH emitter machine
• Start label of the HAMPATH emitter
• Quiescent states of the HAMPATH emitter
• Stacks of a quiescent emitter state
• Counter values of a quiescent emitter state
• Copying a counter in the HAMPATH emitter
• Bits pushed by a copy site of the HAMPATH emitter
• Run of a HAMPATH copy site
• Copy sites chained in the HAMPATH emitter
• Step count of a list of copy sites in the HAMPATH emitter
• Running a chain of copy sites in the HAMPATH emitter
• A symbol that reads as a name bit is that bit
• Comparing a name with the top entry of the variable stack
• Name of a variable in the HAMPATH emitter
• Variable stack of the HAMPATH emitter
• Variable-stack symbols of the HAMPATH emitter
• HAMPATH emitter, phase A: moving the walk stack back onto the variable stack
• HAMPATH emitter, phase A: searching the variable stack for a name
• HAMPATH emitter, phase A: copying a reversed name onto two stacks

HAMPATH emitter, phase A: one literal to Moving the tokens back in the HAMPATH emitter

• HAMPATH emitter, phase A: one literal
• HAMPATH emitter, phase A: the literals of a clause
• HAMPATH emitter, phase A: one clause
• HAMPATH emitter, phase A: the clauses of a formula
• Initial state of the HAMPATH emitter
• The emitter state before the diamonds
• Phase A of the HAMPATH emitter
• Token symbols of the HAMPATH emitter
• The tokens of a literal do not start with a clause end
• One literal of the detour walk
• The literals of a clause in the detour walk
• One clause of the detour walk
• The detour walk of a diamond in the HAMPATH emitter
• Frame copy sites of the HAMPATH emitter
• Row copy sites of the HAMPATH emitter
• Front of a diamond
• The row loop of a diamond in the HAMPATH emitter
• Adding units along no stacks
• Draining a counter
• Moving the tokens back in the HAMPATH emitter

The row of a diamond in the HAMPATH emitter to A row starts at its left end

• The row of a diamond in the HAMPATH emitter
• The detours of a diamond
• End of a diamond
• One diamond
• The diamonds
• The output phase of the HAMPATH emitter
• Correctness and running time of the HAMPATH emitter
• The row of a diamond with its clauses inserted
• Clauses picked up by a diamond
• The visit of a diamond
• The forward path through the diamonds
• Clause vertices picked up by a row
• The clause vertices of a row are distinct
• Each clause is picked up by exactly one row
• The vertices of a diamond row
• A diamond visit is a block of consecutive vertices plus its clauses
• The first \(t\) diamonds occupy consecutive vertices
• The forward path visits every vertex once
• Chain condition for a diamond row
• A row starts at its left end

A row ends at its right end to Consecutive vertices of the contracted path are joined by arcs

• A row ends at its right end
• Chain condition for a diamond traversal
• Chain condition for the forward path
• The forward path starts at the first top
• The forward path ends at the last top
• Diamond arcs are arcs of the construction
• The frame arcs of a diamond
• Row arcs of a diamond
• Positive detour arcs of a diamond
• The detour arcs of a negative occurrence
• A satisfying choice gives a Hamiltonian path
• Satisfiable formulas give Hamiltonian paths (SAT ≤ HAMPATH, forward direction)
• Out-neighbours of a top
• Arcs from a row into a clause vertex
• Row vertices counted from either end
• Out-neighbours of a row vertex outside the clause vertices
• In-neighbours of a row vertex outside the clause vertices
• Deleting the clause vertices from a path
• Contracting a clause detour
• Consecutive vertices of the contracted path are joined by arcs

Every vertex of the contracted path except its end has a successor to Second counter of a HAMPATH-verifier comparison

• Every vertex of the contracted path except its end has a successor
• Entering a row and leaving it at once is impossible
• A row entered at one end is run to the other end
• Every top but the last is followed by an end of its row
• Positions in the list of distinct variables
• Backward direction of SAT ≤ HAMPATH for paths with normal detours
• The construction has a Hamiltonian path iff the formula is satisfiable
• HAMPATH on an encoded instance
• HAMPATH rejects the fixed no-instance
• SAT ≤ HAMPATH preserves membership
• Stacks of the Hamiltonian path verifier
• Counter comparisons of the HAMPATH verifier
• Labels of the Hamiltonian path verifier
• Statements of the Hamiltonian-path verifier
• The unary reader of the Hamiltonian path verifier
• The unary mover of the Hamiltonian path verifier
• Emptiness test
• Step of the HAMPATH verifier's unary comparison loop
• First counter of a HAMPATH-verifier comparison
• Second counter of a HAMPATH-verifier comparison

Exit labels of the counter comparisons to The edge scan of the Hamiltonian path verifier

• Exit labels of the counter comparisons
• The Hamiltonian path verifier machine
• Start label of the Hamiltonian-path verifier
• Interleaved stack updates in the Hamiltonian-path verifier
• A single step of the Hamiltonian-path verifier
• One step of the emptiness test
• The unary reader of the Hamiltonian path verifier reads a terminated number
• The unary reader of the Hamiltonian path verifier rejects an unterminated number
• Extending a reversed unary block
• The unary mover of the Hamiltonian path verifier moves a terminated number
• The unary mover of the Hamiltonian path verifier rejects an unterminated number
• Moving a stack of bits
• Run of a HAMPATH-verifier counter comparison
• Outcome of the HAMPATH verifier's vertex-range comparison
• Outcome of a HAMPATH-verifier equality comparison
• Run of the HAMPATH verifier's unary comparison loop
• HAMPATH-verifier unary comparison with the counter restored
• The edge-list check of the Hamiltonian-path verifier
• The witness check of the Hamiltonian-path verifier
• The edge scan of the Hamiltonian path verifier

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

• The repeat scan of the Hamiltonian path verifier
• Stack layout between vertex steps
• Stack layout during a vertex step
• Running the head-or-edge check
• The rest of a vertex step in the Hamiltonian-path verifier
• One vertex step of the Hamiltonian-path verifier
• Running the vertex loop
• Correctness and running time of the Hamiltonian path verifier
• The HAMPATH verifier as a host component
• HAMPATH is in NP
• The HAMPATH emitter
• SAT ≤ HAMPATH is polynomial-time
• HAMPATH is NP-hard
• HAMPATH is NP-complete

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.