arXiv CSopen access

Color Complexity of Recolorable Graph Exploration: Upper and Lower Bounds via Block Structure

Color Complexity of Recolorable Graph Exploration: Upper and Lower Bounds via Block Structure Shoma Hiraoka∗

Shunsuke Imori∗

Shota Takahashi†

Yuichi Sudo†

arXiv:2609.14356v1 [cs.DC] 13 Sep 2026

Abstract We study exploration of anonymous, port-free graphs by a single agent with no internal memory. To compensate for the lack of memory, the agent uses writable vertex colors as external memory. At each step, the agent observes its current color and the multiset of neighbor colors, recolors the current vertex, and requests a destination color. If several neighbors have that color, an adversary chooses the destination. From every starting vertex, the agent must visit all vertices, return to its start, and terminate there. Throughout, recoloring is unrestricted, and the color count includes the common initial color. Under this convention, previous work gave a six-color algorithm for general graphs and five-color algorithms for triangle-free graphs and for φ-free graphs, a class that contains all cacti. However, to our knowledge, no nontrivial color lower bound was known for unrestricted recoloring. We determine the optimal number of colors on two classes defined by block structure and prove the first nontrivial color lower bounds for unrestricted recoloring. First, a single three-color algorithm explores every tree and every simple cycle in O(n) moves, and no algorithm with at most two colors explores P3 , the path on three vertices. Second, we give a four-color algorithm that explores every graph whose blocks are cycles or complete bipartite graphs in O(n) moves, and we prove that no algorithm with at most three colors explores all subcubic pseudotrees. Hence four colors are optimal for every class between subcubic pseudotrees and this block-defined class. On cacti, this improves the previous five-color upper bound to a tight four. The lower bound reduces the possible initial actions by hand and rules out the remaining cases by a machine-checked SAT certificate on nine graphs with at most five vertices. Independent checkers verify the graph encodings, the hand reduction, and every imported trace and domain clause, and a DRAT checker verifies the refutation. Finally, we extend the known five-color algorithm for triangle-free graphs to graphs whose blocks are cliques or triangle-free, using O(n∆) moves, where ∆ is the maximum degree. The extension uses two conditions that let the semi-DFS cleanup restore temporary marks and return to the correct path endpoint against every adversarial choice. We prove that this class is exactly the class of graphs on which both conditions hold in every reachable state.

2012 ACM Subject Classification: Theory of computation → Distributed algorithms; Mathematics of computing → Graph theory Keywords: graph exploration, oblivious agent, vertex recoloring, semi-DFS, cactus graphs, computer-assisted proof

1

Introduction

Graph exploration asks a single mobile agent to visit every vertex of an initially unknown connected graph and has been studied under many models and objectives [1, 4, 5, 6, 10, 11, 14, 16, 17, 18, 22, 23, 24, 28]. Formulations differ in whether the agent must only visit every vertex, ∗ †

The University of Osaka Hosei University

1

also return to its start, additionally detect completion and stop, or instead visit every vertex infinitely often. Related tasks on anonymous networks, such as dispersion, gathering, uniform deployment, and black-hole search, pursue different objectives [2, 7, 8, 9, 12, 13, 15, 19, 20, 21, 25]. In this paper, we study exploration with return and termination. From every starting vertex, the agent must visit all vertices, return to its start, and terminate there. Whether this objective is achievable depends on the resources available to the agent. Most exploration models rely on port numbers and internal memory, sometimes augmented with vertex identifiers, pebbles, or preprocessed labels [5, 6, 10, 16, 18]. Böckenhauer, Frei, Unger, and Wehner [3] ask how far exploration is possible without these standard resources, replacing them with writable vertex colors. At each step, the agent observes the color of its current vertex and those of its neighbors, may recolor the current vertex, and either selects a destination color or terminates. Unless the agent terminates, the adversary chooses a neighbor of the selected color and moves the agent there. We call this setting the BFUW model. The central question in the BFUW model is how many colors suffice for exploration. Throughout, recoloring is unrestricted, and every color count includes the common initial color.1 When each vertex may be recolored at most once, Böckenhauer et al. prove that exactly n colors are required on general n-vertex graphs and exactly four on trees. These bounds concern the once-recolorable variant. With unrestricted recoloring, they give an eight-color algorithm for general graphs that processes breadth-first layers in order, storing the layer index modulo a constant in the vertex colors. Takahashi et al. [26] instead introduce semi-DFS, a DFS variant that adds an unvisited neighbor of the current path endpoint only if that vertex is adjacent to no other vertex on the path. Their implementation uses six colors on general graphs and five colors on triangle-free graphs. Their separate five-color algorithm for φ-free graphs colors vertices according to distance modulo a constant, as does the eight-color algorithm. A graph is φ-free if, for every vertex v of degree at least four, each component of G − v contains at most two neighbors of v. This class contains every subcubic graph (i.e., a graph with maximum degree at most three) and every cactus.

1.1

Our contribution

We give upper and lower bounds on the number of colors required to explore several graph classes in the BFUW model with unrestricted recoloring. Each upper bound below is achieved by a single algorithm that explores every graph in the corresponding class. The color count includes the common initial color. Three colors. We give a single three-color algorithm that explores every tree and every simple cycle in O(n) moves. We also prove that no algorithm with at most two colors explores P3 , the path on three vertices. Thus the optimal number of colors for the class consisting of all trees and all simple cycles is three. Four colors. A block is a maximal biconnected subgraph or a bridge. We write GCB for the class of graphs whose blocks are cycles or complete bipartite graphs. We give a four-color algorithm that explores every graph in this class in O(n) moves. We also give a computer-assisted proof that at least four colors are required for a single algorithm to explore every subcubic pseudotree. Here, a graph is subcubic if its maximum degree is at most three. A pseudotree is a connected graph with at most one cycle. This lower bound implies that the optimal number of colors is four for every graph class that contains all subcubic pseudotrees and is contained in GCB because GCB contains all subcubic pseudotrees. In particular, we improve the previous five-color upper bound for cacti to four and prove its optimality. Five colors. We write GKTF for the class of graphs whose blocks are cliques or triangle-free. 1 Böckenhauer et al. [3] do not count the initial color, but Takahashi, Kanaya, Hiraoka, Eguchi, and Sudo [26] do. We follow Takahashi et al. and add one color when stating the bounds of Böckenhauer et al.

2

We extend the five-color algorithm of Takahashi et al. [26] for triangle-free graphs to explore every graph in GKTF with five colors in O(n∆) moves. Here, ∆ denotes the maximum degree. The class GKTF and the class of φ-free graphs covered by a separate known five-color algorithm are incomparable. A graph is unichord-free if no cycle has exactly one chord [27]. Every unichord-free graph belongs to GKTF , so we also obtain a five-color upper bound for this class. Our lower bounds are the first nontrivial color lower bounds for unrestricted recoloring. Together with the known six-color algorithm for general graphs, they place the optimal number of colors for general graphs between four and six. It remains open to prove our four-color lower bound without computer assistance. Figure 1 summarizes the class inclusions, and Table 1 summarizes the upper and lower color bounds. trees ∆≤2

subcubic pseudotrees

pseudotrees

cacti

GCB

∆≤3

φ-free

incomparabl

GKTF e

triangle-free

Figure 1: Relations among the graph classes used in this paper. Solid arrows denote proper inclusions, the dashed line denotes incomparability, and ∆ denotes maximum degree.

Table 1: Color bounds including the initial color, for a single algorithm per class. Lower bounds of four follow from Theorem 13 by class containment.

1.2

Graph class

Lower bound

Upper bound

Trees and simple cycles Cacti GCB GKTF φ-free Arbitrary graphs

3 (Lem. 4) 4 (Thm. 13) 4 (Thm. 13) 4 (Thm. 13) 4 (Thm. 13) 4 (Thm. 13)

3 (Thm. 3) 4 (Thm. 6) 4 (Thm. 6) 5 (Thm. 11) 5 [26] 6 [26]

Further Related Work

Other exploration models provide different resources for navigation. Aleliunas, Karp, Lipton, Lovász, and Rackoff [1] show that a random walk covers every finite connected graph with probability one and introduce universal traversal sequences for portnumbered graphs. Koucký [11] introduced exploration sequences with backtracking, and Reingold [18] constructed universal exploration sequences in logarithmic space. Neither approach gives deterministic exploration with return and termination without port numbers. Deterministic exploration becomes possible with other forms of local information. Cohen, Fraigniaud, Ilcinkas, Korman, and Peleg [5] show that three-valued preprocessing labels let a finite automaton explore every graph. Disser, Hackfeld, and Klimm [6] prove that Θ(log log n) distinguishable pebbles, or the same number of constant-memory agents, are both necessary and sufficient to explore arbitrary port-numbered graphs. Bojko, Gotfryd, Kowalski, and Pająk [4] study trees with hidden incoming edges and bound the trade-offs among agent memory, pervertex bits, and time. Several works instead place persistent state directly at vertices. Sudo, Baba, Nakamura, Ooshita, Kakugawa, and Masuzawa [23] study exploration with vertex whiteboards. Priezzhev, Dhar, Dhar, and Krishnamurthy [17] introduced Eulerian walkers, which maintain a cyclic pointer at each vertex, Yanovski, Wagner, and Bruckstein [28] apply them to perpetual patrolling, and Menc, Pająk, and Uznański [14] bound the time and space of rotor-router explo3

ration. Inoue, Kitamura, Izumi, and Masuzawa [10] instead study an agent with no persistent internal state (an oblivious agent) that can update persistent states at vertices. Sudo, Ooshita, and Kamei [24] study self-stabilizing exploration from arbitrary agent and vertex states, where the objective is to visit every vertex infinitely often. For cacti with distinguishable cycles, Shimoyama, Sudo, Kakugawa, and Masuzawa [22] give an algorithm that visits every vertex infinitely often.

2

Model and Preliminaries

Throughout, G = (V, E) is a finite simple connected undirected graph with n = |V | and maximum degree ∆. We write N (v) = {u ∈ V : {u, v} ∈ E} for the neighborhood of a vertex v. A single agent moves on G, whose vertices have colors from a finite set C. Initially, the agent is at an arbitrary start s, and every vertex has the initial color c0 ∈ C. The agent retains no internal state between actions and is therefore called oblivious. At each step, the agent observes only the color c of its current vertex and the multiset M of neighbor colors, including their multiplicities. We write this observation as (c; M ). The agent chooses a new current color and an action from this observation. The action is a move to a neighbor of a specified color, stay to remain at the current vertex, or stop to terminate. A deterministic rule function ξ : C × M(C) → C × (C ∪ {stay, stop}) specifies these choices, where M(C) denotes the finite multisets over C. If ξ(c, M ) = (c′ , d), the agent recolors its current vertex with c′ and then performs action d. This is one rule application. If d ∈ C, an adversary chooses a neighbor of color d as the destination. At each step, the adversary sees all vertex colors and the agent position. If no neighbor of color d exists, this absent-color request ends the process. Since the graph has no self-loops, recoloring the current vertex does not change the neighborhood-color multiset M . Recoloring is unrestricted, so a vertex may be recolored any number of times and may return from a noninitial color to c0 . An exploration algorithm is specified by A = (C, c0 , ξ). The rule function is not given n, ∆, a round counter, a distinguished start marker, vertex identifiers, the previous vertex, or incoming ports. A configuration q = (v, ψ) records the agent position v and vertex coloring ψ : V → C immediately before a rule application. The observation in this configuration is (ψ(v); M (v)), where M (v) = {{ψ(u) : u ∈ N (v)}}. After a move or stay, the next configuration records the resulting coloring and position. An execution is a finite or infinite sequence of configurations obtained in this way from the initial configuration at s. No configuration is recorded after a stop or an absent-color request. An execution is maximal if it is infinite or ends by issuing stop or requesting an absent color. Under the exploration objective of Böckenhauer et al. [3], a maximal execution from s succeeds if it visits every vertex and issues stop at s. A maximal execution fails if it runs forever, requests an absent color, or issues stop before visiting every vertex or at a vertex other than s. An algorithm explores G if, for every start s and every sequence of adversarial choices, the resulting maximal execution succeeds. For a fixed algorithm and graph, a configuration or observation is reachable if it occurs in an execution from some starting vertex. The number of colors is |C|, including the initial color c0 . The color complexity of a graph class is the minimum |C| for which a single algorithm with color set C explores every graph in the class. An algorithm with fewer than k colors can be extended to a color set of size k by leaving the additional colors unused. Running-time bounds count rule applications, including stay actions. For a path P = (u1 , . . . , uk ), we write V (P ) = {u1 , . . . , uk } for its vertex set. A path is induced if no two nonconsecutive vertices on the path are adjacent. A vertex v is a cut vertex of a graph H if H − v has more connected components than H. A block of G is a maximal connected subgraph with at least two vertices and no cut vertex. Equivalently, a block is a 4

maximal biconnected subgraph or a bridge on its two endpoints. Every edge belongs to exactly one block, every cycle lies in one block, and the cut vertices of G are exactly the vertices in at least two blocks. For pairwise distinct colors c1 , . . . , cm , we write c1 , . . . , cm ∈ M if each ci occurs in M and c1 , . . . , cm ∈ / M if none occurs. Lemma 1. A graph family is explorable with a given color set if and only if it is explorable by a rule that never uses stay at a reachable observation. Proof. During consecutive stay actions, the agent position and neighborhood multiset M remain fixed. The starting observation (c; M ) determines the sequence, which must end with a move or stop because the rule succeeds. Replace each reachable such sequence by its final recoloring and move or stop, retaining every other output. The resulting executions are exactly the original executions with their stay steps deleted. The converse holds because a rule that never stays is allowed by the original model. Lemma 2. If two executions of the same rule on the same graph, started at distinct vertices, reach the same configuration before their next rule application, then some starting vertex and sequence of adversarial choices yield a failing maximal execution of the rule. Proof. After the executions reach the same configuration, the adversary can choose the same destinations, so determinism keeps all later configurations identical. An infinite continuation or an absent-color request makes both executions fail. Otherwise they stop at the same vertex, which cannot be both distinct starts.

3

Three Colors

In this section, we present the three-color algorithm ATC3 (Algorithm 1) for trees and simple cycles and show that two colors do not suffice for P3 , the path on three vertices.

3.1

Trees and simple cycles

On a tree rooted at the start, an entry into an all-init child subtree from a ℓ0 parent returns with the subtree colored ℓ1 . On a simple cycle, the first move fixes a direction. The agent colors the forward route ℓ0 , reverses direction, and colors the return route ℓ1 before stopping at the start. Outputs omitted from a rule table may be assigned arbitrarily; each correctness proof shows that the corresponding observations are unreachable. Theorem 3. Algorithm 1 explores every tree and every simple cycle using three colors and O(n) moves. Proof. Case 1 (tree). We root the tree at the start s. If s is isolated, Rule D1 stops immediately. Otherwise Rule D2 recolors s to ℓ0 and moves to an adversarially chosen neighbor. For each nonroot vertex v with parent p, let Tv denote the subtree rooted at v. We prove the following claim by induction on its height. The induction claim assumes that the agent is at v, the parent p is in ℓ0 , and all of Tv is in init. From this configuration, the agent visits every vertex of Tv , colors them all with ℓ1 , and returns to p, whose color remains ℓ0 . Except for the final move to p, the agent stays inside Tv . If v is a leaf, Rule D6 does exactly this. We next assume that v is not a leaf. Rule D3 recolors v to ℓ1 and enters an adversarially chosen init-colored child x. If x is a leaf, the agent sees only the ℓ1 -colored vertex v there, so Rule D5 recolors x with ℓ1 and returns to v. Otherwise the agent sees both init and ℓ1 , so Rule D4 returns immediately to v and leaves every vertex of Tx colored init. Hence the agent is back at v, and every child subtree is either entirely init or entirely ℓ1 .

5

Algorithm 1: Three-Color Exploration of Trees and Simple Cycles ATC3 Colors: CTC3 = {init, ℓ0 , ℓ1 } and c0 = init Rule Function:   /M (Rule D1) (ℓ1 , stop) if init, ℓ0 , ℓ1 ∈     (ℓ0 , init) else if init ∈ M ∧ ℓ0 , ℓ1 ∈ / M (Rule D2)    (ℓ , init) else if init, ℓ ∈ M (Rule D3) 1 0 ξTC3 (init, M ) =  (init, ℓ1 ) else if init, ℓ1 ∈ M (Rule D4)      (ℓ1 , ℓ1 ) else if ℓ1 ∈ M (Rule D5)    (ℓ , ℓ ) else if ℓ0 ∈ M (Rule D6) 1 0   (Rule D7) (ℓ0 , init) if init, ℓ1 ∈ M ξTC3 (ℓ0 , M ) = (ℓ1 , ℓ0 ) else if ℓ0 , ℓ1 ∈ M (Rule D8)   (ℓ1 , stop) else if ℓ1 ∈ M ∧ init, ℓ0 ∈ / M (Rule D9) ( (ℓ0 , init) if init, ℓ0 ∈ M (Rule D10) ξTC3 (ℓ1 , M ) = (ℓ1 , ℓ0 ) else if ℓ0 , ℓ1 ∈ M (Rule D11)

If a child subtree still has all vertices colored init, Rule D10 first changes v to ℓ0 and enters one such subtree. On later iterations, Rule D7 keeps v colored ℓ0 and enters the next such subtree. By the induction hypothesis, the agent visits every vertex of that subtree, colors them all with ℓ1 , and returns to v. This decreases the number of child subtrees whose vertices all have color init by one. When none remains, Rule D11 if v is ℓ1 , or Rule D8 if v is ℓ0 , recolors v with ℓ1 and returns to p. Until the final return every move stays at v or inside a child subtree, so p remains ℓ0 . After Rule D2, the claim applies because s is ℓ0 and the entered child subtree is entirely init. After each return, Rule D7 enters another init-colored child if one remains. Otherwise Rule D9 recolors s with ℓ1 and stops there. Entering a child subtree and returning to its parent traverses the edge between its root and parent once in each direction. The test by Rules D3–D4 traverses the same edge at most once more in each direction. Hence the execution uses O(n) moves. Case 2 (simple cycle). Let v1 be the first selected destination, and list the cycle vertices in order as v0 = s, v1 , . . . , vn−1 , v0 . Immediately after Rule D2 and after each complete sequence Rules D3–D4–D10, the agent is at vi , the vertices v0 , . . . , vi−1 are ℓ0 , and vi and every vertex in the rest of the cycle have color init. For 1 ≤ i ≤ n − 3, the sequence Rules D3–D4–D10 moves the agent to vi+1 and restores the same condition with i + 1 in place of i. For i = n − 2, the sequence Rules D3–D5–D11 visits the last vertex vn−1 and returns to vn−3 , reversing direction. Each application of Rule D8 changes one ℓ0 vertex to ℓ1 and moves one step closer to s. Rule D9 stops at s. After Rule D2, every requested destination is unique. There are O(1) rule applications per vertex, giving O(n) moves in total. A displayed rule applies at every stage described above, so every omitted observation is unreachable.

3.2

The two-color lower bound and tightness

Lemma 4. The path P3 cannot be explored with at most two colors. Proof. We write P3 = (v1 , v2 , v3 ). By adding unused colors if necessary and renaming colors, we may assume w.l.o.g. that C = {0, 1}, with 0 as the initial color. The notation a → b means 6

that the agent recolors the current vertex to a and requests color b. The notation (vi ; a, b, c) denotes the configuration with the agent at vi and colors (a, b, c) on (v1 , v2 , v3 ). By Lemma 1, we may assume that no reachable observation uses stay. Initially, stopping leaves vertices unvisited, and only color 0 is available as a destination. Moving without recoloring reaches the initial configuration for a start at the destination. Hence Lemma 2 forces (0; {0}) 7→ 1 → 0 and (0; {0, 0}) 7→ 1 → 0. We set α = ξ(0; {1}) and β = ξ(0; {0, 1}). We start at v2 , and the adversary chooses v1 after the forced initial action. The agent then observes (0; {1}) at v1 . The vertex v3 remains unvisited. Hence α cannot stop and is either 0 → 1 or 1 → 1. We first suppose α = 0 → 1. The execution reaches (v2 ; 0, 1, 0), with observation (1; {0, 0}). There, 0 → 0 reaches an endpoint with every vertex colored 0, which is also the initial configuration for a start at that endpoint. With output 1 → 0, the adversary can choose v1 as the destination, after which α returns the agent to (v2 ; 0, 1, 0). Repeating this choice prevents termination. Every other action either stops with v3 unvisited or requests an absent color. Thus α = 1 → 1. Starting at v1 , the forced first action reaches observation (0; {0, 1}) at v2 . The vertex v3 remains unvisited. Hence β cannot stop, and it remains to consider its four possible move values. If β = 0 → 0, the executions started at v1 and v3 both reach (v2 ; 1, 0, 1). If β = 1 → 0, the same two executions, using α = 1 → 1, both reach (v2 ; 1, 1, 1). If β = 0 → 1, the execution starting at v1 reaches (v1 ; 1, 0, 0) with observation (1; {0}). At this observation, output 0 → 0 reaches the initial configuration for a start at v2 . Output 1 → 0 followed by β returns to (v1 ; 1, 0, 0), so these two actions repeat without termination. Finally, if β = 1 → 1, the execution starting at v1 reaches (v1 ; 1, 1, 0) with observation (1; {1}). With output 0 → 1, the executions starting at v1 and v3 both reach (v2 ; 0, 1, 0). With output 1 → 1, the execution starting at v1 and the execution starting at v2 after its forced first move and α both reach (v2 ; 1, 1, 0). At observations (1; {0}) and (1; {1}), stopping leaves v3 unvisited. Requesting an absent color also fails. Thus every two-color rule either has a failing execution or allows executions from distinct starts to reach the same configuration. In the latter case, Lemma 2 also gives a failing maximal execution, so no rule with at most two colors explores P3 . Since P3 is a tree, Theorem 3 and Lemma 4 show that the class of all trees and simple cycles has color complexity exactly three.

4

Four-Color Exploration

In this section, we present the four-color algorithm AC4 (Algorithm 2). It explores every graph in GCB in O(n) moves. Each edge of K1,q forms a bridge block K1,1 , so it suffices to consider complete bipartite blocks K1,1 and Kp,q with p, q ≥ 2. Moves to initial-color vertices leave their sources in front or path, distinguishing their behavior on return. Recoloring a vertex fin completes it. Since fin is never requested, completed vertices are never revisited and need no rule-table entry. At any noninitial arrival at an init vertex, its source remains a front or path neighbor. Thus an init-vertex observation whose neighbor colors are exactly init and fin is unreachable and may have an arbitrary output. Figure 2 shows two executions. To analyze the exploration, we use the following tree to represent the connections between blocks. For nonisolated s, the block-cut tree TG has one node for each block and one node for each cut vertex, with adjacency given by containment. We root TG at the cut-vertex node s when it exists and at the unique block containing s otherwise. For a nonroot block B, let ρ(B) be its parent cut vertex. For a root block B0 , set ρ(B0 ) = s. Let GB be the union of the blocks in the subtree rooted at B. We explore GB from r = ρ(B), called the parent attachment. A

7

Algorithm 2: Four-Color Exploration AC4 Colors: CC4 = {init, fin, front, path} and c0 = init Rule Function:   if init, front, path ∈ /M (Rule C1) (fin, stop) ξC4 (c, M ) = (front, init) else if fin, front, path ∈ / M (Rule C2)   ηc (M ) otherwise   (fin, path) if front, init ∈ /M (Rule C3)      else if init ∈ /M (Rule C4) (fin, front) ηinit (M ) = (path, init) else if front, path ∈ M (Rule C5)    (front, init) else if path ∈ M (Rule C6)     (front, front) else if front ∈ M (Rule C7)   (Rule C8) (path, front) if front ∈ M ηfront (M ) = (front, init) else if init ∈ M (Rule C9)   (fin, path) otherwise (Rule C10)   (front, init) if front ∈ / M ∧ init ∈ M (Rule C11)    (path, init) else if front, init ∈ M (Rule C12) ηpath (M ) =  (fin, front) else if front ∈ M (Rule C13)    (fin, path) otherwise (Rule C14)

(c ̸= fin),

child block of B is a block node D whose parent cut-vertex node is a child of B in TG . We call v = ρ(D) ∈ V (B) its child attachment. The color of a parent attachment at entry means its color after the recoloring in the move into the block. Lemma 5. Let B be a block with parent attachment r. During an execution of Algorithm 2, suppose that the agent moves from r to an init-colored vertex of B according to its rules, and every vertex of GB − r still has color init. The color of r at entry is front or path. For every adversarial choice, the agent remains in GB and never requests an absent color until its final return to r. In finite time, it colors every vertex of GB − r with fin and makes its final return to r. (i) If r is path at entry, the agent returns with r in path. (ii) If r is front at entry, the agent visits r at most once before the final return. Such a visit immediately follows entry. The agent recolors r to path and returns to the vertex just entered. At the final return, r has color front or path. Proof. We use induction on the height of B in the block-cut tree. We first show how the induction hypothesis allows us to omit exploration below child blocks, then analyze the moves within B. A move to an init vertex leaves its source in front under Rules C2, C6, C9, C11, which require no front neighbor, or in path under Rules C5, C12, which require one. Child blocks. On first entry into a child block D from v = ρ(D), all of GD −v is init-colored by the block-cut-tree structure. By induction, the agent completes GD − v and returns to v in finite time without changing B − v. The resulting fin-colored neighbors do not affect Rules C9–C14. After return from a path entry, Rule C12 enters another init neighbor if one remains; otherwise Rule C13 completes v toward the front side of B. After return from a front entry, Rule C9 8

(a) Bridge and cycle (C9, C7, C8)2

C2, C7, C8 b s

b

a

c

s

b

a

d

C142 , C1

C9, C4, C10

c

s

a

d

b c

s

b

a

d

c

s

a

d

c d

(b) Complete bipartite block K3,2 C9, C7, C8, C9, C5

C2, C7, C8 r

r y1

x1

r

x1

y1 x1

r y1

x1

y2 x2

C10, C14, C1 r

y1

y2 x2

C3, C13

y2 x2

y2 x2

(f, h) = (1, 2)

y1 x1 y2 x2

(f, h) = (1, 1)

Figure 2: Traces of Algorithm 2 for one adversary. Gray, orange, blue, and green denote init, front, path, and fin. Heavy outlines mark the agent. In (b), r is the starting vertex, X = {r, x1 , x2 } and Y = {y1 , y2 }, and (f, h) counts the front vertices of X − r and the path vertices of Y . or Rule C11 enters another init neighbor if one remains; otherwise Rule C10 or Rule C14 completes v toward the path side. Thus child exploration preserves the choice between advancing and returning in B. Each child exploration completes every vertex other than its attachment, so only finitely many occur. We omit their moves below. Between these explorations, every vertex of GB − B has color init or fin. Initial front entry. For an initial front entry at an init-colored vertex v, the entering rule is applicable only when r has no front neighbor. If v has an init-colored neighbor, Rule C7 makes v the unique front neighbor of r and moves back to r. Rule C8 must therefore return to v. Together these rules change r from front to path and leave v in front. If v has no init-colored neighbor, Rule C4 completes v and returns directly to r. Bridge. For a bridge {r, v}, the explorations below child blocks at v finish before the agent colors v with fin and returns to r. A path entry uses Rule C3 directly, or Rule C6 followed by Rule C10 or Rule C14 after explorations below child blocks. A front entry uses Rule C4 directly, or Rules C7–C8 first change r from front to path before Rule C10 or Rule C14 eventually returns there. Simple cycle. We write the cycle as r, v1 , . . . , vm , r in the direction fixed on entry. Between the rule sequences described below, the cycle vertices recolored so far form an arc from r whose far endpoint is front and whose other vertices are path. All vertices in the interior of the other arc still have color init. A path entry establishes this form when Rule C6 recolors the first vertex. For a front entry, Rules C7–C8 first change r to path and then reach the same form. Each advance uses Rule C9 followed by Rules C7–C8, recoloring the old endpoint path and moving the front endpoint one step along the arc with init-colored interior vertices. The Rule C9 move may instead enter a child block at the front endpoint. By the induction hypothesis, the agent returns to the endpoint with its color front or path, and Rule C9 or Rule C11 repeats the move because no neighbor of the endpoint is front. Once the move reaches the next cycle vertex, Rules C7–C8 restore the form above. When no init-colored cycle vertex remains, Rule C4 or Rule C13, followed by Rule C10 or Rule C14, makes the agent reverse direction. Rule C14 then completes one path vertex per step until it returns to r. Rule C11 first processes any init-colored child encountered during the return phase. The agent visits r before the final return only during the initial Rules C7–C8. 9

Complete bipartite block. We denote the bipartition of B = Kp,q by (X, Y ), where r ∈ X and p, q ≥ 2. Between the rule sequences below, r has color path, every vertex of X − r has color init, front, or fin, and every vertex of Y has color init, path, or fin, except in the final step described last. The pair (f, h) counts the front vertices in X − r and the path vertices in Y . Same-colored vertices in one partite set have identical neighborhoods in B, so every adversarial choice gives the same count change. A path entry reaches a state with r and one vertex of Y in path and one vertex of X − r in front by Rule C6 and Rules C7–C8. A front entry reaches the same state after Rules C7–C8 change r to path, followed by Rule C9 and another application of Rules C7–C8. In both cases, (f, h) = (1, 1). Advance. When both sides contain init-colored vertices, each iteration uses Rule C9, Rule C5, and Rule C6 to change one vertex of X − r to front and one vertex of Y to path, increasing both counts by one. Rule C11 and Rule C12 resume the same process after explorations below child blocks. Exhaustion of one side. If Y runs out of init-colored vertices first, the agent completes each remaining init-colored vertex of X and returns to Y , leaving (f, h) = (q − 1, q). This uses Rule C3, or Rule C6 followed by Rule C10 or Rule C14 if explorations below child blocks intervene. Rule C12 selects another init-colored vertex of X until none remains. If X runs out first, the agent similarly completes each remaining init-colored vertex of Y and returns to X − r, leaving (f, h) = (p − 1, p − 1). This uses Rule C4, or Rule C5 followed by Rule C13 after explorations below child blocks. Rule C9 or Rule C11 selects the next init-colored vertex. Return. When B has no init vertex, the return phase starts with (f, h) = (k, k) or (k − 1, k) for some k ≥ 1. Without child calls, Rule C10 maps (k, k) to (k − 1, k), and Rule C13 maps (k − 1, k) to (k − 1, k − 1) for k > 1. These moves reach (0, 1) with h ≥ 1 throughout. Child calls during the return phase change the counts only temporarily. At a vertex of Y with f ≥ 1, child calls use Rule C12 and preserve the attachment’s path color. A child call at x ∈ X − r may return with x in path instead of front, decreasing f by one. If an init neighbor remains, Rule C11 restores x to front and restores the counts. Otherwise Rule C14 completes x and moves to a path vertex of Y , which exists because h ≥ 1. At y ∈ Y with (f, h) = (0, 1), remaining child calls use Rule C11, then Rule C9 or Rule C11. These calls may change y to front and the counts to (0, 0). This is the final step that leaves the color pattern above. After all children finish, Rule C10 or Rule C14 completes y and returns to r, its unique path neighbor. Each return move completes one vertex of B − r, so the phase terminates at r. The three cases prove the lemma for B whenever it holds for its children. A leaf block has no explorations below child blocks, so induction on block height completes the proof. Theorem 6. Every graph in GCB can be explored by Algorithm 2 using four colors and O(n) moves. Proof. Each first block entry follows an algorithm rule, and the initial-color premise of Lemma 5 holds because its parent attachment is the unique access to its block-cut subtree and only the current vertex is recolored. If s is isolated, Rule C1 completes it and stops. Otherwise each move from s to an init-colored neighbor enters an unprocessed block containing s. By Lemma 5, the agent then completes all vertices other than s in the block-cut subtree below that block and returns to s. That subtree is never entered again, so after finitely many such explorations every vertex other than s is fin. Rule C1 then completes s and stops. We associate each move whose destination is an init vertex with that destination. We associate a pair Rules C7–C8 with the init-colored vertex at which Rule C7 is executed, and a return move with the vertex that it changes to fin. The algorithm never recolors a vertex init after it leaves that color and never changes a fin vertex. Thus only O(1) moves are associated with each vertex, and the agent makes O(n) moves.

10

Algorithm 3: Five-Color Exploration AUS5 Colors: CUS5 = {init, path, neigh, fin, head} and c0 = init Rule Function:   (path, init) if init ∈ M ∧ path, neigh, fin, head ∈ / M (Rule U1)      else if neigh ∈ M ∧ head ∈ /M (Rule U2) (path, stay) ξUS5 (init, M )= (neigh, head) else if head ∈ M ∧ path ∈ M (Rule U3)   (head, head) else if head ∈ M ∧ path ∈ /M (Rule U4)     (head, stay) otherwise (Rule U5)   (fin, init) if init, neigh ∈ M ∧ path, head ∈ / M (Rule U6)      (head, neigh) else if head, neigh ∈ M (Rule U7)      (path, head) else if head, path ∈ M (Rule U8)    (fin, head) else if head ∈ M (Rule U9) ξUS5 (head, M )=  (head, init) else if path, init ∈ M (Rule U10)     (head, path) else if path ∈ M (Rule U11)     (path, init) else if init ∈ M (Rule U12)    (fin, stop) otherwise (Rule U13)   (init, head) if neigh, head ∈ M (Rule U14)    (path, neigh) else if neigh ∈ M (Rule U15) ξUS5 (path, M )=  (head, stay) else if head ∈ / M (Rule U16)    (head, head) otherwise (Rule U17) ( (init, path) if path ∈ M ∧ head ∈ / M (Rule U18) ξUS5 (neigh, M )= (init, head) otherwise (Rule U19)

5

Five-Color Exploration

In this section, we present the five-color algorithm AUS5 (Algorithm 3). It explores every graph in GKTF in O(n∆) moves. In GKTF , every block containing a triangle is a clique. Algorithm 3 contains the thirteen rules of the five-color algorithm for triangle-free graphs by Takahashi et al. [26] as Rule U1, Rules U3–U5, Rules U7–U13, Rule U17, and Rule U19. These rules check the init-colored neighbors of the current path endpoint one at a time to determine whether it can extend the path. They temporarily mark rejected candidates with neigh and restore them to init before completing an expansion or a backtracking step, so that they can be tested again. We call the removal of these marks cleanup. On triangle-free graphs, no rejected candidate is adjacent to the predecessor of the endpoint, so every mark is restored through the endpoint. When the endpoint and its predecessor lie in a clique block, every rejected candidate is adjacent to the predecessor (Lemma 10). The six new rules Rule U2, Rule U6, Rules U14–U16, and Rule U18 handle this case. They temporarily recolor the predecessor with init, finish the endpoint, and restore the marks through the predecessor. No rule requests fin as a destination color, so the rule table omits the case in which the current vertex is colored fin.

11

5.1

Semi-DFS and the two cleanup conditions

A semi-DFS state consists of a path P = (u1 , u2 , . . . , uk ) with set F ⊆ V.  u1 = s and a finished Sk−1 The initial state is ((s), ∅). We define U (P, F ) = N (uk ) \ F ∪ {u1 , u2 , . . . , uk } ∪ i=1 N (ui ) as the set of neighbors of uk that are neither finished nor on P and are adjacent to no earlier vertex of P . If U (P, F ) ̸= ∅, semi-DFS appends an arbitrary vertex of U (P, F ) to P . This is a semi-DFS expansion. If U (P, F ) = ∅ and k ≥ 2, it deletes uk from P and adds it to F . This is semi-DFS backtracking. If P = (s) and U (P, F ) = ∅, it adds s to F and stops. Lemma 7 (Semi-DFS [26]). The path P remains induced throughout semi-DFS. After at most 2n iterations, the procedure has visited every vertex and terminates at s. To formulate the two conditions, we call a semi-DFS state reachable if arbitrary candidate choices can produce it from the initial state. For such a state with P = (u1 , . . . , uk ), we write a = uk for the head and p = uk−1 for its predecessor when k ≥ 2. We call any b ∈ U (P, F ) an eligible candidate and define the rejected set as R(P, F ) = {x ∈ N (a) \ (F ∪ V (P )) : N (x) ∩ {u1 , . . . , uk−1 } ̸= ∅}. We call any x ∈ R(P, F ) a rejected candidate. The simulation represents (P, F ) by coloring V \ (V (P ) ∪ F ) with init, F with fin, u1 , . . . , uk−1 with path, and uk with head. With these color roles, two moves during cleanup require structural conditions. During expansion cleanup, the old and new endpoints a, b both have color head as the neigh marks are restored. If a rejected candidate x were adjacent to b, the adversary could send the agent from x to the wrong endpoint. After a backtracking scan, either no rejected candidate is adjacent to p and all marks are restored through a, or every rejected candidate must be adjacent to p and to no earlier path vertex. Otherwise the adversary could choose the wrong path vertex. These two possible failures lead to the following conditions on every reachable state (P, F ). (i) Expansion separation: for all b ∈ U (P, F ) and x ∈ R(P, F ), {b, x} ∈ / E. (ii) Backtracking uniformity: if k ≥ 2, p = uk−1 , and U (P, F ) = ∅, then either R(P, F ) ∩ N (p) = ∅, or every x ∈ R(P, F ) satisfies {x, p} ∈ E and N (x) ∩ V (P ) = {p, a}. A graph has the uniform separation property when both conditions hold for every reachable state from every start s. Figure 3 shows the two configurations. (a) Expansion separation x

P

ui

···

(b) Backtracking uniformity R(P, F ) x ···

b p

a

x ∈ R(P, F ), b ∈ U (P, F ) =⇒ {x, b} ∈ /E

P

ui

···

p

z

a

R(P, F ) ∩ N (p) ̸= ∅ =⇒ N (y) ∩ V (P ) = {p, a} (∀y ∈ R(P, F ))

Figure 3: The two conditions that prevent cleanup from moving to the wrong endpoint. Blue, orange, and teal denote path, head, and neigh. The crossed dashed edge in (a) is forbidden.

5.2

Five-color simulation

A configuration γ = (v, ψ) is consistent if the vertices colored neither init nor fin form an induced path P (γ) = (u1 , . . . , uk ) with u1 = s, every ui with i < k is colored path, and uk = v is colored head. This path is unique. With F (γ) = {v ∈ V : ψ(v) = fin}, the configuration represents the semi-DFS state (P (γ), F (γ)). 12

Lemma 8. On a graph with the uniform separation property, from every consistent configuration representing a reachable semi-DFS state (P, F ), Algorithm 3 reaches one of the following outcomes in finite time. (i) If U (P, F ) ̸= ∅, it reaches a consistent configuration representing an expansion P 7→ P ◦ b for some b ∈ U (P, F ). (ii) If U (P, F ) = ∅ and |P | ≥ 2, it reaches the consistent configuration representing the corresponding backtracking step. (iii) If P = (s) and U (P, F ) = ∅, it stops at s. Proof. Start. For P = (s), Rule U12 followed by Rule U5 makes an init-colored neighbor the new head, and Rule U13 stops if none exists. Scan. For |P | ≥ 2, Rule U10 visits the init-colored neighbors of the head a one at a time, and each visit returns through the unique head vertex a. Rule U3 marks a candidate neigh when the agent sees path there, and otherwise Rule U4 colors it head. The scan ends either with a new head b and the scanned rejected candidates marked, or with every init-colored neighbor of a marked. Expansion cleanup. With a and b both head, Rule U7 moves to a mark and Rule U19 restores it and returns to head, which is a alone because expansion separation keeps every rejected candidate away from b. After the last mark, Rule U8 recolors a with path and moves to b, which gives the consistent configuration of P ◦ b. Backtracking. If no candidate is eligible, Rule U11 moves to the predecessor p, and backtracking uniformity leaves two patterns. If p is adjacent to no mark, Rule U17 makes p a head and returns to a, repetitions of Rules U7 and U19 restore the marks through a, and Rule U9 finishes a and moves to p. If p is adjacent to one mark, it is adjacent to all of them, so Rule U14 temporarily recolors p with init, Rule U6 finishes a and moves to p as the unique init neighbor of a, and Rule U2 recolors p with path. Repetitions of Rules U15 and U18 then restore the marks through p, which is their unique path neighbor by uniformity, and Rule U16 makes p the head. Both patterns give the consistent configuration of P without a. Each scan or cleanup iteration removes one remaining candidate, so every phase is finite. Theorem 9. Every graph with the uniform separation property can be explored by Algorithm 3 using five colors and O(n∆) moves. Proof. At a nonisolated start, Rule U1 followed by Rule U5 creates the first consistent configuration. At an isolated start, Rule U5 followed by Rule U13 stops there. The simulation established by Lemma 8 follows semi-DFS step by step. Lemma 7 therefore gives finite exploration of all vertices and termination at s. There are at most 2n semi-DFS steps. Each examines at most ∆ candidates and restores their colors with constant work per candidate, for O(n∆) moves.

5.3

Structural characterization

Lemma 10. Expansion separation holds in every reachable semi-DFS state from every start if and only if the graph belongs to GKTF . Every graph in GKTF also satisfies backtracking uniformity. Consequently, the uniform separation property holds exactly for graphs in GKTF . Proof. We first suppose that G ∈ GKTF and that expansion separation fails for an eligible candidate b and a rejected candidate x. Since both are adjacent to the head a and {b, x} ∈ E, the vertices a, b, x form a triangle. Because x is rejected, it has a neighbor ui earlier on P . The edge {x, ui }, the subpath from ui to a, and {a, x} form a cycle sharing the edge {a, x} with that triangle. The triangle and cycle therefore lie in one block, which must be a clique because G ∈ GKTF . This forces {b, ui } ∈ E, contradicting the eligibility of b. 13

Next, we assume x ∈ R(P, F ) ∩ N (p). The triangle x, p, a lies in a block containing {p, a}. Because G ∈ GKTF , this block is a clique. For every rejected candidate y, its edge to an earlier path vertex together with the subpath to a and the edge {a, y} forms a cycle using {p, a}. Hence this cycle lies in the same clique block, which forces {y, p} ∈ E. If y were also adjacent to some uj with j ≤ k − 2, the same clique block would force {uj , a} ∈ E, contradicting the fact that P is induced. Thus backtracking uniformity follows. For the converse, we assume that expansion separation always holds and that a block B contains a triangle but is not a clique. We will construct a reachable state with adjacent vertices b ∈ U (P, F ) and z ∈ R(P, F ), contradicting expansion separation. We choose an inclusionmaximal clique K ⊊ V (B) that contains a triangle. By biconnectivity, some component C of B − K has two distinct neighbors in K. We choose a shortest path Q = a, q1 , . . . , qt , z with t ≥ 1, all internal vertices in C, and distinct endpoints in K. Then Q − z is induced. Indeed, any chord of Q − z would give a shorter path with two endpoints in K and all internal vertices in C. We claim that some b ∈ K \ {a, z} is adjacent to no qi . If t ≥ 2, any b ∈ K \ {a, z} suffices, and such a vertex exists because K contains a triangle. An edge {b, qi } would contradict the minimality of Q. For i < t, the path a, q1 , . . . , qi , b is shorter than Q. For i = t, the path b, qt , z is shorter than Q. If t = 1, maximality of K gives a vertex b ∈ K \ {a, z} nonadjacent to q1 , since otherwise K ∪ {q1 } would be a larger clique. We start semi-DFS at qt , and the adversary follows the vertices of Q − z in reverse order until it reaches a. These choices are eligible because Q − z is induced. The resulting path is the reverse of Q − z and has F = ∅. The vertex z is rejected because it is adjacent to the head a and the earlier path vertex qt . The vertex b is eligible because it is adjacent to a and to none of the qi . Finally, {b, z} ∈ E because both vertices lie in the clique K, contradicting expansion separation. Theorem 11. Every graph in GKTF can be explored by Algorithm 3 using five colors and O(n∆) moves. Proof. Lemma 10 gives the uniform separation property, so Theorem 9 applies. The diamond K4 − e is φ-free but not in GKTF , whereas K5 is in GKTF but not φ-free, so the two classes are incomparable. A graph is unichord-free if no cycle has exactly one chord [27]. A structure theorem of Trotignon and Vušković gives a further consequence for this class. Corollary 12. Every unichord-free graph can be explored with five colors and O(n∆) moves. Proof. Every block is an induced subgraph and hence unichord-free, and it has no cut vertex. By [27, Theorem 2.2], a connected unichord-free graph that contains a triangle is a clique or has a cut vertex in the maximal clique containing that triangle. Hence every block containing a triangle is a clique, so the graph belongs to GKTF and Theorem 11 applies.

6

A Four-Color Lower Bound for Subcubic Pseudotrees

In this section, we use the obstruction family H of nine graphs in Figure 4 to show that no single rule with at most three colors explores every subcubic pseudotree. By adding unused colors if necessary and renaming colors, we may assume w.l.o.g. that C = {0, 1, 2}, with 0 as the initial color. By Lemma 1, candidate successful rules may be restricted to those that never stay at a reachable observation. Initially, the current vertex and all its neighbors have color 0, so the observation depends only on the degree of the starting vertex. At a start of degree d ∈ {1, 2, 3}, stopping would leave vertices unvisited, and color 0 is the only neighbor color that can be requested. Thus the first action writes a color rd ∈ C determined by d and moves to a neighbor of color 0. We call the triple (r1 , r2 , r3 ) the initial tuple and abbreviate it as r1 r2 r3 . 14

C3

T5

K1,3

C5

C4

C4 + leaf

C3 + leaf

C3 + tail of length 2

C3 + 2 leaves

Figure 4: The obstruction family H of nine subcubic pseudotrees on at most five vertices. Theorem 13. No single rule with at most three colors explores every subcubic pseudotree. Proof. Suppose that a common successful rule exists, and let r1 r2 r3 be its initial tuple. The graphs C3 and K1,3 are subcubic pseudotrees containing vertices of degrees 2 and 1, 3, respectively. If rd = 0 for some d ∈ {1, 2, 3}, the first move from a degree-d vertex in one of these graphs reaches the initial configuration for its destination. Lemma 2 then contradicts success, so r1 , r2 , r3 ̸= 0. Up to exchanging colors 1 and 2, the remaining eight tuples reduce to the four representatives 111, 121, 211, 221. After this reduction, one rule must still explore every graph in the obstruction family H of Figure 4. The computer-assisted Lemma 14 in Appendix A excludes such a common rule for each of the four initial representatives. Hence no single rule with at most three colors explores every subcubic pseudotree. Consequently, every graph class that contains all subcubic pseudotrees and is contained in GCB has color complexity exactly four, since Algorithm 2 explores every graph in GCB .

7

Conclusion

We obtain tight three-color bounds for trees and simple cycles and tight four-color bounds for every class between subcubic pseudotrees and GCB , including cacti. The five-color cleanup conditions characterize GKTF . A four-color lower bound without computer assistance or for a single graph remains open.

Use of AI tools OpenAI Codex (GPT-5.6 Sol/xhigh) assisted with editing and verification and implemented most of the lower-bound code, all of which the authors reviewed.

References [1] Romas Aleliunas, Richard M. Karp, Richard J. Lipton, László Lovász, and Charles Rackoff. Random walks, universal traversal sequences, and the complexity of maze problems. In 20th Annual Symposium on Foundations of Computer Science (FOCS 1979), pages 218–223. IEEE, 1979. doi:10.1109/SFCS.1979.34. [2] John Augustine and William K. Moses Jr. Dispersion of mobile robots. Proceedings of the 19th International Conference on Distributed Computing and Networking, Jan 2018. doi:10.1145/3154273.3154293.

15

[3] Hans-Joachim Böckenhauer, Fabian Frei, Walter Unger, and David Wehner. Zeromemory graph exploration with unknown inports. In 30th International Colloquium on Structural Information and Communication Complexity (SIROCCO 2023), volume 13892 of Lecture Notes in Computer Science, pages 246–261. Springer, 2023. doi:10.1007/ 978-3-031-32733-9_11. [4] Dominik Bojko, Karol Gotfryd, Dariusz R. Kowalski, and Dominik Pająk. Tree Exploration in Dual-Memory Model. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), pages 22:1–22:16, 2022. doi:10.4230/LIPIcs.MFCS. 2022.22. [5] Reuven Cohen, Pierre Fraigniaud, David Ilcinkas, Amos Korman, and David Peleg. Labelguided graph exploration by a finite automaton. ACM Transactions on Algorithms, 4(4):42:1–42:18, 2008. doi:10.1145/1383369.1383373. [6] Yann Disser, Jan Hackfeld, and Max Klimm. Tight bounds for undirected graph exploration with pebbles and multiple agents. Journal of the ACM, 66(6):40:1–40:41, 2019. doi: 10.1145/3356883. [7] Stefan Dobrev, Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro. Searching for a black hole in arbitrary networks: Optimal mobile agents protocols. Distributed Computing, 19(1):1–18, 2006. doi:10.1007/s00446-006-0154-y. [8] Stefan Dobrev, Paola Flocchini, Giuseppe Prencipe, and Nicola Santoro. Mobile search for a black hole in an anonymous ring. Algorithmica, 48:67–90, 2007. doi:10.1007/ s00453-006-1232-z. [9] Stefan Dobrev, Nicola Santoro, and Wei Shi. Using scattered mobile agents to locate a black hole in an un-oriented ring with tokens. International Journal of Foundations of Computer Science, 19(06):1355–1372, 2008. doi:10.1142/S0129054108006327. [10] Taichi Inoue, Naoki Kitamura, Taisuke Izumi, and Toshimitsu Masuzawa. Computational power of a single oblivious mobile agent in two-edge-connected graphs. In 26th International Conference on Principles of Distributed Systems (OPODIS 2022), volume 253 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1–11:18, 2023. doi:10.4230/ LIPIcs.OPODIS.2022.11. [11] Michal Koucký. Universal traversal sequences with backtracking. Journal of Computer and System Sciences, 65(4):717–726, 2002. doi:10.1016/S0022-0000(02)00023-5. [12] Ajay D. Kshemkalyani and Faizan Ali. Efficient dispersion of mobile robots on graphs. In Proceedings of the 20th International Conference on Distributed Computing and Networking, pages 218–227, 2019. doi:10.1145/3288599.3288610. [13] Ajay D. Kshemkalyani, Anisur Rahaman Molla, and Gokarna Sharma. Fast dispersion of mobile robots on arbitrary graphs. In International Symposium on Algorithms and Experiments for Sensor Systems, Wireless Networks and Distributed Robotics, pages 23–40. Springer, 2019. doi:10.1007/978-3-030-34405-4_2. [14] Artur Menc, Dominik Pająk, and Przemysław Uznański. Time and space optimality of rotor-router graph exploration. Information Processing Letters, 127:17–20, 2017. doi: 10.1016/j.ipl.2017.06.010. [15] Fukuhito Ooshita, Shinji Kawai, Hirotsugu Kakugawa, and Toshimitsu Masuzawa. Randomized gathering of mobile agents in anonymous unidirectional ring networks. IEEE Transactions on Parallel and Distributed Systems, 25(5):1289–1296, 2013. doi:10.1109/ TPDS.2013.259. 16

[16] Petrişor Panaite and Andrzej Pelc. Exploring unknown undirected graphs. Journal of Algorithms, 33(2):281–295, 1999. doi:10.1006/JAGM.1999.1043. [17] Vyatcheslav B. Priezzhev, Deepak Dhar, Abhishek Dhar, and Supriya Krishnamurthy. Eulerian walkers as a model of self-organized criticality. Physical Review Letters, 77(25):5079, 1996. doi:10.1103/PhysRevLett.77.5079. [18] Omer Reingold. Undirected connectivity in log-space. Journal of the ACM, 55(4):1–24, 2008. doi:10.1145/1391289.1391291. [19] Masahiro Shibata, Toshiya Mega, Fukuhito Ooshita, Hirotsugu Kakugawa, and Toshimitsu Masuzawa. Uniform deployment of mobile agents in asynchronous rings. In Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing, pages 415–424, 2016. doi:10.1145/2933057.2933093. [20] Masahiro Shibata, Daisuke Nakamura, Fukuhito Ooshita, Hirotsugu Kakugawa, and Toshimitsu Masuzawa. Partial gathering of mobile agents in arbitrary networks. IEICE Transactions on Information and Systems, E102.D(3):444–453, 2019. doi:10.1587/ transinf.2018FCP0008. [21] Masahiro Shibata, Yuichi Sudo, Junya Nakamura, and Yonghwan Kim. Uniform deployment of mobile agents in dynamic rings. In International Symposium on Stabilizing, Safety, and Security of Distributed Systems, pages 248–263. Springer, 2020. doi: 10.1007/978-3-030-64348-5_20. [22] Kohei Shimoyama, Yuichi Sudo, Hirotsugu Kakugawa, and Toshimitsu Masuzawa. One bit agent memory is enough for snap-stabilizing perpetual exploration of cactus graphs with distinguishable cycles. In Stabilization, Safety, and Security of Distributed Systems (SSS 2022), volume 13751 of Lecture Notes in Computer Science, pages 19–34, 2022. doi: 10.1007/978-3-031-21017-4_2. [23] Yuichi Sudo, Daisuke Baba, Junya Nakamura, Fukuhito Ooshita, Hirotsugu Kakugawa, and Toshimitsu Masuzawa. A single agent exploration in unknown undirected graphs with whiteboards. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, E98.A(10):2117–2128, 2015. doi:10.1587/TRANSFUN.E98.A.2117. [24] Yuichi Sudo, Fukuhito Ooshita, and Sayaka Kamei. Self-stabilizing graph exploration by a single agent. Theoretical Computer Science, 1082:116085, 2026. doi:10.1016/j.tcs.2026. 116085. [25] Yuichi Sudo, Masahiro Shibata, Junya Nakamura, Yonghwan Kim, and Toshimitsu Masuzawa. Near-Linear Time Dispersion of Mobile Agents. In 38th International Symposium on Distributed Computing (DISC 2024), pages 38:1–38:22, 2024. doi:10.4230/LIPIcs. DISC.2024.38. [26] Shota Takahashi, Haruki Kanaya, Shoma Hiraoka, Ryota Eguchi, and Yuichi Sudo. Recolorable graph exploration by an oblivious agent with fewer colors. In 29th International Conference on Principles of Distributed Systems (OPODIS 2025), volume 361 of Leibniz International Proceedings in Informatics (LIPIcs), pages 32:1–32:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2026. doi:10.4230/LIPIcs.OPODIS.2025.32. [27] Nicolas Trotignon and Kristina Vušković. A structure theorem for graphs with no cycle with a unique chord and its consequences. Journal of Graph Theory, 63(1):31–67, 2010. doi:10.1002/jgt.20405.

17

[28] Vladimir Yanovski, Israel A. Wagner, and Alfred M. Bruckstein. A distributed ant algorithm for efficiently patrolling a network. Algorithmica, 37(3):165–186, 2003. doi: 10.1007/s00453-003-1030-9.

A

Certificate for the Three-Color Subcubic-Pseudotree Lower Bound

This appendix proves the computer-assisted Lemma 14 used in Section 6. We first specify the graphs and initial tuples and state the lemma. We then prove that the base encoding represents a common exploration rule and that the additional clauses are sound. Finally, we describe the checked unsatisfiability certificates, reproduction procedure, and trusted software, and complete the proof of the lemma. The source code, fixed inputs, and verification scripts for this certificate are available in the repository below. https://github.com/littlegirl0820/color-complexity-recolorable-exploration

A.1

Obstruction family and initial representatives

Throughout this appendix, C = {0, 1, 2} and the initial color is 0. At an all-zero observation of degree d ∈ {1, 2, 3}, any successful rule that never stays at a reachable observation must write some rd ∈ C and move to color 0. We call r1 r2 r3 its initial tuple. The family H in Figure 4 consists of two trees and seven graphs containing exactly one cycle, all on three to five vertices. The graph T5 is K1,3 with one edge subdivided. Throughout the encoding, τ ranges over the four representatives 111, 121, 211, 221. Lemma 14 (Computer-assisted). Let C = {0, 1, 2} be the color set, with initial color 0. Let τ ∈ {111, 121, 211, 221}. No single deterministic three-color rule with initial tuple τ that never stays at a reachable observation explores every graph in H from every start and against every adversarial choice. We prove this lemma at the end of the appendix using the encoding and verification results below.

A.2

Exact base encoding

We fix one representative τ . The possible observations at nonisolated vertices of graphs of maximum degree three form the set O = {(c, M ) ∈ C × M(C) : 1 ≤ |M | ≤ 3}.
Since the number of multisets of size d over three colors is d+2 2 , |O| = 3

 3  X d+2 d=1

2

= 3(3 + 6 + 10) = 57.

The encoding represents the rule using the ten actions in A = {astop }∪C 2 . An action (c′ , d) ∈ C 2 recolors the current vertex with c′ and moves to a neighbor of color d. For an observation o = (c, M ), the available actions are Act(o) = {astop } ∪ {(c′ , d) ∈ C 2 : d ∈ M }. 18

A stopping action ends the execution immediately, so its written color is irrelevant. We therefore represent all three actions (c′ , stop), c′ ∈ C, by the single action astop . For every o ∈ O and a ∈ A, the generator allocates a rule variable xo,a and adds the exactlyone clauses _ xo,a , ¬xo,a ∨ ¬xo,b (a, b ∈ A, a ̸= b). a∈A

For each action a ∈ A \ Act(o) that requests a color absent from the neighborhood, the generator adds the unit clause ¬xo,a . Three further unit clauses fix the actions at the all-zero observations τ of degrees 1, 2, and 3 according to τ . We write Prule for these exactly-one, availability, and initial-tuple clauses. The remaining variables and clauses are generated separately for every H ∈ H. We denote the set of all configurations of H by QH . For q = (v, ψ) ∈ QH , we write Mψ (v) = {{ψ(u) : u ∈ N (v)}} and o(q) = (ψ(v), Mψ (v)). For a configuration q = (v, ψ) and a selected action a, the set of configurations that the adversary may choose next is denoted by δH (q, a). If a is not stopping, then δH (q, a) is nonempty by the definition of allowed actions. The encoding expresses four requirements. It must include every configuration that the adversary can reach, ensure finite termination, require return to the chosen start, and require every vertex to be visited before stopping. Variables Rq and ranks h(q) express the first two requirements. Variables Ts,q remember the start for the third. Variables Rq¬m track an execution that has not visited m for the fourth. The encoding introduces a reachability variable Rq for each configuration q. For every start s, the symbol qs0 denotes the all-zero initial configuration, and the encoding contains the unit clause Rqs0 . For every q ′ ∈ δH (q, a), it contains ¬Rq ∨ ¬xo(q),a ∨ Rq′ to require q ′ to be reachable whenever q is reachable and the rule selects a. We write Preach (H) for these clauses. Each q has a rank h(q) of ⌈log2 |QH |⌉ bits. For every nonstopping successor q ′ ∈ δH (q, a), the encoding contains a standard binary-comparator CNF for Rq ∧ xo(q),a

=⇒

h(q ′ ) < h(q).

This condition forces the rank to decrease at every reachable transition. The ranks of configurations marked unreachable may have arbitrary values. We write Pterm (H) for the comparator clauses. The variables Rq combine executions from every start, so a separate family records where each execution began. For the start-specific reachability variables Ts,q , the encoding contains the unit clause Ts,qs0 . For every q ′ ∈ δH (q, a), it contains ¬Ts,q ∨ ¬xo(q),a ∨ Ts,q′ to propagate reachability from start s to every adversarial successor. With astop denoting the stopping action, the encoding also contains ¬Ts,q ∨ ¬xo(q),astop whenever the current position in q is not s. This prevents an execution started at s from stopping elsewhere. We write Preturn (H) for these clauses. The variable Rq¬m means that q is reachable along an execution prefix that has not yet visited vertex m. For every start s and vertex m ̸= s, the encoding contains the unit clause Rq¬m 0 . It s ¬m ′ ′ propagates Rq over a transition q → q only when the current position of q is not m. For every such q ′ ∈ δH (q, a), it contains ¬Rq¬m ∨ ¬xo(q),a ∨ Rq¬m ′ . 19

For every q and m, it also contains ¬Rq¬m ∨ ¬xo(q),astop . Hence an execution leaving any vertex unvisited cannot stop. We write Pvisit (H) for these clauses. The encoding does not require each configuration marked reachable to have a marked predecessor. When constructing an assignment from a successful rule, we use exactly the configurations that the rule can reach. In the other direction, the initial unit clauses and the transition clauses ensure that every configuration actually reached by the rule is marked reachable. The base encoding is ^
τ Bτ = Prule ∧ Preach (H) ∧ Pterm (H) ∧ Preturn (H) ∧ Pvisit (H) . H∈H

A.3

Exactness of the base encoding

Lemma 15. The formula Bτ is satisfiable if and only if there exists a three-color rule with initial tuple τ satisfying two conditions. The rule never stays at a reachable observation. It explores every graph in H from every start against every adversarial choice. Proof. A satisfying assignment selects a unique available action at each observation. These actions define the rule. The Rq clauses mark every configuration that the adversary may reach from a marked configuration. The ranks strictly decrease at every such move, so an execution cannot be infinite. Every maximal execution therefore stops. The Ts,q clauses require every stop to be at its start. The Rq¬m clauses forbid a stop before every vertex has been visited. For the converse, we start with a successful rule. We first redefine its outputs at unreachable observations to use arbitrary available non-stay actions. This does not change any execution. We assign each reachability variable according to whether the corresponding configuration is actually reachable, including the variants that record the start and an unvisited vertex. A directed cycle in the reachable configuration-transition graph would let the adversary repeat it forever, so that graph is acyclic. We order its configurations topologically so that every transition goes from a larger position to a smaller one. These positions give the required ranks, and all clauses of Bτ follow.

A.4

Additional clauses checked independently

The exact encoding Bτ is large and difficult to refute directly. We therefore add three families of clauses that every successful rule satisfies. They shorten the propositional proof but do not change the represented exploration problem. For distinct starts s, t and every configuration q, the encoding contains ¬Ts,q ∨ ¬Tt,q . These clauses form Pmerge . If a successful rule is assigned its actual start-specific reachable sets, both variables cannot be true. Otherwise the two executions reach q, and Lemma 2 gives a failing maximal execution, contradicting the assumption that the rule explores the graph. Separate checkers verify the remaining two kinds of additional clauses. The generator imports 279,197 such clauses over the rule variables. They consist of 252,515 trace clauses and 26,682 domain clauses. A trace clause has the form _ ¬xoi ,ai . i

The simultaneous assignments xoi ,ai = 1 fix a partial rule with ξ(oi ) = ai . With these actions fixed, an execution fails if it stops away from its start, stops leaving some vertex unvisited, 20

requests an absent color, or runs forever. The supplied checker searches for a failing execution prefix or a reachable cycle using only the fixed actions on some H ∈ H and start s. It stops a search branch when the next observation has no fixed action. Every accepted witness therefore remains a failure for every complete rule containing the fixed actions. Every successful rule must therefore satisfy the clause. A domain certificate assigns a nonempty set D(o) ⊆ Act(o) to every observation and contributes _ _ xo,a . o

a∈Act(o)\D(o)

The checker solves a finite reachability game. For a fixed graph H and start s, a game state records the agent position, the complete vertex coloring, and the set of vertices already visited. The controller may choose an action from D(o) separately at every game state, even when two game states have the same observation o. The checker accepts only if the all-zero game state at start s is losing against the adversary. This controller can make more choices than a deterministic rule restricted to D, because it may choose different actions at states with the same observation. If even this controller loses when restricted to D, then every deterministic rule using only actions in D also loses. Every successful rule must therefore select an action outside D at some observation and satisfy the clause. We write Ptrace and Pdomain for these two clause families and set Fτ = Bτ ∧ Pmerge ∧ Ptrace ∧ Pdomain . Lemma 2 proves the soundness of Pmerge . Separate routines verify Ptrace and Pdomain independently of the SAT solver and DRAT proof. Neither check assumes a fixed initial representative τ . Together with Lemma 15, they show that Fτ is satisfiable exactly when such a successful rule with initial representative τ exists.

A.5

Reference encoding and checked proof objects

The reference encoding FH contains the base and strengthening clauses for all nine graphs but does not fix one particular τ . It instead imposes r1 , r2 ∈ {1, 2} and r3 = 1. Thus one common rule chooses one of the four representatives and shares every other action across the four cases. Lemma 15 and the soundness of the additional clauses show that FH is satisfiable exactly when such a successful rule exists. For each Fτ , we take its checked unsatisfiable core and remove the unit clauses fixing τ . We unite the four remaining clause sets, add the three constraints above, and delete duplicates. The result is the combined unsatisfiable core, a subformula of FH . The same DRAT refutation has been checked against both this core and the containing reference encoding. We obtain the reduced encoding by removing unused variables, renumbering the remaining variables, and applying core extraction twice. Its new DRAT proof is checked independently of the original proof. The reference encoding directly represents the graph-exploration problem. The combined core and reduced encoding give smaller checked routes to the same contradiction. Table 2 gives the dimensions of the checked objects. Of the 984,882 variables in FH , 832,032 are auxiliary variables introduced by the transitionwise binary rank comparators. The rule, reachability, and rank variables account for the remainder.

A.6

Reproducing the proof and required trusted software

The reproducible proof chain runs from H in graph6 form through FH to a checked DRAT refutation. The repository preserves the vertex labels, and the verification script checks that its graph6 strings encode the nine graphs in Figure 4. For the archived proof, the supplied generator reproduced the 111 CNF. A second program replaced the degree-one and degree-two 21

Table 2: Checked objects for the three-color subcubic-pseudotree lower bound. File sizes are uncompressed bytes. Object Reference encoding FH Combined unsatisfiable core Reduced encoding Binary DRAT for reference/combined encodings Binary DRAT for reduced encoding

Variables

Clauses

Bytes

984,882 984,882 282,535 — —

4,756,124 904,855 433,150 — —

118,444,022 18,905,669 9,817,630 1,749,789,591 1,435,082,233

unit clauses with disjunctions that allow either value 1 or 2 and retained r3 = 1. The resulting formula was FH . The verification script compared the generated formula byte for byte with the stored reference CNF used by the checked DRAT proof. This comparison linked the checked graph and clause inputs to that exact reference CNF. The repository contains the fixed inputs, generator, checkers, and a script for regenerating the four branch proofs. It does not contain the large precomputed CNF and DRAT files or the denseto-original variable map. No separate precomputed-proof archive is part of this distribution. The script reproduction/regenerate_and_verify.sh checks the graph, trace-clause, and domainclause inputs, generates Fτ for each of the four representatives, and compares each CNF with its recorded SHA-256 hash. It then uses CaDiCaL to produce a DRAT refutation for each branch and checks every refutation with drat-trim. Together with the initial-tuple reduction, these four checks establish the same lower bound without the archived combined or reduced proof objects. The repository’s README gives the commands and dependencies. Four parallel branches took about half a day in the reference environment, with about 7 GB of free disk space and 10 GB of memory. As a positive control for the generator, the encoding for the two trees and three cycles in H, including the merge clauses, is satisfiable. It remains satisfiable when the rule of Algorithm 1 is fixed by unit clauses. Replacing its action at the degree-one all-zero observation (0; {{0}}) by a stop makes it unsatisfiable. Moreover, the base encoding of every single graph in H is satisfiable, so no graph in H alone witnesses the lower bound, which is a statement about one rule for all nine graphs. In the reference environment, drat-trim reported s VERIFIED for the reference encoding, combined core, and reduced encoding. For all three verifications, drat-trim reported zero RAT lemmas. Every proof addition retained in the checked cores was verified by reverse unit propagation. The three checks took approximately 164, 132, and 79 minutes, with about 3 GiB of peak memory in the largest check. The file certificate/SHA256SUMS records the hashes of these archived CNF, DRAT, and variable-map files. The trusted base consists of the generator, the independent checkers, the C++ toolchain and runtime, the Node.js runtime, SHA-256, and drat-trim. It excludes the SAT solver and core-extraction tools, since the generated refutations are checked independently. The trusted programs comprise about 1,700 lines of C++ and 1,200 lines of Node.js. Lemma 15 establishes the semantic interpretation of the base encoding. The source checkers validate the graph and clause inputs used by the generator. In the regeneration procedure, drat-trim checks the generated Fτ for all four representatives, and the initial-tuple reduction then gives the lower bound. Proof of Lemma 14. Suppose that a successful rule has one of the four initial representatives. By Lemma 15, this rule gives a satisfying assignment of the corresponding base formula Bτ . The soundness of the merge clauses and of the independently checked trace and domain clauses ensures that the assignment corresponding to the successful rule also satisfies the additional clauses. Hence the reference encoding FH , which combines the four representatives, is satisfiable. 22

However, the reference CNF regenerated from the checked graph and clause inputs is byteidentical to the stored reference CNF, and its DRAT refutation has been checked by drat-trim. Thus FH is unsatisfiable, a contradiction.

23