Graph 3-coloring

Bit-string encoding of a graph to Decoding fails on a dangling half-pair

• Bit-string encoding of a graph
• Graph of an edge list
• 3-COLOR
• State of the SAT-to-3-COLOR construction
• Consistency edges between two occurrences of a variable
• Adding a literal occurrence in the 3-COLOR construction
• OR gadget of the 3-COLOR construction
• Processing the remaining literals of a clause
• Processing one clause in the 3-COLOR construction
• The SAT-to-3-COLOR graph construction
• The 3-COLOR instance of a CNF formula
• The complete graph on four vertices as a bit string
• The SAT to 3-COLOR reduction map on bit strings
• Reading a unary number shortens the input
• Edge-list decoder
• Decoding a graph
• Bit encoding of an edge list
• Decoding the empty input
• The edge-list decoder fails on a cut-off first number
• Decoding fails on a dangling half-pair

Decoding one pair, then the rest to Correctness of the reduction from SAT to 3-coloring

• Decoding one pair, then the rest
• Decoding the bits of an edge list
• The edge-list decoder succeeds only on edge bits
• Graph encoding as vertex count plus edge bits
• Graph decoding inverts graph encoding
• Graph decoding succeeds only on encodings
• The complete graph on four vertices is not 3-colorable
• Proper 3-colorings of an edge list
• 3-colorability through colorings of the natural numbers
• Coloring an OR gadget
• Soundness of the OR gadget
• Adding a literal occurrence takes two new vertices
• Growth of construction states
• Extending a state makes it grow
• Well-formed construction states
• Extending a well-formed state keeps it well formed
• The construction's edges lie below its vertex count
• Colorings that follow an assignment
• Output of the OR gadget under a proper 3-coloring
• Correctness of the reduction from SAT to 3-coloring

Correctness of the SAT to 3-COLOR map on bit strings to Quiescent states of the 3-COLOR emitter

• Correctness of the SAT to 3-COLOR map on bit strings
• Bit encoding of an edge
• Bits pushed for a list of edges
• Stacks of the 3-coloring emitter
• Stack alphabets of the 3-coloring emitter
• Counters read by copy sites of the 3-COLOR emitter
• Stack of a counter
• Unit symbol of a counter
• Copy sites of the 3-COLOR emitter
• The copy sites of the 3-COLOR emitter, listed
• Counter copied by a copy site
• Constant block of a copy site
• Control labels of the 3-coloring emitter
• Successor label of a copy site
• Literal-marker test
• Reading unary units
• Bits of the palette triangle
• The 3-COLOR emitter machine
• Start label of the 3-coloring emitter
• Quiescent states of the 3-COLOR emitter

Stacks of a quiescent state to Adding the vertex counter to the OR output

• Stacks of a quiescent state
• Counter values of a quiescent state
• Counters are not held on the output stack
• Copying a counter through \(W\)
• Bit list of a copy site of the 3-COLOR emitter
• Running a copy site of the 3-COLOR emitter
• Copy sites of the 3-COLOR emitter running in sequence
• Bits pushed by a sequence of copy sites of the 3-COLOR emitter
• Running a sequence of copy sites of the 3-COLOR emitter
• Walk tokens
• Name of a variable
• Encoding of an earlier occurrence on stack \(D\)
• Moving the current name from \(T\) to \(A\)
• Name comparison in the 3-COLOR emitter
• Moving an earlier name from \(D\) to \(E\)
• Skipping an earlier literal vertex
• Moving an earlier literal vertex from \(D\) to \(U\)
• Moving \(U\) onto \(E\)
• The 3-COLOR emitter clears its OR-output counter
• Adding the vertex counter to the OR output

3-COLOR emitter: moving the walk side back to The emitter on a list of clauses

• 3-COLOR emitter: moving the walk side back
• Recording the current occurrence
• Copy sites of the occurrence triangle
• Copy sites of the consistency edges
• The OR-gadget copy sites
• Copy sites of the clause end
• Copy sites of the empty clause
• Consistency edges of two occurrences of the same variable
• One step of the walk over earlier occurrences
• Walking the earlier occurrences
• Emitting one literal occurrence
• Size invariant of the 3-coloring emitter
• One more token preserves the 3-COLOR emitter's size invariant
• The size invariant survives a new literal occurrence
• Per-token step budget of the 3-COLOR emitter
• The emitter state of a construction state
• Step budget for one literal
• The emitter processes the remaining literals of a clause
• The 3-COLOR emitter processes one clause
• The emitter on a list of clauses

Correctness and step bound of the 3-COLOR emitter to Witness colors of the first \(n\) vertices

• Correctness and step bound of the 3-COLOR emitter
• Color code of a vertex in a witness
• Valid color code
• The 3-COLOR verifier
• Acceptance condition of the 3-COLOR verifier
• Two-bit code of a color
• Decoding a color code
• Decoding a color code recovers the color
• Color codes are valid
• Re-encoding a decoded valid color
• Flattening pairs of bits
• Flattening the empty list
• Flattening a nonempty list
• Flattening a concatenation
• Length of a flattening
• Color codes of flattened pairs
• Color codes of a flattened coloring
• 3-colorability by witness bits
• 3-COLOR is verified by the witness check
• Witness colors of the first \(n\) vertices

Edge verdict to Interleaved updates of two stacks of the 3-COLOR verifier

• Edge verdict
• Edge-loop verdict
• Number of witness colors
• Reading a witness color
• Peeling a vertex off the witness colors
• The 3-COLOR verifier as an edge loop
• Shifting the edge verdict past the first color
• Stacks of the 3-COLOR verifier
• Labels of the 3-COLOR verifier
• Statements of the 3-COLOR verifier
• Unary reader of the 3-COLOR verifier
• Load step of the 3-COLOR verifier
• Edge-loop start of the 3-COLOR verifier
• Moving one color code in the 3-COLOR verifier
• One step of the joint walk of the 3-COLOR verifier
• One step of the walk towards the farther endpoint
• The 3-COLOR verifier machine
• Start label of the 3-coloring verifier
• One step of the 3-COLOR verifier
• Interleaved updates of two stacks of the 3-COLOR verifier

Moving one color code from the color stack to The 3-COLOR verifier as a host component

• Moving one color code from the color stack
• The color-moving block rejects on an empty color stack
• Walk-on step with the counter exhausted
• Walk-on step with a unit on the counter
• The walk towards the farther endpoint decides the edge
• Joint-walk step with both counters nonempty
• Joint-walk step when the second endpoint counter runs out first
• Joint-walk step when the first endpoint counter runs out first
• Joint-walk step with both counters exhausted
• Edge verdict for an edge starting at vertex 0
• Edge verdict for an edge ending at vertex 0
• The joint walk of the 3-COLOR verifier decides one edge
• The unary reader on a terminated number
• The unary reader rejects an unterminated number
• Run of the load phase of the 3-COLOR verifier
• Edge-loop verdict after one parsed edge
• Restoring the color stack in the 3-COLOR verifier
• Correctness and running time of the edge loop
• Correctness and time bound of the 3-coloring verifier machine
• The 3-COLOR verifier as a host component

3-COLOR is in NP to 3-COLOR is NP-complete

• 3-COLOR is in NP
• The 3-COLOR emitter
• The SAT-to-3-COLOR reduction is polynomial-time
• 3-COLOR is NP-hard
• 3-COLOR is NP-complete

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.