July 16, 2026
Enumerating simple paths and cycles subject to a given length bound is a fundamental problem in graph algorithms with applications ranging from network analysis to computational biology. Recent algorithms for this problem, namely \(\mathrm{\small CYCLE\_SEARCH}\) (Gupta and Suzumura, 2021) and \(\mathrm{\small BC-DFS}\) (Peng et al., 2019, 2021), employ barrier values to prune fruitless searches.
Both algorithms have been shown incomplete and their delay-bound arguments rely on monotonicity claims that are flawed. For \(\mathrm{\small CYCLE\_SEARCH}\) this was shown previously. In this paper we establish the analogous results for \(\mathrm{\small BC-DFS}\) by presenting new counter-examples and identifying a defect in its barrier-update procedure.
As our main contribution, we introduce the concept of edge-consistency, a local invariant on barrier values analogous to heuristic consistency in informed search. Edge-consistency provides an incremental mechanism for maintaining admissible barrier estimates and yields concise correctness proofs.
We use edge-consistency as a unifying framework for design and analysis of Bounded-Scope Depth-First Search (\(\mathrm{\small BS-DFS}\)) — a new \(O(k(n+m))\) delay algorithm for enumerating simple paths or cycles of length at most \(k\) in a directed graph — and of several variants of it. We also use edge-consistency to pinpoint the precise failure mechanism of \(\mathrm{\small BC-DFS}\).
Experimental results confirm that the omissions in \(\mathrm{\small BC-DFS}\) are not isolated edge cases and occur with noticeable frequency on random graphs.
The enumeration of simple paths and cycles in directed graphs is a classical problem in graph algorithms, with applications ranging from chemistry and circuit analysis to network science.
The classical line of work places no bound on the length of the reported paths or cycles. Early work by Tiernan [1] introduced a backtracking algorithm for enumerating elementary circuits, but suffered from exponential run-time in some dense graphs; Tarjan [2] reduced this redundancy by a marking scheme. A breakthrough was achieved by Johnson [3], whose influential algorithm combines depth-first search with a Boolean blocking-unblocking mechanism to avoid repeatedly exploring fruitless search branches; it runs in \(O((n+m)(c+1))\) time, where \(c\) denotes the number of simple cycles. Subsequent work, including that of Szwarcfiter and Lauer [4], refined these ideas, and Tarjan’s algorithm for strongly connected components [5] continues to serve as a preprocessing step in many enumeration algorithms. Birmelé et al. [6] give output-sensitive algorithms that list all simple cycles, and all simple \(s\)-\(t\)-paths, in undirected graphs, optimal in the total output size. A survey on enumeration algorithms in graphs was compiled in 2016 by Grossi [7].
Since the number of simple paths and cycles may grow exponentially with the size of the graph, unrestricted enumeration is generally impractical on large instances; moreover, many associated decision problems, including the classical Hamiltonian path and Hamiltonian cycle problems, are NP-complete [8]. Practical applications therefore often restrict the problem, most commonly by a bound \(k\) on the path or cycle length. In many contemporary applications the underlying graphs are huge, but only paths or cycles up to a small length bound are of interest; examples are the analysis of large social networks, fraud detection in transaction networks, and motif discovery in biological networks.
Rizzi et al. [9] impose such a length bound, listing all length-bounded simple \(s\)-\(t\)-paths. Their focus is the weighted case, matching the classic \(K\)-shortest-paths time bounds in only \(O(n+m)\) space while a short remark deals with the unweighted case. For the unweighted case, they suggest using a reverse (from the target) breadth-first search at each node visited to eliminate the fruitless (no output generating) successors from the depth-first recursion.
The length-bounded setting has further stimulated the development of algorithms pruning the depth-first search efficiently by maintaining per-node barrier values. Two notable such algorithms are CYCLE_SEARCH, introduced by Gupta and Suzumura [10], and BC-DFS, proposed by Peng et al. [11], [12]. Both algorithms build upon ideas originating in Johnson’s algorithm, but replace the classical binary blocking mechanism by numeric barrier values. These barrier values are intended to cache information about previously explored searches and thereby avoid redundant fruitless exploration. These algorithms are shown to be very efficient in practical experiments, and they are claimed to achieve a worst-case delay of \(O((k-1)(n+m))\) and \(O(km)\), respectively, per output.
Unfortunately, the correctness of these barrier-based approaches has proven to be more delicate than originally anticipated. For \(\mathrm{\small CYCLE\_SEARCH}\), counter-examples and proof gaps were identified by Bauernöppel and Sack [13]. As a remedy, they suggest using an approach similar to Rizzi’s unweighted case: use depth-first search starting at \(s\) and prune it by exact barrier values, freshly computed by a reverse (from \(t\)) depth-limited breadth-first search for each node visited in the depth-first search. In contrast to Rizzi, the underlying graph \(G\) is not mutated during recursion.
Although the breadth-first search at every node visit does not affect the asymptotic delay bound, it repeatedly recomputes essentially the same information. Peng et al. [11], [12] (where a similar approach for path enumeration is named T-DFS) report that “T-DFS demonstrates the worst performance on most of the graphs although it is a polynomial delay algorithm with a nice theoretical guarantee”. The central challenge is therefore developing an efficient barrier based output-sensitive enumeration algorithm with proven correctness and delay bound.
We introduce Bounded-Scope Depth-First Search (\(\mathrm{\small BS-DFS}\)), a simple and efficient algorithm for enumerating all length-bounded simple paths or simple cycles in a directed graph for a given node pair \(s, t\) or a single node \(s\), respectively. While inspired by earlier barrier-based approaches, \(\mathrm{\small BS-DFS}\) warrants independent presentation and analysis through the notion of edge-consistency, a local invariant that forms the basis of its correctness proof. \(\mathrm{\small BS-DFS}\) is an output-sensitive algorithm achieving \(O(k(n+m))\) delay with small constant factors. In our experiments, it produced the complete output at a total runtime within a factor of about \(1.5\) of the incomplete \(\mathrm{\small BC-DFS}\).
We also present and discuss edge-consistent variants of \(\mathrm{\small BS-DFS}\), varying in how barrier values are maintained, including a lazy variant using dependency lists similar to \(\mathrm{\small CYCLE\_SEARCH}\) and Johnson’s algorithm.
For \(\mathrm{\small BC-DFS}\) [11], [12], we present a new counter-example and identify the underlying defect as a single misplaced guard in \(\mathrm{\small UpdateBarrier}\) that prevents valid barrier relaxations from propagating. We further locate the point at which the published correctness argument breaks down.
These contributions are not only of theoretical interest. Both \(\mathrm{\small BC-DFS}\) and \(\mathrm{\small CYCLE\_SEARCH}\) have already been cited in subsequent work [14], [15] and \(\mathrm{\small CYCLE\_SEARCH}\) is used in the popular graph library NetworkX [16], [17].
Our experiments on random graphs show that the resulting omissions are not rare edge cases but occur with noticeable frequency in practice. More broadly, the paper illustrates how subtle barrier propagation schemes can be and why correctness arguments based on explicit invariants are essential.
The paper is organized as follows. After fixing terminology in 2 and presenting \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) in 3, we prove soundness (4), establish completeness by introducing edge-consistency (5), and derive the delay bound (6). We then discuss several edge-consistent variants of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) (7), analyze the shortcomings of BC-DFS (8), and report first experimental results (9) before concluding in 10. All source code, counter-examples, and experiments are available online at [18].
A directed graph \(G\) is an ordered pair \(G=(V,E)\), where \(V\) denotes a finite set of nodes and \(E \subseteq V \times V\) denotes a set of ordered pairs of nodes \((u,v)\), the edges of \(G\). Let \(n=|V|\) and \(m=|E|\) denote the number of nodes and edges of \(G\), respectively. Throughout this paper, all graphs are directed and simple, i.e., they contain neither self-loops (\((u,u) \notin E\)) nor multiple edges.
For an edge \((u,v) \in E\), node \(u\) is a predecessor of \(v\) and \(v\) is a successor of \(u\). The sets of predecessors and successors of a node \(v\) are denoted by \(\mathop{\mathrm{\mathrm{pred}}}(v)\) and \(\mathop{\mathrm{\mathrm{succ}}}(v)\), respectively. The edge \((u,v) \in E\) is said to be outgoing from \(u\) and incoming to \(v\).
A path in \(G\) is a sequence of nodes \(P=(v_0,v_1,\ldots,v_l)\) such that \((v_i,v_{i+1}) \in E\) for all \(0 \le i < l\). When a path \(P\) begins at a node \(x\) (\(v_{0}=x\)) and ends at a node \(y\) (\(v_{l}=y\)), it is called an \(x\)-\(y\)-path. The length of a path is the number of edges it contains, \(\|P\| = l\). A simple path is a path in which all nodes are pairwise distinct. A simple cycle is a node sequence \(C=(v_{0}, v_{1}, \dots, v_{l})\) with \(l \ge 2\), \((v_{0}, v_{1}, \dots, v_{l-1})\) is a simple path, and \(v_{l} = v_{0}\). Two such sequences represent the same simple cycle if one is a cyclic rotation of the other, i.e. \((v_0,\dots,v_l)\) and \((v_0',\dots,v_l')\) agree up to the choice of starting node; a cycle is thus determined by its cyclic sequence of edges, independently of which of its nodes is written first. A simple cycle containing node \(s\) is called a simple \(s\)-cycle. The length of a cycle is the number of edges it contains, \(\|C\| = l\). When appropriate, a path or cycle is identified with the set of nodes it contains.
For a path \(P=(v_{0}, v_{1}, \dots, v_{l})\) and a node \(v\) with \((v_l, v) \in E\), we write \(Pv\) for the path obtained by appending \(v\) to \(P\); iterating, \(Pvw\) appends first \(v\), then \(w\). The dot \(\cdot\) is reserved for concatenating two paths, as in \(P_1 \cdot P_2\).
Definition 1 (Relative Distance). Let \(S \subseteq V\) be a set of nodes, then \[dist_S(x,y) = \begin{cases} \min(\|P\|): & \text{P is an x-y-path in G and P \cap S \subseteq \{x, y\},} \\ \infty: & \text{if no such path exists}. \end{cases}\] The quantity \(dist_S(x,y)\) is the length of a shortest path from \(x\) to \(y\) among all paths which may intersect \(S\) only at the endpoints \(x\) and \(y\). Note that \(dist_\emptyset(x,y)\) is the ordinary edge distance \(dist(x,y)\) in \(G\). All distances are taken in the graph \(G\) unless stated otherwise; where the ambient graph is ambiguous, we indicate it by a superscript, as in \(dist^{G'}_S(x,y)\).
The relative distance provides a triangle inequality in the following sense:
Lemma 1 (Triangle Inequality). Let \(S \subseteq V\) be a set of nodes. For any nodes \(x, z \in V\) and any intermediate node \(y \in V \setminus S\), \[dist_S(x,z) \;\le\; dist_S(x,y) + dist_S(y,z).\]
Proof. If either term on the right is \(\infty\) the bound is trivial. Otherwise, let path \(P_1\) realize \(dist_S(x,y)\) and path \(P_2\) realize \(dist_S(y,z)\). The concatenation \(P_1 \cdot P_2\) is an admissible \(x\)-\(z\)-path: its nodes meet \(S\) only within \((\{x,y\} \cup \{y,z\}) \cap S = \{x,z\} \cap S\) because \(y \notin S\). Hence, the minimum \(dist_S(x,z)\) over all admissible paths satisfies \(dist_S(x,z) \le \|P_1\| + \|P_2\| = dist_S(x,y) + dist_S(y,z)\). ◻
Throughout, we assume \(0 < k \le n\) and \(s \ne t\) for finding all length \(k\) bound simple \(s\)-\(t\)-paths in the directed graph \(G\). The upper bound \(k \le n\) is without loss of generality: a simple \(s\)-\(t\)-path has length at most \(n - 1\); the value \(k = n\) is retained to cover simple cycle search, where a cycle through \(s\) may have length up to \(n\).
We give a short overview of the algorithm. All details will be elaborated upon and proven in later sections. After initialization, \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\) sets the search-path stack \(S\) empty and calls \(\mathop{\mathrm{\mathrm{\small Search}}}(s)\), starting the recursive depth-first exploration of \(G\). A call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) (2) appends its node \(v\) to \(S\) (line 2), so that during the call \(S = (s = v_0, v_1, \dots, v_h = v)\) is the current search path, of length \(h = \|S\|\) (line 3); it mirrors the \(\mathop{\mathrm{\mathrm{\small Search}}}\) call stack. We name a call by its current node, \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\); in the prose we write \(P\) for the contents of \(S\) at entry (the prefix, before \(v\) is appended), \(Pv = P \cdot v\) for the search path while the call is active, and \(Pvw\) for the search path of the child call on a successor \(w\). These are snapshots of the single stack \(S\) at successive moments. The successors \(w\) of \(v\) are examined (line 5), each guarded by a pruning condition \(b[w] + h < k\) (line 6) to avoid excessive fruitless searches. When a successor equals the target (\(w = t\)), the path \(S \cdot t\) is output and \(sd\) (“shortest distance”) is set to \(1\) (lines 8–9); otherwise a recursive search \(\mathop{\mathrm{\mathrm{\small Search}}}(w)\) is performed at the successor \(w\) (line 11). During the for-loop, \(sd\) tracks the shortest path length to \(t\) found via an edge to \(t\) or in any child search (line 12). After the for-loop, \(sd \le k\) marks the fruitful case (line 13), in which output was produced, and \(sd = k + 1\) the fruitless case (line 15). In the fruitful case, \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v, sd)\) (3) assigns \(b[v] \gets sd\) and propagates distance values \(d\) backwards to predecessors in a breadth-first cascade; in the fruitless case, \(b[v] \gets k - h + 1\) (line 16). Finally, \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) pops \(v\) from \(S\) (line 17), restoring the prefix, and returns \(sd\) (line 18).
The algorithm maintains the current search path in a single stack \(S\), appending a node upon entry to \(\mathop{\mathrm{\mathrm{\small Search}}}\) and removing it immediately before returning. By augmenting the stack with an auxiliary boolean on-stack flag for each node, both stack operations and the membership tests — \(w \notin S\) in \(\mathop{\mathrm{\mathrm{\small Search}}}\) and \(p \notin S\) in \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\) — can be performed in \(O(1)\) time. The resulting space requirement is \(O(n+m)\).
The procedure \(\mathop{\mathrm{\mathrm{\small Search}}}\) is formulated in an edge-oriented manner. This leads to the following reduction.
Lemma 2 (Cycle Reduction). Let \(G'=(V',E')\) with \(V' = (V\setminus\{s\}) \cup \{s_o, s_i\}\), where every edge \((s, v)\) of \(G\) becomes \((s_o, v)\), every edge \((u, s)\) becomes \((u, s_i)\), and all edges not incident to \(s\) are kept unchanged.
Then \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, s, k)\) and \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G', s_o, s_i, k)\) produce the same output. In particular, \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, s, k)\) enumerates exactly all simple \(s\)-cycles of length \(\le k\) in \(G\).
Proof. The initial call \(\mathop{\mathrm{\mathrm{\small Search}}}(s)\) explores only the outgoing edges \((s,w) \in E\) of the source, while the target test \(w=t\) recognizes only the incoming edges \((v,t)\in E\) of the target. Thus, under the correspondence \(s \leftrightarrow s_o\) and \(t \leftrightarrow s_i\), the two executions \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, s, k)\) and \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G', s_o, s_i, k)\) coincide step by step. The single barrier \(b[s]\) of \(G\) serves as both \(b[s_o]\) and \(b[s_i]\) of \(G'\), but, because of [obs:source-barrier] () and [obs:target-barrier] (), this is benign. Thus, \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, s, k)\) yields exactly the simple \(s\)-cycles of length \(\le k\) in \(G\). ◻
Enumerating all simple cycles of length at most \(k\) in \(G=(V,E)\) — not only those through a fixed node — reduces to the single-node case by a pre-processing step. Order the nodes as \(V = \{v_1, v_2, \dots, v_n\}\) and let \(G^i\) denote the subgraph of \(G\) induced by \(V^i = \{v_i, v_{i+1}, \dots, v_n\}\). Every simple cycle \(C\) of length \(\le k\) occurs in exactly one of these graphs as a cycle through the distinguished node, namely in \(G^i\) for the smallest index \(i\) among the nodes of \(C\).
Preprocessing creates a list \(L\) of all indices \(i\) where \(G^i\) contains at least one simple \(v_i\)-cycle of length \(k\) or less. For each graph \(G^i\), this can be decided by a distance-limited breadth-first search from \(v_i\), testing if any predecessor of \(v_i\) can be reached within distance \(k-1\). This takes \(O(n+m)\) time per graph and the total pre-processing time is \(O(n(n+m))\). After pre-processing, for all \(v_i \in L\), \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G^i, v_i, v_i, k)\) is executed, producing all simple cycles in \(G\) of length \(\le k\).
Further pre-processing is common for reducing the practical runtime [3], [10], [12]: reducing \(G^i\) to the strongly connected component containing \(v_i\), or removing nodes \(x\) with \(dist^{G^i}(v_i, x) + dist^{G^i}(x, v_i) > k\), which cannot lie on any qualifying cycle.
In the remainder of the paper we focus on the path-search setting and, unless stated otherwise, assume that \(s \neq t\). The assumption is not restrictive: the case \(s = t\) is covered verbatim by 2 (), and it lets us state path-avoidance conditions without endpoint exemptions.
The following elementary observations capture structural properties and invariants of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) that will be used repeatedly in the correctness proofs. Their proofs are straightforward and are therefore omitted.
Every search path is simple.
Every output path is a simple \(s\)-\(t\)-path.
Every search path occurs at most once.
No output path is produced more than once.
Every return value \(sd\) is non-negative.
During a call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\), the barrier value \(b[v]\) can be modified only by that call’s final assignment.
For the source, \(b[s]=0\) remains during execution until the final assignment of the initial call.
For the target, \(b[t]=0\) remains throughout the execution, except in the case \(s=t\) where [obs:source-barrier] applies.
In \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\), every cascade assignment strictly decreases the barrier value of the updated node.
In this section we show that every output produced by \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\) is a simple \(s\)-\(t\)-path of length \(\le k\) in \(G\).
Lemma 3 (Parent Pruning Guard). During \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\), every call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) with search path \(Pv\) satisfies at entry \[b[v] \le k - h, \qquad h = \|Pv\|.\]
Proof. By induction over the search-path length \(h\). Base case (\(h = 0\)): \(v = s\). By Observation [obs:source-barrier] \(b[s] = 0 \le k\) at entry.
Inductive step: \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) with search path \(Pv\) is invoked from some parent call \(\mathop{\mathrm{\mathrm{\small Search}}}(u)\) with search path \(P = P' \cdot u\) of length \(\|P\| = h - 1\). The recursion is reached only when the parent’s pruning condition holds for \(v\): \(b[v] + (h-1) < k\), i.e.\(b[v] < k - h + 1\), hence \(b[v] \le k - h\). ◻
Lemma 4 (Barrier non-negative). During \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\) holds
\(b[x] \ge 0\) for all \(x \in V\),
after initialization, only strictly positive values are assigned.
Proof. We argue by induction over the sequence of assignments to entries of \(b\); recall that no assignment changes \(b[v]\) while \(v\) is on the search path (Observation [obs:path-barrier-fixed]).
Initialization: \(b[x] \gets 0\) for all \(x \in V\).
Fruitful assignment \(b[v] \gets sd\): the value \(sd\) is either \(1\), set when an edge to \(t\) is found, or \(d + 1\) for some child return value \(d \ge 0\) (Observation [obs:return-value]); in either case \(sd \ge 1\).
Fruitless assignment \(b[v] \gets k - h + 1\): by the inductive hypothesis and 3 (), at entry \(0 \le b_{entry}[v] \le k - h\), so the assigned value \(k - h + 1 > k - h \ge 0\).
Cascade assignment \(b[p] \gets d + 1\): the cascade starts from \((v, sd)\) with \(sd \ge 1\) (case 2), and each enqueued pair carries a strictly larger value than its dequeued \((q, d)\); so every assigned \(d + 1 \ge 2 > 0\).
In any case but initialization, a strictly positive value is assigned. ◻
Lemma 5 (Search Path Length). In \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\), every call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) has search-path length \(h = \|Pv\|\) with \(0 \le h \le k\).
Lemma 6 (Termination). The algorithm \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G,s,t,k)\) always terminates.
Proof. We consider all places where loops or recursion occur.
For-loops. In each call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) the for-loop iterates once over the finite set \(\mathop{\mathrm{\mathrm{succ}}}(v)\), and no successor is reconsidered; likewise each step of the \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\) cascade iterates once over \(\mathop{\mathrm{\mathrm{pred}}}(q)\) for the dequeued node \(q\). Thus, every for-loop is finite.
Search recursion. By Observation [obs:simple-search-path] the search path is always simple, and by Observation [obs:search-path-uniqueness] each simple path occurs at most once. Since a finite graph has finitely many simple paths, only finitely many recursive calls \(\mathop{\mathrm{\mathrm{\small Search}}}(\cdot)\) occur.
Cascade. Each assignment \(b[p] \gets d + 1\) in \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\) strictly decreases the potential \(\sum_{x \in V} b[x]\) (the guard ensured \(b[p] > d + 1\)), which by 4 () is bounded below by \(0\); so only finitely many assignments occur. As a pair is enqueued only together with such an assignment, the queue is emptied after finitely many steps.
Since the cascades, the search recursion, and all for-loops are finite, the entire execution of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G,s,t,k)\) is finite. ◻
Summarizing all above claims, we conclude that the algorithm produces only valid output (soundness):
Theorem 1 (\(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) Soundness). Every path produced by \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\) is a simple \(s\)-\(t\)-path in \(G\) of length \(\le k\).
Proof. Output is produced in a call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) when a successor \(w = t\) passes the pruning condition; the output is \(Pv \cdot t\), which by Observation [obs:simple-output] is a simple \(s\)-\(t\)-path in \(G\). Its length is \(\|Pv\| + 1 = h + 1\); the pruning condition \(b[t] + h < k\) held, and \(b[t] = 0\) by Observation [obs:target-barrier], so \(h < k\) and the length is at most \(k\). By 6 (), \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\) is finite. ◻
We close this section by stating two corollaries.
Corollary 1 (Fruitful Return). If a call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) returns a fruitful value \(sd \le k\), then in fact \(sd \le k - h\), where \(h = \|Pv\|\).
Proof. By induction on the search recursion, well-founded by 6 ().
Base case: a successor \(w = t\) passes the pruning condition \(b[t] + h < k\) in \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\), so \(sd \gets 1\) is executed and the returned value satisfies \(sd \le 1\). Since \(b[t] = 0\) by 4 (), the pruning condition gives \(h < k\), hence \(sd \le 1 \le k - h\).
Inductive step: no successor \(w = t\) passes the pruning condition; then the fruitful value \(sd\) is set by a recursive call. At least one child returned a fruitful value \(d\); let \(w\) be a child achieving the minimum such \(d\). Its search path has length \(h + 1\), so by the inductive hypothesis \(d \le k - (h+1)\). In \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) we set \(sd = d + 1\), hence \(sd \le k - h\). ◻
Corollary 2 (Barrier Upper Bound). Throughout the execution of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G,s,t,k)\), \[0 \le b[x] \le k \quad \text{for all } x \in V,\] except that a completely fruitless run sets \(b[s] = k+1\) as its last action. Thus, \(k+1\) is a sentinel value, strictly above every barrier value that is ever read.
Proof. The lower bound is 4 (). For the upper bound we induct over the sequence of assignments to \(b\), showing each assigned value is \(\le k\) apart from the stated exception.
Initialization: \(b[x] \gets 0 \le k\).
Fruitful assignment: \(b[v] \gets sd \le k - h \le k\) by 1 ().
Fruitless assignment \(b[v] \gets k - h + 1\): for \(h \ge 1\) this is \(\le k\); for \(h = 0\), i.e.\(v = s\), it is \(k+1\), which occurs only when the initial call \(\mathop{\mathrm{\mathrm{\small Search}}}(s)\) is fruitless and is then the algorithm’s last action.
Cascade assignment \(b[p] \gets d + 1\): The upper bound follows from the inductive hypothesis and Observation [obs:cascade-lowers]
Hence every value is \(\le k\) except the terminal \(b[s] = k+1\); as that assignment is the algorithm’s last action, every barrier read during the execution sees a value \(\le k\). ◻
In this section we prove the completeness of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G,s,t,k)\), namely that it produces every simple \(s\)-\(t\)-path in \(G\) of length at most \(k\). The proof is based on a graph-local property of the barrier values, called edge-consistent labelling. We first introduce this property and establish its basic consequences. We then show that it is maintained throughout the execution of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\), and finally use it to prove completeness.
The following discussion is naturally interpreted through the framework of heuristic search. The barrier value \(b[x]\) may be viewed as an estimate of the remaining distance from \(x\) to the target \(t\), while the search-path length \(h\) represents the cost already incurred. In the terminology of \(A^*\)-search [19], \(h\) plays the role of the \(g\)-value and \(b[x]\) the role of a heuristic estimate. The pruning condition \(b[w] + h < k\) is then \(f\)-value pruning against a budget: a successor is explored only when the estimated total cost \(g + h\) stays below \(k\). The edge-consistent labelling is precisely the consistency (monotonicity) condition \(h(x) \le w(x,y) + h(y)\) of \(A^*\), with unit edge weights \(w \equiv 1\) and required only for edges whose two endpoints lie outside the current search path.
The completeness argument then follows the classical pattern. Consistency implies admissibility: the barrier never overestimates the true remaining distance to the target. We shall show that \(b[x]\le dist_S(x,t)\), where \(S\) is the current search path. Consequently, whenever a simple \(s\)-\(t\)-path of length at most \(k\) exists through a successor, the pruning condition cannot exclude that successor. Every feasible path therefore survives all pruning tests and is eventually generated.
The principal difference from classical heuristic search is that the heuristic is not fixed. In \(A^*\), consistency is a static property verified once for a given heuristic. In contrast, the barrier values of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) are continually modified during the search: fruitless returns raise barriers, while update cascades may lower them. Consistency is therefore not a precondition but an invariant that must be preserved under every state update. Establishing this invariant constitutes the main technical component of the completeness proof. In this respect \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) is closer to learning real-time \(A^*\) [20], where the heuristic is likewise refined as the search proceeds, than to the static algorithm.
Definition 2 (Edge-Consistent Labelling).
Let \(G=(V,E)\) be a directed graph and let \(S\subseteq V\). A function \(b:V\rightarrow\mathbb{N}_0\) is an edge-consistent labelling with respect to \(S\)* if \[b[x]\le b[y]+1\] for every edge \((x,y)\in E\) satisfying \(\{x,y\}\cap S=\emptyset\).*
Lemma 7 (Barrier Distance Bound). Let \(G=(V,E)\) be a directed graph, \(S \subseteq V\), and \(b: V \rightarrow \mathbb{N}_0\) an edge-consistent labelling w.r.t.\(S\). Then \[b[x] \le b[y] + l \quad \text{for every x-y-path P of length l in G with P \cap S = \emptyset;}\] in particular, \(b[x] - b[y] \le dist_S(x,y)\) for all \(x, y \in V \setminus S\).
Proof. By induction on \(l\). For \(l = 0\), \(x = y\) and the claim holds. In the inductive step, let \((z,y) \in E\) be the last edge of the path. The induction hypothesis applied to the prefix up to \(z\) gives \(b[x] \le b[z] + l - 1\), and 2 () gives \(b[z] \le b[y] + 1\); substitution yields \(b[x] \le b[y] + l\). The distance bound follows by taking a shortest \(x\)-\(y\)-path avoiding \(S\) (trivially when \(dist_S(x,y) = \infty\)). ◻
Specialized to \(y = t\) with \(b[t] = 0\), the distance bound reads \(b[x] \le dist_S(x,t)\): the barrier never overestimates the true remaining distance — admissibility in the sense of \(A^*\). What makes the analysis nontrivial is that \(S\) changes during the search, and admissibility is a property of a given \(S\); the remainder of this section tracks how the three kinds of state change — barrier writes, path pushes, and path pops — affect it.
We stress that edge-consistency is sufficient but stronger than necessary: completeness needs only that the barrier be admissible (\(b[x] \le dist_S(x,t)\)) at the moment each successor is tested, which is all 8 () uses. Any labelling that under-estimates the remaining distance at that instant therefore yields completeness, edge-consistent or not; we maintain the stronger, local edge-consistency only because it implies admissibility incrementally across the search’s writes, pushes, and pops.
Lemma 8 (Pruning is Permissive). Let \(b\) be edge-consistent with respect to a set \(S\), with \(b[t] = 0\), and let \(P = (v_0, \dots, v_h, v_{h+1}, \dots, v_l = t)\) be a simple path of length \(l \le k\) ending at \(t\) whose prefix has node set \(S = \{v_0, \dots, v_h\}\). Then \(b[v_{h+1}] + h < k\).
Proof. Since \(P\) is simple, the suffix \((v_{h+1}, \dots, v_l = t)\) avoids \(S = \{v_0, \dots, v_h\}\) and witnesses \(dist_S(v_{h+1}, t) \le l - h - 1\). By 7 () and \(b[t] = 0\), \(b[v_{h+1}] \le l - h - 1\), hence \(b[v_{h+1}] + h \le l - 1 < l \le k\). ◻
The following lemmas characterize how a single search call affects the barrier values. A fruitless call can only increase its own barrier (9), and while a call remains fruitless no barrier value decreases anywhere in its recursion subtree (10). Conversely, a fruitful call returns a value that is at least the true distance to the target (11), and the ensuing update cascade assigns barrier values that are likewise lower bounded by the corresponding distances to \(t\) (12). The complementary upper bounds, which together imply that cascade updates coincide with the exact distances, are established in 5.3.
Recall from 3 that during a call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) (2) the search path is the current stack snapshot \(Pv=(s=v_0,\ldots,v_h=v)\) where \(h = \|Pv\|\), and that \(P\) denotes the prefix of this path at the time the call is entered. Since Observation [obs:target-barrier] shows that \(b[t]=0\) throughout the execution, every lemma below may assume this property without further mention.
Lemma 9 (Fruitless Increasing). Suppose in \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\) a call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) returns fruitless. Then, for the barrier value of \(v\) at entry \(b_{entry}[v]\) and at exit \(b_{exit}[v]\), \(b_{exit}[v] > b_{entry}[v]\).
Proof. By 3 (), \(b_{entry}[v] \le k - h\) at entry, where \(h = \|Pv\|\). A fruitless return executes the assignment \(b[v] \gets k - h + 1\), which by Observation [obs:path-barrier-fixed] is the only write to \(b[v]\) during \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\); hence \(b_{exit}[v] = k - h + 1 > k - h \ge b_{entry}[v]\). ◻
Lemma 10 (Fruitless Monotonicity). If \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) returns fruitless, then no call nested within \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) returns fruitful, no execution of \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\) occurs during \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\), and every barrier value is non-decreasing throughout the execution of \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\).
Proof. Suppose that some call nested within \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) returns a fruitful value. By Corollary 1, a fruitful call at depth \(h'\) returns a value at most \(k-h'\). Its parent therefore computes
\[sd \le (k-h')+1 = k-(h'-1)\le k,\] and is itself fruitful. Repeating the argument up the recursion stack shows that \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) must also be fruitful, contradicting the assumption. Therefore, no nested search call is fruitful. Since the procedure \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\) is invoked only after a fruitful return, no cascade execution can occur within \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\). The only barrier updates performed during \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) are therefore fruitless assignments, either by \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) itself or by calls nested within it. By 9 (), each such update strictly increases the corresponding barrier value. Consequently, every barrier value is non-decreasing throughout the execution of \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\). ◻
Lemma 11 (Fruitful Lower Bound). If a call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) with search path \(Pv\) returns a fruitful value \(sd\), then
\[sd \ge dist_{Pv}(v,t).\]
Proof. We proceed by induction on the search recursion, which is well-founded by 6 (). A fruitful value \(sd\) is obtained in one of two ways. If an edge \((v,t)\) is discovered, then \(sd=1\). Since such an edge yields a path of length one, \(dist_{Pv}(v,t)\le 1 = sd\). Otherwise, \(sd=d_w+1\) for some successor \(w\notin Pv\) whose recursive call \(\mathop{\mathrm{\mathrm{\small Search}}}(w)\) returns the minimum fruitful value \(d_w\) encountered by the loop. By the induction hypothesis, \(d_w \ge dist_{Pvw}(w,t)\). Since \(w\) is exempt as an endpoint, \(dist_{Pvw}(w,t)=dist_{Pv}(w,t)\). Furthermore, \(dist_{Pv}(v,w)\le 1\). Applying 1 () to the intermediate node \(w\notin Pv\) gives \[dist_{Pv}(v,t) \le dist_{Pv}(v,w)+dist_{Pv}(w,t) \le 1+d_w = sd.\] ◻
Lemma 12 (Fruitful Distance Lower Bound). Let the cascade \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v, sd)\) be invoked from a fruitful \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) with search path \(Pv\), prefix \(P\). Then every assignment \(b[u] \gets d+1\) performed by the cascade satisfies \(b[u] \ge dist_P(u,t)\).
Proof. The cascade does not modify the search path; \(P\) and \(Pv\) are fixed throughout. We show by induction on enqueue order that every pair \((q,d)\) placed on the queue satisfies \(d \ge dist_P(q,t)\). Since each assignment \(b[u] \gets d+1\) is accompanied by enqueuing \((u, d+1)\), the claim follows.
The initial pair is \((v, sd)\). By 11 (), \(sd \ge dist_{Pv}(v,t)\), and since \(v\) is endpoint-exempt, \(dist_{Pv}(v,t) = dist_P(v,t)\).
Every later pair \((u, d+1)\) is enqueued while an earlier pair \((q,d)\) with \(u \in \mathop{\mathrm{\mathrm{pred}}}(q)\) is processed; by the induction hypothesis, \(d \ge dist_P(q,t)\). The intermediate node \(q\) lies off \(P\): either \(q = v \notin P\), or \(q\) passed the guard \(q \notin S\) when enqueued, and \(S = Pv \supseteq P\) throughout the cascade. Hence, 1 () on the edge \((u,q)\) gives \(dist_P(u,t) \le 1 + dist_P(q,t) \le d + 1 = b[u]\). ◻
Lemma 13 (Cascade Distance). Suppose the cascade \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v,sd)\) is initiated by a \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) call whose search path is \(Pv\), and assume that the barrier labelling is edge-consistent with respect to \(Pv\) at cascade entry. Then, at cascade exit, \[b[x] \le sd + dist_{Pv}(x,v) \quad \text{for every } x \notin Pv,\] with equality for every node that was enqueued by the cascade.
Proof. By Observation [obs:cascade-lowers], the cascade only decreases barrier values and, because nodes are processed in FIFO order, each node is relaxed at most once.
Upper bound. We prove \(b[x] \le sd + dist_{Pv}(x,v)\) for every \(x \notin P\) by induction on \(r = dist_{Pv}(x,v).\) The claim is trivial when \(r=\infty\). For \(r=0\), we have \(x=v\), and the cascade initializes \(b[v]=sd\).
For \(r \ge 1\) let \(x_1\) be the successor of \(x\) on a shortest \(x\)-\(v\)-path avoiding \(Pv\) except at \(v\), so \(dist_{Pv}(x_1,v) = r-1\) and either \(x_1 = v\) or \(x_1 \notin Pv\); by induction \(b[x_1] \le sd + (r-1)\) at exit. If \(x_1\) is enqueued (in particular if \(x_1 = v\)), then when its pair is dequeued it relaxes \(x \in \mathop{\mathrm{\mathrm{pred}}}(x_1)\), leaving \(b[x] \le b[x_1] + 1 \le sd + r\). If \(x_1\) is never enqueued, \(b[x_1]\) keeps its entry value and entry edge-consistency on the edge \((x, x_1)\) gives \(b_{entry}[x] \le b[x_1] + 1 \le sd + r\); by Observation [obs:cascade-lowers], \(b[x] \le b_{entry}[x] \le sd + r\) at exit.
Lower bound for enqueued nodes. If \(u\) is enqueued, it is relaxed by some dequeued \((q, d)\) with \(u \in \mathop{\mathrm{\mathrm{pred}}}(q)\), setting \(b[u] = d + 1\) where \(d = b[q]\). By induction on dequeue order, \(b[q] \ge sd + dist_{Pv}(q,v)\) (base \(b[v] = sd\)); either \(q = v\), and the edge \((u,v)\) gives \(dist_{Pv}(u,v) \le 1 = 1 + dist_{Pv}(v,v)\); or \(q \notin Pv\), and the edge \((u,q)\) with 1 () gives \(dist_{Pv}(u,v) \le 1 + dist_{Pv}(q,v)\). Thus, \(b[u] = b[q] + 1 \ge sd + dist_{Pv}(u,v)\). With the upper bound, \(b[u] = sd + dist_{Pv}(u,v)\). ◻
We now isolate the only state transition that can violate admissibility. Barrier writes cannot do so: a fruitless or fruitful return modifies the barrier of a node that still lies on the current search path, and admissibility places no restriction on such nodes. Likewise, a cascade only decreases barrier values (Observation [obs:cascade-lowers]), so it cannot raise an admissible value above its distance bound.
A push enlarges the forbidden set, which only relaxes the edge-consistency constraints. The remaining transition is a pop: when \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) removes \(v\) from the search path, the forbidden set shrinks from \(Pv\) to \(P\), and an edge \((x,y)\) is newly constrained w.r.t.\(P\) exactly when \(v \in \{x,y\}\) — removing \(v\) changes the constrained/exempt status of no other edge. Re-establishing edge-consistency at a pop is therefore a local obligation on the edges incident to \(v\). The next lemma discharges the incoming edges and the case \(y = v\); the single family it defers — edges leaving \(v\) — is handled in 18 (), and is the only point where the exact fruitful value is needed.
Lemma 14 (Update Repairs). Under the cascade \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v,sd)\) of 13 (), edge-consistency with respect to \(P\) holds at cascade exit for every edge except, possibly, those leaving \(v\).
Proof. Take an edge \((x, y)\) with \(\{x,y\} \cap P = \emptyset\) and \(x \ne v\); then \(x \notin Pv\), and either \(y = v\) or \(y \notin Pv\). By 13 (), \(b[x] \le sd + dist_{Pv}(x,v)\).
\(y = v\): the edge \((x,v)\) gives \(dist_{Pv}(x,v) \le 1\), so \(b[x] \le sd + 1 = b[v] + 1\).
\(y \notin Pv\) and \(y\) is enqueued: then \(b[y] = sd + dist_{Pv}(y,v)\) by 13 (), and 1 () (\(y \notin Pv\)) with \(dist_{Pv}(x,y) \le 1\) gives \[b[x] \;\le\; sd + dist_{Pv}(x,v) \;\le\; sd + 1 + dist_{Pv}(y,v) \;=\; b[y] + 1.\]
Case \(y\notin Pv\) and \(y\) is not enqueued. Since \(y\) is never enqueued, the cascade never writes to \(b[y]\). Hence \(b[y] = b_{\mathrm{entry}}[y].\) Entry edge-consistency on \((x,y)\) gives \[b_{\mathrm{entry}}[x] \le b_{\mathrm{entry}}[y]+1.\] Since the cascade only lowers barriers, \[b[x] \le b_{\mathrm{entry}}[x] \le b_{\mathrm{entry}}[y]+1 = b[y]+1.\] ◻
It suffices to show that \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) keeps its labelling edge-consistent w.r.t.the path after the pop; completeness then follows. By the preceding subsection the only nontrivial obligation at a pop of \(v\) is on the edges leaving \(v\), and discharging it needs the cascade to have deposited the exact distance — equivalently, that the fruitful return value satisfies \(sd = dist_{Pv}(v,t)\), which in turn needs the shortest completion to have been produced. Completeness, the exact value, and preservation at the pop are thus mutually dependent and are established together, by a single induction on the search recursion, well-founded by 6 ().
For each call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) the induction carries the following clauses:
completeness of the call (15);
the exact fruitful value (16);
global monotonicity (17);
preservation across the call (18).
In each of the four lemmas below the induction hypothesis is that all four claims hold for every call nested strictly within the current \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\). A pruning test that a budget-respecting path must survive is discharged directly by 8 (); no global completeness statement is invoked inside the induction.
Lemma 15 (Call Completeness). Consider a call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) with search path \(Pv = (s = v_0, \dots, v_h = v)\) at which edge-consistency w.r.t.\(P\) holds at entry. Then \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) produces every simple \(s\)-\(t\)-path of length \(\le k\) having \(Pv\) as a prefix.
Proof. We argue within the joint induction on the search recursion; the induction hypothesis supplies all four claims for every call nested strictly within \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\).
On entry \(v\) is pushed, turning \(P\) into \(Pv\); pushing only enlarges the set of exempt nodes, so edge-consistency w.r.t.\(Pv\) holds. Within the for-loop, a successor that is pruned or equals \(t\) writes no barrier, while a recursively searched successor \(w'\) is entered with search path \(Pvw'\) and, by the induction hypothesis (18), preserves edge-consistency w.r.t.\(Pvw' \setminus \{w'\} = Pv\) across the call. Edge-consistency w.r.t.\(Pv\) is therefore maintained throughout the for-loop, and in particular holds whenever a successor is examined.
Let \(R = (s = v_0, \dots, v_h = v, v_{h+1}, \dots, v_l = t)\) be a simple \(s\)-\(t\)-path of length \(l \le k\) with prefix \(Pv\), and let \(w = v_{h+1}\). As \(w \in \mathop{\mathrm{\mathrm{succ}}}(v)\), the for-loop examines it; at that moment edge-consistency w.r.t.\(Pv\) holds and \(b[t] = 0\) (Observation [obs:target-barrier]), so by 8 () \(b[w] + h < k\) and \(w\) is not pruned. If \(w = t\), the closing-edge branch outputs \(Pv\) followed by \(t\), which is \(R\). Otherwise, \(w \ne t\) and, \(R\) being simple, \(w \notin \{v_0, \dots, v_h\} = Pv\); hence \(\mathop{\mathrm{\mathrm{\small Search}}}(w)\) is entered with search path \(Pvw\), at which edge-consistency w.r.t.\(Pv\) holds. Since \(R\) has prefix \(Pvw\), the induction hypothesis (15 for \(\mathop{\mathrm{\mathrm{\small Search}}}(w)\)) yields that \(R\) is produced. ◻
Lemma 16 (Strict Barrier Invariant). Consider a call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) with search path \(Pv = (s = v_0, \dots, v_h = v)\) at which edge-consistency w.r.t.\(P\) holds at entry. If \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) is fruitful, then \(sd = dist_{Pv}(v,t)\).
Proof. Again within the joint induction, with the induction hypothesis available for every nested call. The bound \(sd \ge dist_{Pv}(v,t)\) is 11 (); it remains to show \(sd \le dist_{Pv}(v,t)\).
Being fruitful, \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) has \(sd \le k - h\) (1 ()), so \(dist_{Pv}(v,t) \le sd \le k - h\) is finite. Let \(R = (v, w, \dots, t)\) be a shortest \(v\)-\(t\)-path with \(R \cap Pv \subseteq \{v,t\}\), of length \(dist_{Pv}(v,t)\), and let \(w\) be its node after \(v\). Prepending \(Pv\) yields a simple \(s\)-\(t\)-path of length \(h + dist_{Pv}(v,t) \le k\) with prefix \(Pv\) whose node after \(v\) is \(w\).
After \(v\) is pushed, edge-consistency w.r.t.\(Pv\) holds, and by the induction hypothesis (18) each successor searched before \(w\) preserves it; so it holds when \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) examines \(w\). With \(b[t] = 0\) (Observation [obs:target-barrier]), 8 () gives \(b[w] + h < k\), so \(w\) is not pruned.
If \(w = t\), then \(dist_{Pv}(v,t) = 1\) and the closing-edge branch sets \(sd \gets 1 = dist_{Pv}(v,t)\). Otherwise, \(w \ne t\) and, \(R\) being simple with \(R \cap Pv \subseteq \{v,t\}\), \(w \notin Pv\); so \(\mathop{\mathrm{\mathrm{\small Search}}}(w)\) runs with search path \(Pvw\). The \(s\)-\(t\)-path above has prefix \(Pvw\), so by the induction hypothesis (15 for \(\mathop{\mathrm{\mathrm{\small Search}}}(w)\)) it is produced during \(\mathop{\mathrm{\mathrm{\small Search}}}(w)\), which is therefore fruitful (10 ()); by the induction hypothesis (16 for \(\mathop{\mathrm{\mathrm{\small Search}}}(w)\)) its return value is \(sd_w = dist_{Pvw}(w,t)\). The suffix of \(R\) from \(w\) meets \(Pvw\) only at \(w\) and \(t\) and has length \(dist_{Pv}(v,t) - 1\), so \(dist_{Pvw}(w,t) \le dist_{Pv}(v,t) - 1\). The for-loop sets \(sd \le sd_w + 1 = dist_{Pvw}(w,t) + 1 \le dist_{Pv}(v,t)\).
In both cases \(sd \le dist_{Pv}(v,t)\), hence \(sd = dist_{Pv}(v,t)\). ◻
Lemma 17 (Per-Call Global Monotonicity). Consider a call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) with search path \(Pv = (s = v_0, \dots, v_h = v)\) at which edge-consistency w.r.t.\(P\) holds at entry, with entry barriers \(b_{entry}\) and exit barriers \(b_{exit}\). Then \(b_{exit}[x] \ge b_{entry}[x]\) for every \(x \in V\).
Proof. Within the joint induction; the induction hypothesis holds for every nested call. The execution of \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) writes barriers only through (i) its child calls, (ii) the post-loop assignment at \(v\), and, in the fruitful case, (iii) the cascade \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v, sd)\).
For-loop. On entry \(v\) is pushed and edge-consistency w.r.t.\(Pv\) holds; a recursively searched successor \(w'\) is entered with search path \(Pvw'\) and, by the induction hypothesis (18), preserves edge-consistency w.r.t.\(Pv\) across the call. Each child is thus entered with the invariant and is, by the induction hypothesis (17), globally non-decreasing; chaining over the children in order, \(b[x] \ge b_{entry}[x]\) for every \(x\) when the for-loop completes.
Fruitless case. No cascade runs and the only post-loop write is \(b[v] \gets k - h + 1\), which by 3 () exceeds \(b_{entry}[v] \le k - h\).
Fruitful case. By 7 () at entry (\(v, t \notin Pv \setminus \{v\}\)) with \(b[t] = 0\) (Observation [obs:target-barrier]) \(b_{entry}[v] \le dist_P(v,t) = dist_{Pv}(v,t)\) (dist is unaffected by whether its first argument lies in the forbidden set), and by 11 () the post-loop write is \(b[v] \gets sd \ge dist_{Pv}(v,t)\); so \(b[v]\) does not decrease. The cascade then writes only nodes \(u \notin Pv\), each assignment being \(b[u] \gets d + 1 \ge dist_P(u,t)\) by 12 (), while entry edge-consistency and 7 () give \(b_{entry}[u] \le dist_P(u,t)\). Hence, no node barrier falls below its entry value. ◻
Lemma 18 (Search Preserves). Consider a call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) with search path \(Pv = (s = v_0, \dots, v_h = v)\) at which edge-consistency w.r.t.\(P\) holds at entry. Then, edge-consistency w.r.t.\(P\) holds at exit.
Proof. Within the joint induction; the induction hypothesis holds for every nested call, and 16 () and 17 () are available for \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) itself.
Push and for-loop. On entry \(v\) is pushed, turning \(P\) into \(Pv\); pushing only enlarges the set of exempt nodes, so edge-consistency w.r.t.\(Pv\) holds. A pruned successor and the closing-edge branch write no barrier, while a recursively searched successor \(w'\) is entered with search path \(Pvw'\) and, by the induction hypothesis, preserves edge-consistency w.r.t. \(Pvw' \setminus \{w'\} = Pv\). Hence, edge-consistency w.r.t.\(Pv\) holds when the for-loop completes.
An edge \((x,y)\) is constrained by edge-consistency w.r.t.\(P\) exactly when \(\{x,y\} \cap P = \emptyset\); such edges are of three kinds:
edges with \(v \notin \{x,y\}\);
incoming edges \((x,v)\) with \(x \notin Pv\);
outgoing edges \((v,y)\) with \(y \notin Pv\).
Popping \(v\) writes no barrier, so \(b_{exit}\) denotes the values after the post-loop assignment and, in the fruitful case, after the cascade.
Fruitful case (\(sd \le k\)). The assignment \(b[v] \gets sd\) is made, \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v, sd)\) runs, and \(b_{exit}[v] = sd\) (the cascade does not write \(b[v]\), as \(v \in Pv\) throughout it, Observation [obs:path-barrier-fixed]).
(I) and (II). When the for-loop completes, edge-consistency w.r.t.\(Pv\) holds; \(b[v] \gets sd\) changes only \(b[v]\), affecting only edges incident to \(v\), which are exempt w.r.t.\(Pv\), so edge-consistency w.r.t.\(Pv\) still holds when \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v,sd)\) is invoked. By 14 (), at the cascade’s end edge-consistency w.r.t.\(P\) holds everywhere except possibly on edges leaving \(v\); edges of kind (I) and (II) do not leave \(v\), hence are consistent at exit.
(III). Let \((v,y)\) be an edge with \(y \notin Pv\). If \(y = t\): as \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) is fruitful, \(1 \le sd \le k - h\) (1 ()), so \(h < k\) and the closing edge \((v,t)\) passes its pruning test (\(b[t] + h = h < k\)), firing and setting \(sd \gets 1\); with all return values \(\ge 1\), \(sd = 1\). With \(b[t] = 0\) (Observation [obs:target-barrier]), \(b_{exit}[v] = 1 = b[t] + 1\).
Now let \(y \ne t\). By 16 () and endpoint-exemption, \(sd = dist_{Pv}(v,t) = dist_P(v,t)\). The edge \((v,y)\) gives \(dist_P(v,y) \le 1\), and 1 () (intermediate \(y \notin Pv \setminus \{v\}\)) yields \(sd \le 1 + dist_P(y,t)\), so \(dist_P(y,t) \ge sd - 1\). We show \(b[y] \ge sd - 1\) from the moment the for-loop finishes processing \(y\) until exit.
Base. If \(y\) was pruned, \(b[y] + h < k\) failed, so \(b[y] \ge k - h \ge sd\) (1 ()). If \(y\) was recursively searched, then right after the child \(\mathop{\mathrm{\mathrm{\small Search}}}(y)\) (depth \(h+1\)) returns, \(b[y] = k - h \ge sd\) if that child was fruitless, or \(b[y] = sd_y\) if it was fruitful, where \(sd \le sd_y + 1\) (the for-loop minimization), so \(b[y] = sd_y \ge sd - 1\). In all cases \(b[y] \ge sd - 1\) when the for-loop finishes with \(y\).
Preservation. After the for-loop finishes processing \(y\), every further write to \(b[y]\) occurs either within a later child call of \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) or in the post-loop cascade \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v, sd)\); in particular, a cascade \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(z, sd_z)\) with \(z\) a strict descendant of \(v\) runs entirely within the child subtree containing \(z\). Each later child is entered with edge-consistency w.r.t.\(Pv\) (as above) and is, by the induction hypothesis (17), globally non-decreasing, so \(b[y] \ge sd - 1\) persists through the end of the for-loop. The post-loop cascade writes \(b[y] \gets d + 1 \ge dist_P(y,t) \ge sd - 1\) by 12 (). Hence, \(b_{exit}[y] \ge sd - 1\), i.e.\(b_{exit}[v] = sd \le b_{exit}[y] + 1\).
Fruitless case (\(sd = k + 1\)). Then \(b_{exit}[v] = k - h + 1\), and by 10 () no cascade runs within \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) and every barrier is non-decreasing throughout it.
(I). When the for-loop completes, edge-consistency w.r.t.\(Pv\) holds; \(b[v] \gets k - h + 1\) changes only \(b[v]\), so every edge \((x,y)\) with \(v \notin \{x,y\}\) and \(\{x,y\} \cap Pv = \emptyset\) keeps \(b[x] \le b[y] + 1\), and for such edges \(\{x,y\} \cap Pv = \emptyset\) coincides with \(\{x,y\} \cap P = \emptyset\).
(II). Let \((x,v)\) be an edge with \(x \notin Pv\). At entry it is constrained w.r.t.\(P\), so \(b_{entry}[x] \le b_{entry}[v] + 1 \le (k - h) + 1\) (3 ()). During \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\), \(b[x]\) changes only through a fruitless \(\mathop{\mathrm{\mathrm{\small Search}}}(x)\) nested within it (depth \(h_x \ge h + 1\), assigning \(b[x] \gets k - h_x + 1 \le k - h\)); so \(b[x]\) never exceeds \(k - h + 1\), giving \(b_{exit}[x] \le k - h + 1 = b_{exit}[v] \le b_{exit}[v] + 1\).
(III). Let \((v,y)\) be an edge with \(y \notin Pv\); we show \(b_{exit}[y] \ge k - h\), which gives \(b_{exit}[v] = k - h + 1 \le b_{exit}[y] + 1\). In the for-loop \(y\) was pruned or searched. If pruned, \(b[y] + h < k\) failed, so \(b[y] \ge k - h\). If searched, the child \(\mathop{\mathrm{\mathrm{\small Search}}}(y)\) has depth \(h + 1\) and, being fruitless, assigns \(b[y] \gets k - (h+1) + 1 = k - h\). Either way \(b[y] \ge k - h\) at some point, and since barriers are non-decreasing, \(b_{exit}[y] \ge k - h\).
In all cases edge-consistency w.r.t.\(P\) holds at exit. ◻
We have seen that edge-consistency w.r.t.the current search path holds throughout the execution of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G,s,t,k)\). This is the global reading of 18 (): starting from \(b \equiv 0\) (edge-consistent w.r.t.the empty path), the single call \(\mathop{\mathrm{\mathrm{\small Search}}}(s)\) is entered with the invariant, and the lemma shows each call preserves it w.r.t. the path after its node is popped; chaining over the call tree gives the invariant at every point. We close with the main theorems in this section.
Theorem 2 (\(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) Completeness). The algorithm \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\) produces every simple \(s\)-\(t\)-path of length \(\le k\) in \(G\).
Proof. The initial call \(\mathop{\mathrm{\mathrm{\small Search}}}(s)\) has search path \((s)\) and is entered with the labelling \(b \equiv 0\), edge-consistent w.r.t.\((s) \setminus \{s\} = \emptyset\). Every simple \(s\)-\(t\)-path of length \(\le k\) has \((s)\) as a prefix, so by 15 () it is produced by \(\mathop{\mathrm{\mathrm{\small Search}}}(s)\). ◻
For delay analysis, the entire \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G,s,t,k)\) execution is partitioned into a sequence of intervals. A new interval starts when the algorithm begins or whenever output is produced. An interval ends with the next output or when the algorithm terminates.
Let the delay of an interval be the number of elementary steps executed by the algorithm in that interval. We will show that for a graph \(G\) with \(n\) nodes and \(m\) edges and a given length bound \(k \in \mathbb{N}^+\), the maximum delay of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G,s,t,k)\) is bounded by \(O(k(n+m))\). Before doing so, we will analyze the execution of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) within an interval in greater detail, see also 4.
We index the intervals \(\tau = 1, 2, \dots\) in order of occurrence. The output path opening interval \(\tau\) is called its spine, denoted \(S_\tau = (s = v_0, v_1, \dots, v_l = t)\). The first interval is opened by the start of the execution rather than by an output; we set \(S_1 = \emptyset\). Symmetrically, the execution’s end closes the terminal interval \(T\) without an output; we set \(S_{T+1} = \emptyset\). Sums indexed by an empty spine are zero.
When \(v_l = t\) is reached, the spine path is output. Next, the \(\mathop{\mathrm{\mathrm{\small Search}}}\) call stack unwinds one level, leaving \(v_{l-1}\) on top. \(\mathop{\mathrm{\mathrm{\small Search}}}(v_{l-1})\) continues enumerating the successors of \(v_{l-1}\) after \(v_l\) in the successor list and recurses into those that pass the pruning condition. If one such sibling search returns fruitful, the next \(s\)-\(t\)-path was produced during that search and the output immediately starts the next interval, before the fruitful sibling search returns. Otherwise, all sibling searches at \(v_{l-1}\) return fruitless. Since \(\mathop{\mathrm{\mathrm{\small Search}}}(v_{l-1})\) itself is fruitful (it produced \(v_l\) on the spine), \(b[v_{l-1}]\) is assigned and the cascade \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v_{l-1}, sd)\) runs. The stack then unwinds to \(v_{l-2}\) and the procedure repeats.
This continues until either (a) at some spine level \(v_j\) a sibling search \(\mathop{\mathrm{\mathrm{\small Search}}}(q)\) returns fruitful, producing the next \(s\)-\(t\)-path \(S_{\tau+1} = (v_0, \dots, v_j, q, \dots, t)\); or (b) the unwinding exhausts level \(v_0 = s\) and the algorithm terminates. In case (a), the spine node \(v_j\) is the deepest stack level that remains continuously occupied across the two outputs; we call it the lowest common ancestor (LCA) of \(S_\tau\) and \(S_{\tau+1}\). The spine prefix \((v_0, \dots, v_j)\) is shared between the two paths; the suffixes \((v_{j+1}, \dots, v_l)\) and \((q, \dots, t)\) are disjoint.
4 additionally depicts a deeper spine node \(v_i\) whose cascade \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v_i, sd)\) deposits a barrier value \(b[x]\) at some node \(x\) off the spine; the witness path \(W\) from \(x\) via \(v_i\) to \(t\) plays a central role in the interval-ending argument below.
Consider the sequence of barrier assignments in an interval. For a node \(x\), we classify the assignments to \(b[x]\):
S-event: \(b[x] \gets k - h + 1\), assigned in a fruitless \(\mathop{\mathrm{\mathrm{\small Search}}}(x)\);
F-event: \(b[x] \gets sd\), the origin write at the start of a cascade \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(x, sd)\) invoked from a fruitful \(\mathop{\mathrm{\mathrm{\small Search}}}(x)\).
U-event: \(b[x] \gets d + 1\), the predecessor write inside some cascade call \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(q, d)\) with \(q \in \mathop{\mathrm{\mathrm{succ}}}(x)\), under the guard \(b[x] > d + 1\);
There are no other types of events, and no other function call during \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\) visits a node \(x\) without assigning \(b[x]\).
Note that there is at most one F-event per node per interval, namely when \(\mathop{\mathrm{\mathrm{\small Search}}}(v_i)\) at a spine node \(v_i\) returns fruitful.
We consider the sequence of S- and U-events occurring in an interval and divide it into one or more homogeneous blocks of events of the same type, separated by event-type transitions. Note that the order of events, due to recursion, can differ from the function-call order, since the barriers are written in postfix order before return.
Lemma 19 (S-Event Bound). Every S-block at a node \(x \ne s\) contains at most \(k\) events. At \(x = s\), every S-block contains at most one event.
Proof. By 9 (), each S-event at \(x\) strictly increases \(b[x]\). By 4 ()(2), each assigned value is at least \(1\), and by 2 (), \(b[x] \le k + 1\) with \(b[x] = k + 1\) only for \(x = s\).
For \(x \ne s\), the assigned values lie in \(\{1, 2, \dots, k\}\), so a strictly increasing chain of S-events at \(x\) has length at most \(k\). For \(x = s\), \(\mathop{\mathrm{\mathrm{\small Search}}}\) is invoked at node \(s\) exactly once during the entire execution (the initial call from \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\)), so at most one S-event at \(s\) can occur. ◻
Lemma 20 (U-Event Bound). Every U-block at a node \(x \ne s\) contains at most \(k\) events. At \(x = s\), no U-event occurs.
Proof. Each U-event at \(x\) assigns \(b[x] \gets d + 1\) under the guard \(b[x] > d + 1\), hence strictly decreases \(b[x]\). By 4 ()(2), each assigned value is at least \(1\), and by 2 (), \(b[x] \le k + 1\) with equality only at \(x = s\).
For \(x \ne s\), the assigned values lie in \(\{1, 2, \dots, k\}\), so a strictly decreasing chain of U-events at \(x\) has length at most \(k\).
For \(x = s\), the initial call \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\) pushes \(s\) onto the search path and \(s\) remains there throughout the execution; the \(p \notin S\) guard in the cascade therefore prevents any U-event at \(s\). ◻
Lemma 21 (Cascade Witness Path). Under the cascade \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v, sd)\) of 13 (), invoked from a fruitful \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\), every enqueued node \(x\) admits an \(x\)-\(t\)-path of length \(b[x]\) whose nodes avoid \(P\).
Proof. By 13 (), \(b[x] = sd + dist_{Pv}(x,v)\). Take a shortest \(x\)-\(v\)-path realizing \(dist_{Pv}(x,v)\); it meets \(Pv\) only at \(v\). Since \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) is fruitful, it produces an output whose suffix from \(v\) is a \(v\)-\(t\)-path of length \(sd\) (the shortest produced), with interior nodes searched below \(v\) and hence off \(Pv\). Concatenating the two gives an \(x\)-\(t\)-path of length \(dist_{Pv}(x,v) + sd = b[x]\) whose only node in \(Pv\) is the junction \(v\); as \(v \notin Pv \setminus \{v\}\), the path avoids \(P\). ◻
Lemma 22 (Interval Ending). Consider a node \(x \in V\) and an interval, and the sequence of S- and U-events at \(x\) in that interval (ignoring F-events). Once a U-block at \(x\) ends, no further U-event at \(x\) occurs in the interval.
Proof. If no U-event at \(x\) occurs in the interval, the claim holds trivially — in particular for the first interval, which has no spine path and hence no cascade.
Otherwise, let \(S_\tau = (s = v_0, v_1, \dots, v_l = t)\) be the spine path opening the interval (see 4), and let \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v_i, sd)\) be the cascade containing the last U-event of the U-block at \(x\), setting \(b[x] = d\). If no S-event at \(x\) follows, the interval ends with that U-block and the claim holds. So suppose a later S-event at \(x\) occurs, triggered by some \(\mathop{\mathrm{\mathrm{\small Search}}}(v_j)\). Since each cascade is the last action at its spine level, \(j < i\).
Let the search path at the moment of that S-event be \(S' = (v_0, \dots, v_j, q, \dots, x)\) — possibly \(q = x\) — where \(q\) is the successor of \(v_j\) currently being explored in \(\mathop{\mathrm{\mathrm{\small Search}}}(v_j)\)’s for-loop; write \(h = \|S'\|\). The segment \((q, \dots, x)\) has length \(h - j - 1\) and avoids \(\{v_0, \dots, v_j\}\) by simplicity of the search path (Observation [obs:simple-search-path]). The pruning guard at the S-event gives \(b[x] \le k - h\); since the preceding U-event set \(b[x] = d\), we have \(d \le k - h\), i.e.\(h + d \le k\).
We show that \(\mathop{\mathrm{\mathrm{\small Search}}}(q)\) returns fruitful, producing the next \(s\)-\(t\) path before returning to \(\mathop{\mathrm{\mathrm{\small Search}}}(v_j)\) — making \(v_j\) the LCA of \(S_\tau\) and \(S_{\tau+1}\), and ending the interval. By 21 () applied to the cascade \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v_i, sd)\) (whose live search path is \((v_0, \dots, v_i)\)), there is an \(x\)-\(t\)-path \(W\) of length \(d\) avoiding \(\{v_0, \dots, v_{i-1}\}\), hence in particular avoiding \(\{v_0, \dots, v_j\}\).
Concatenating \((q, \dots, x)\) with \(W\) yields a \(q\)-\(t\)-path \(Q\) in \(G \setminus \{v_0, \dots, v_j\}\) of length \((h - j - 1) + d \le k - j - 1\). \(Q\) need not be simple; shortcutting any repeated nodes gives a simple \(q\)-\(t\)-path \(Q'\) of length at most \(k - j - 1\) in the same sub-graph. Prepending \((v_0, \dots, v_j, q)\) to \(Q'\) extends it to a simple \(s\)-\(t\)-path \(R\) of length at most \(k\), whose first \(j + 2\) nodes coincide with the current search path.
By 2 (), \(R\) is produced by \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G, s, t, k)\); by Observation [obs:search-path-uniqueness], each search path occurs at most once during the execution. Since the search path \((v_0, \dots, v_j, q)\) is currently active, \(R\) must be produced during this ongoing call \(\mathop{\mathrm{\mathrm{\small Search}}}(q)\); reaching \(t\) along \(R\) yields the next output and ends the interval.
Before \(\mathop{\mathrm{\mathrm{\small Search}}}(q)\) reaches \(t\), node \(x\) may still receive trailing S-events; the lemma’s claim concerns U-events only. ◻
Lemma 23 (Block Sequence). In any interval, for each node \(x\) the sequence of S- and U-events at \(x\) has the form \(S^* U^* S^*\), where \(^*\) denotes zero, one, or more repetitions of the indicated event type.
Proof. Reading the sequence in order, it begins with a (possibly empty) leading S-block. If any U-event occurs, the first such event starts the U-block; by 22 (), once this U-block ends, no further U-event at \(x\) occurs in the interval. Any S-events that occur after the U-block thus form a single trailing S-block. Hence, the sequence has the claimed form. ◻
Theorem 3 (Delay Bound). For a graph \(G\) with \(n\) nodes and \(m\) edges, and the standing length bound \(0 < k \le n\), \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G,s,t,k)\) has a per-interval delay bounded by \(3(k+1)(n+m) \;\in\; \mathcal{O}(k(n+m))\).
Proof. By 23 (), each node participates in at most two S-blocks and one U-block per interval. By 19 () and 20 (), each block contains at most \(k\) events (with at most one S-event at \(s\), and no U-event at \(s\)). Each spine node \(\ne t\) additionally contributes at most one F-event per interval, and by 5 () the spine contains at most \(k + 1\) nodes.
Every elementary step of the execution belongs either to a \(\mathop{\mathrm{\mathrm{\small Search}}}\) call — entry and exit bookkeeping, the successor scan of the for-loop, and the post-loop assignment — or to a cascade — dequeuing a pair and scanning its predecessors. Since output is produced only inside the for-loop of \(\mathop{\mathrm{\mathrm{\small Search}}}\), a cascade runs entirely within one interval; and a fruitless call, containing no output, lies entirely within one interval as well. A fruitful call may span several intervals: it terminates in the interval of its F-event, and in every earlier interval it intersects it is still on the stack at the closing output. We charge each step to the interval in which it is executed.
Each non-origin dequeue in a cascade corresponds to the U-event that enqueued the pair and costs \(1 + |\mathop{\mathrm{\mathrm{pred}}}(x)|\) steps (propagation-guard checks); both lie in the same interval. With at most \(k\) U-events per node per interval: \[\sum_{x \in V} k \cdot (1 + |\mathop{\mathrm{\mathrm{pred}}}(x)|) \;=\; k\,(n+m).\]
Each S-event at \(x\) corresponds to a fruitless \(\mathop{\mathrm{\mathrm{\small Search}}}\) call at \(x\), executed entirely within the S-event’s interval, of cost \(1 + |\mathop{\mathrm{\mathrm{succ}}}(x)|\) (pruning-condition checks). With at most \(2k\) S-events per node per interval: \[\sum_{x \in V} 2k \cdot (1 + |\mathop{\mathrm{\mathrm{succ}}}(x)|) \;=\; 2k\,(n+m).\]
F-events occur only at spine nodes except for \(v_l = t\). The F-event at a spine node \(v_j\) is charged the entire cost of its fruitful \(\mathop{\mathrm{\mathrm{\small Search}}}\) call, \(1 + |\mathop{\mathrm{\mathrm{succ}}}(v_j)|\), together with the cascade origin \(\mathop{\mathrm{\mathrm{\small Fruitful}}}(v_j, sd_j)\), costing \(1 + |\mathop{\mathrm{\mathrm{pred}}}(v_j)|\) — a deliberate over-charge, since part of the scan may have been executed in earlier intervals. By 5 () the spine contains at most \(k\) nodes besides \(t\): \[\sum_{v_j \in S_\tau \setminus \{t\}} \bigl(2 + |\mathop{\mathrm{\mathrm{succ}}}(v_j)| + |\mathop{\mathrm{\mathrm{pred}}}(v_j)|\bigr) \;\le\; 2k + 2m.\]
It remains to cover the steps that fruitful calls execute in intervals before the one containing their F-event. In such an interval \(\tau\), the call is on the stack at the closing output, so its node lies on \(S_{\tau+1} \setminus \{t\}\) (the search path at that moment is \(S_{\tau+1}\) less its final node \(t\)) — at most \(k\) distinct nodes. Each call examines every successor at most once during its lifetime, so the work these live calls execute within \(\tau\) is at most \[\sum_{x \in S_{\tau+1} \setminus \{t\}} \bigl(1 + |\mathop{\mathrm{\mathrm{succ}}}(x)|\bigr) \;\le\; k + m.\]
For the terminal interval this sum is empty (\(S_{T+1} = \emptyset\)): every call live in it terminates within it and is charged by its own S- or F-event. Likewise, the fruitful-work sum is empty for the first interval (\(S_1 = \emptyset\)), which contains no F-event. Summing, the per-interval delay is bounded by \[2k(n+m) + k(n+m) + (2k + 2m) + (k + m) \;=\; 3k(n+m) + 3(k+m) \;\le\; 3(k+1)(n+m),\] the last inequality using \(k \le n\). ◻
Fruitful work and boundary work are thus symmetric: the former is indexed by the spine \(S_\tau\) that opens the interval, the latter by the spine \(S_{\tau+1}\) that closes it.
3 charges every interval the full \(3(k+1)(n+m)\). Two refinements lower the effective constant: the first interval is genuinely cheaper, and across an output boundary the trailing and leading fruitless work of consecutive intervals can be amortized. We record both, the former as a proven sharpening and the latter as a conjecture with its residual obligation made precise. Both rest on the global monotonicity clause of the joint induction (17 ()). This lemma is a statement about a completed call: a fruitful call may lower barriers transiently while its cascade is in flight, but never below the value held at the call’s entry. It does not bound barriers at instants interior to a call still on the stack — precisely the instants that an output boundary straddles — which is why it sharpens the first interval but leaves the cross-boundary amortization a conjecture.
The first interval starts at the entry of \(\mathop{\mathrm{\mathrm{\small Search}}}(s)\) and ends at the first output, which is produced inside the for-loop of the deepest spine node, before that call returns fruitful. No \(\mathop{\mathrm{\mathrm{\small Search}}}\) call has yet returned fruitful, so no \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\) cascade has run: the interval contains neither F-events nor U-events. By 23 () the event sequence at each node is a single S-block, and only the fruitless-work and boundary-work terms of 3 () contribute. The first interval therefore has delay at most \(k(n+m) + (k + m) \le (k + 1)(n + m)\), a factor \(3\) below the general bound.
Fix a node \(x\) and read its S- and U-events across the whole run, ignoring the output boundaries. Within one interval the sequence has the form \(S^* U^* S^*\) (23 ()). An output is not a barrier event at \(x\), so the trailing S-block of interval \(\tau\) and the leading S-block of interval \(\tau+1\) are separated only by the output boundary — unless a barrier-lowering write to \(x\) falls between them. The only lowering writes are U-events (guarded cascade decreases) and the F-event origin of \(x\)’s own fruitful call (which ends \(x\)’s interval). Thus, if no U-event at \(x\) occurs across the boundary, the two S-blocks form one contiguous strictly increasing chain, which by 19 () still has at most \(k\) events.
This suggests counting the cumulative fruitless work over the first \(p\) outputs by maximal monotone S-runs rather than per-interval S-blocks. Each node’s S-events decompose into runs delimited by its lowering writes, every run of length at most \(k\); the number of runs at \(x\) is \(1\) plus the number of lowering writes to \(x\). Charging each run to the U-event (or interval-ending F-origin) that closes it yields, over \(p\) outputs, \(p\) S-runs interspersed with the \(p-1\) U-blocks of the interior boundaries, in place of the \(2p\) S-blocks and \(p\) U-blocks counted interval-by-interval. Empirically the per-output delay settles near \(2k(n+m)\) rather than \(3k(n+m)\), consistent with this picture.
We state the amortized bound as a conjecture, since the charging argument above trades the clean per-interval accounting of 3 () for a global S\(\leftrightarrow\)U bookkeeping whose constant we have not established rigorously; the worst-case per-interval bound of 3 () remains the proven guarantee.
Conjecture 1 (Amortized Delay). The cumulative delay of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G,s,t,k)\) over its first \(p\) outputs is \(2k(n+m)p + O(k(n+m))\); equivalently, the amortized per-output delay tends to \(2k(n+m)\).
We close this section with a delay bound for enumerating all simple cycles.
Corollary 3 (Delay for Enumerating All Simple Cycles). After a pre-processing step taking \(O(n(n+m))\) time, all simple cycles of length at most \(k\) in graph \(G\) can be enumerated with \(O(k(n+m))\) delay.
Proof. By 3.3, the runs \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}(G^i, v_i, v_i, k)\) for \(v_i \in L\) output every simple cycle of length at most \(k\) exactly once, and every executed run produces at least one output. Within a run, 3 () applies through 2 () to the graphs \(G^i \subseteq G\). Between the last output of one run and the first output of the next lie at most one terminal interval, the \(O(n+m)\) set-up of the next run (constructing \(G^i\) and initializing \(b \equiv 0\)), and one first interval — in total \(O(k(n+m))\) by 3 () and the first-interval bound of 6.2. ◻
The pruning of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) is governed entirely by the barrier values, and the only freedom in the algorithm is how the algorithm revises the barriers. Several schemes share the same skeleton — the recursive search, and the pruning condition \(b[w] + h < k\) — and differ only in the barrier post-processing after recursion. We call a scheme edge-consistent if it maintains edge-consistency with respect to the current search path at every quiescent point, i.e.whenever control is in \(\mathop{\mathrm{\mathrm{\small Search}}}\) and not inside a fruitful cascade; by 8 () every edge-consistent scheme is complete. The tight scheme of the original \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) is one extreme. We record three further points on the spectrum.
Leave every barrier at \(0\): the algorithm does not manage barriers at all. Then \(b \equiv 0\) is trivially edge-consistent w.r.t.any search path, so the scheme is complete — it is plain depth-first search with the length cutoff \(h < k\), performing no barrier-based pruning. Soundness and completeness obviously hold, but there is no polynomial delay bound: if the depth-first search first descends into a complete subgraph of size \(k-1\) not containing the target \(t\), it traverses \(\Theta((k-2)!)\) partial paths before producing any output.
The loose scheme keeps the backward cascade of the fruitful case but replaces the distance values it deposits by \(0\). That is, 3 () is replaced by \(\mathrm{\small Reset}(v)\): a breadth-first traversal backwards from \(v\) over predecessors, restricted to nodes off the search path, setting every visited barrier to \(0\).
The guard \(b[p] \ne 0\) cannot be tightened to the depth-aware \(b[p] > d + 1\) of the tight cascade. Because \(\mathrm{\small Reset}\) records no distance information, edge-consistency is preserved only by resetting the entire reachable off-path cone: stopping the propagation early would leave a node with a positive barrier adjacent to a node reset to \(0\), breaking consistency. The full cone is the price of discarding distances, and it is why the loose scheme has no delay advantage — a point we return to below.
The conceptual value of the loose scheme is that it isolates which part of the tight correctness proof is essential. We show it is edge-consistent; completeness then follows from 8 () as for any edge-consistent scheme. As in the tight case, a cascade transiently violates edge-consistency while in flight and restores it on completion, so the statements below concern quiescent points.
The case that dominates the tight proof disappears. A fruitful node ends its cascade with \(b[v] = 0\) (line 2 of 5), so every outgoing edge \((v,y)\) satisfies \(b[v] \le b[y] + 1\) as \(0 \le b[y] + 1\). This is precisely the case for which the tight proof needs the exact value \(sd = dist_{Pv}(v,t)\), and hence completeness; here it is free. The only case requiring an argument is an off-path edge \((x,y)\) whose head \(y\) was reset to \(0\), settled by the following closure property.
Lemma 24 (Reset Closure). Let \(\mathrm{\small Reset}(v)\) run with search path \(S\), and let \(R\) be the set of nodes it sets to \(0\). Then at the cascade’s completion, every off-path predecessor of a node in \(R\) has barrier \(0\).
Proof. Every node placed in \(R\) is enqueued, and the while-loop runs until \(Q\) is empty, so each \(y \in R\) is dequeued and all its predecessors are examined (lines 6–8). For an off-path predecessor \(x\) of such a \(y\): if \(b[x] \ne 0\) the guard sets it to \(0\); otherwise \(b[x] = 0\) already. Either way \(b[x] = 0\), and since the cascade only sets values to \(0\), this persists to completion. ◻
If \((x,y)\) is off-path with \(y \in R\), then \(x\) is an off-path predecessor of a reset node, so \(b[x] = 0\) and \(b[x] \le b[y] + 1\). The configuration one might fear — a fruitless node \(x\) with a high barrier pointing into a freshly-reset \(y\) — cannot arise, because the cascade reaches \(x\) through \(y\) and resets it too. Off-path edges with both endpoints untouched inherit consistency from before the cascade, and the edges that the pop of \(v\) newly constrains are consistent for the same two reasons (\(b[v] = 0\) outgoing, 24 with \(y = v\) incoming). The fruitless case and the push are as in the tight scheme. Hence, the loose scheme is edge-consistent, and the four-way joint induction of 5 collapses to a single inequality invariant: no exact-value claim, no coupling to completeness.
Both, tight and loose schemes are complete and deterministic and scan successors in the same order. Since pruning removes only output-free subtrees, each emits its outputs in lexicographic path order; hence the two output sequences are equal. Therefore, the intervals correspond one-to-one and the spine paths coincide. The fruitful calls returning within an interval are exactly the calls along its spine, so the fruitful and boundary work of the tally in 3 () is identical in both schemes.
Nonetheless, there can be more fruitless searches within an interval, because some barriers are reset to 0 instead of being updated to the tight bound and 23 () fails for the loose scheme, violating executions were observed experimentally. We leave the delay bound for the loose scheme as an open question.
The loose scheme (7.2) discards distance information but still incurs, at every fruitful step, the cost of a backward cascade over the entire reachable off-path cone. The lazy scheme retains the same coarse reset to \(0\) while deferring the cascade. A fruitless node registers itself in a dependency list at each of its successors, and a later fruitful node consumes those lists, clearing only the nodes that registered through it. Distance information is still discarded—a fruitful node is reset to \(0\) exactly as in the loose scheme— so the lazy scheme inherits the loose scheme’s simple correctness argument, which does not rely on exact distance values. The only difference is which barriers are cleared by a fruitful step, and when they are cleared.
Each node \(x\) now carries, in addition to its barrier \(b[x]\), a dependency list \(B[x] \subseteq V\). When a call \(\mathop{\mathrm{\mathrm{\small Search}}}(v)\) returns fruitless at depth \(h\), it performs the usual assignment \[b[v] \gets k-h+1\] and additionally inserts \(v\) into \(B[w]\) for every successor \(w \in \mathop{\mathrm{\mathrm{succ}}}(v)\) (the registration step, line [line:register]). The fruitful case runs \(\mathrm{\small Update}(v)\) instead of the loose reset.
The barrier \(b[\cdot]\) is initialized to \(0\) and the dependency lists \(B[\cdot]\) to \(\emptyset\); the rest of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) (3) is unchanged. The clear of \(B[v]\) in line [line:clear] couples de-registration with clearing: a node is removed from a dependency list exactly when the cascade that clears its barrier passes through. Without it the lists would only grow, accumulating stale entries; with it they record precisely the nodes whose positive barrier is still in force, which is what the analysis below exploits.
Gupta and Suzumura [10] pair lazy registration with the tight (distance-depositing) fruitful case; but that combination is not always complete, see [13]. The lazy scheme is complete precisely because it is coarse: it resets to \(0\), so no exact distance need be maintained, and registration only has to control which nodes are reset.
Next, we show completeness of the lazy scheme.
The mechanism rests on a single edge-local invariant.
Lemma 25 (Registration Invariant). At every instant of the execution, including while a cascade is in progress, every node \(x\) with \(b[x] > 0\) and \(x \notin S\) satisfies \(x \in B[w]\) for every successor \(w \in \mathop{\mathrm{\mathrm{succ}}}(x)\).
Proof. A barrier is written only by initialization (\(0\)), by the fruitful reset (\(0\)), by the fruitless assignment (\(k - h + 1\)), or by \(\mathrm{\small Update}\) (\(0\)). Any positive value of \(b[x]\) must originate from a fruitless assignment, made by some invocation \(\sigma = \mathop{\mathrm{\mathrm{\small Search}}}(x)\); immediately after it, \(\sigma\) inserted \(x\) into \(B[w]\) for every \(w \in \mathop{\mathrm{\mathrm{succ}}}(x)\) (line [line:register]). We show \(x\) remains in all of these lists until the instant in question.
A node leaves a list only by the clear \(B[w] \gets \emptyset\) on line [line:clear], inside some \(\mathrm{\small Update}(w)\). Suppose such an \(\mathrm{\small Update}(w)\) runs after \(\sigma\)’s assignment and removes \(x\), so \(x \in B[w]\) when its loop reaches \(x\). At that moment:
if \(x \notin S\) and \(b[x] > 0\), the loop executes \(b[x] \gets 0\) — a write to \(b[x]\) later than \(\sigma\)’s, so \(\sigma\)’s is not the most recent, contradicting that \(b[x] > 0\) now stems from \(\sigma\);
if \(x \notin S\) and \(b[x] = 0\), the barrier fell from its positive value to \(0\) after \(\sigma\) — again a later write, the same contradiction;
if \(x \in S\), some \(\mathop{\mathrm{\mathrm{\small Search}}}(x)\) is on the stack; it began after \(\sigma\) returned (since \(\sigma\) popped \(x\)) and either returns before the instant in question, writing \(b[x]\) later than \(\sigma\), or is still on the stack then, making \(x \in S\), contrary to assumption.
Every case is contradictory, so no \(\mathrm{\small Update}\) removes \(x\) from any \(B[w]\); hence \(x \in B[w]\) for every \(w \in \mathop{\mathrm{\mathrm{succ}}}(x)\). ◻
We show the lazy scheme is edge-consistent w.r.t.the current search path at every point at which control is not inside an \(\mathrm{\small Update}\) cascade; completeness then follows from 8 () exactly as for the loose scheme. As before, a cascade transiently breaks edge-consistency and restores it on completion, so the statement concerns these quiescent points.
The induction over the run is identical to the loose case (7.2) on entry, fruitless assignment, and push; only the fruitful cascade differs, and there 25 replaces the loose closure property. The crux is the following.
Lemma 26 (Cascade clears predecessors). During \(\mathrm{\small Update}(v)\), for every node \(y\) on which \(\mathrm{\small Update}(y)\) is invoked, every off-stack predecessor \(x\) of \(y\) has \(b[x] = 0\) from the moment \(\mathrm{\small Update}(y)\) returns.
Proof. Consider the start of \(\mathrm{\small Update}(y)\). If \(b[x] > 0\) and \(x \notin S\) then, since \(y \in \mathop{\mathrm{\mathrm{succ}}}(x)\), 25 gives \(x \in B[y]\), so the loop of \(\mathrm{\small Update}(y)\) reaches \(x\) and, as \(x \notin S\), sets \(b[x] \gets 0\). If instead \(b[x] = 0\), nothing is required. A cascade only sets barriers to \(0\) and never raises one, so \(b[x] = 0\) persists until \(\mathrm{\small Update}(y)\) returns. ◻
With 26, the fruitful cascade preserves edge-consistency just as the loose reset did. Consider an off-path edge \((x,y)\) after \(\mathrm{\small Update}(v)\) completes. If \(b[y]\) was cleared by the cascade, then \(\mathrm{\small Update}(y)\) was invoked. Since \(x\) is an off-stack predecessor of \(y\), 26 implies that \(b[x]=0\) from the moment \(\mathrm{\small Update}(y)\) returns. Therefore, \(b[x]=0 \le b[y]+1.\) If \(b[y]\) was not cleared, then the edge retains the consistency it had before the cascade. Indeed, \(b[x]\) can only have decreased during the cascade, so any inequality \(b[x] \le b[y]+1\) that held before the cascade continues to hold afterward. The fruitful node itself ends with \(b[v]=0\). Hence, its outgoing edges are consistent for free. Its incoming edges are covered by 26 with \(y=v\), for exactly the same reason as in the loose scheme. The fruitless case, the push, and the pop are as in the loose scheme. Thus, the lazy scheme is edge-consistent at every quiescent point of the execution. By 8 (), it follows that the algorithm produces every simple \(s\)-\(t\)-path of length \(\le k\).
Like the loose scheme, the lazy scheme discards distance information and resets fruitful nodes to \(0\). Consequently, it offers no proven delay improvement over the tight scheme, and its interval-delay complexity remains open. Its main interest is structural. It demonstrates that the fruitful cascade can be driven lazily, through dependency lists accumulated during fruitless search and consumed upon success, while still preserving edge-consistency. More importantly, it shows that correctness depends on the coarse reset itself rather than on the lazy bookkeeping. Indeed, it is precisely the combination of lazy registration with a tight fruitful case that fails in \(\mathrm{\small CYCLE\_SEARCH}\), as shown in [13]. The lazy scheme remains complete because it abandons exact distance information and resets fruitful nodes to \(0\).
Now that we have established the correctness of \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) and its variants, we turn to the \(\mathrm{\small BC-DFS}\) algorithm of Peng et al. [11], [12]. We show that \(\mathrm{\small BC-DFS}\) is not complete and identify a corresponding gap in its correctness proof. The crucial difference between \(\mathrm{\small BC-DFS}\) and \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) lies in the handling of fruitful returns. In \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\), a fruitful call always performs an unconditional barrier update through \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\) (3). By contrast, \(\mathrm{\small BC-DFS}\) propagates a fruitful value only when a guard condition is satisfied. Its update procedure, reproduced in [alg:UpdateBarrier], assigns a value \(l\) to a node \(u\) only if \(b[u] > l\). Moreover, if the guard fails for the initial call to \(\mathrm{\small UpdateBarrier}\), the entire update cascade is skipped. This behavior appears both in the conference version [11] and in the journal version [12]. As we show below, suppressing the cascade in this way can leave stale barrier values in place and may cause valid paths to be pruned.
Skipping the update cascade can violate edge-consistency and thereby destroy completeness. This is demonstrated by the graph \(X\) depicted in 8.
The directed graph \(X\) is assumed to be stored in adjacency list format in alphabetical order. It contains the following simple paths starting at node \(A\), terminating at node \(E\) and having length 4 or less:
\((A,B,E)\) of length 2,
\((A,C,B,E)\) of length 3, and
\((A,C,D,B,E)\) of length 4.
However, when \(\mathrm{\small BC-DFS}(G,s,t,k)\) with \(G=X\), \(s=A\), \(t=E\), \(k=4\) is executed, it will only find the first two paths and miss the third one. An execution trace for the counter-example is given in [list:bcdfs-counterexample-X].
While \(B\) is on the search path, the fruitless searches of \(C\) and \(D\) raise their barriers to \(b[C] = b[D] = 3\).
When the search of \(B\) then returns fruitful, \(\mathrm{\small BC-DFS}\) skips its \(\mathrm{\small UpdateBarrier}\) cascade — visible as the
absence of any update at search(B) fruitful, the barrier vector being unchanged across the pop of \(B\). The relaxations that would lower \(b[C]\) and \(b[D]\) along the edges \((C, B)\) and \((D, B)\) are therefore never performed, and \(b[D] = 3\) persists.
The stale barrier is fatal one step later. When the search path becomes \((A, C)\), the successor \(D\) is examined at depth \(h = 1\); the pruning test
fails, since \(b[D] + h = 3 + 1 = 4 \ge k\), so \(D\) is pruned (trace: D pruned (4 >= k)). The only \(A\)-\(E\)-path through this edge, \((A, C, D, B, E)\), is thereby lost: \(\mathrm{\small BC-DFS}\) outputs \((A, B, E)\) and \((A, C, B, E)\) but misses the valid path \((A, C, D, B, E)\) proving that the algorithm is not complete. The same stale \(b[D] = 3\) had already pruned \(D\) at the deeper path \((A, C, B)\), where \(b[D] + h = 3 + 2 = 5 \ge k\) (trace: D pruned (5 >= k)).
Additional counter-examples were found experimentally by searching small random graphs, of which \(X\) is among the smallest. Moreover, infinitely many counter-examples can be obtained by suitable augmentations of \(X\).
The incompleteness of \(\mathrm{\small BC-DFS}\) is not merely an implementation issue. Upon closer inspection, the correctness proof contains a gap precisely at the point where the algorithm fails on the counter-example above. The proof of Theorem 1 in [11], [12] argues that “for any vertex \(u\), \(u.\mathrm{bar}\) is correctly maintained in Algorithm \(\mathrm{\small BC-DFS}\)”. The argument distinguishes two cases, depending on whether the vertex \(x\) coincides with a vertex \(v\). For the case \(x \ne v\), the proof explicitly describes how barrier values are propagated along the path \(p(u \to x)\). For the case \(x = v\), however, it states only that “the proof is similar” and does not provide the corresponding argument. Our counter-example falls precisely into this omitted case. When \(x=v\) and \(N=\emptyset\), the propagation argument through the vertices of \(N\) becomes vacuous. At the same time, the guard \(u.\mathrm{bar} > l\) in \(\mathrm{\small UpdateBarrier}\) may prevent the relaxation from reaching \(u\). Consequently, stale barrier values can remain in place and valid paths may be pruned, exactly as observed in the counter-example. Thus, the failure exhibited by the counter-example corresponds precisely to the case that is not established in the published proof.
We also identify a gap in the time-complexity argument of \(\mathrm{\small BC-DFS}\). Beyond its relevance to the complexity analysis, the discussion reveals several interesting structural properties of the algorithm. In [11], [12], the central step in the proof of Theorem 2, which states that “\(\mathrm{\small BC-DFS}\) is a polynomial-delay algorithm with \(O(km)\) time per output”, is the following argument:
Suppose a vertex u is unstacked twice and there is no new output in Algorithm 1. Let \(S1\) and \(S2\) denote the stack size after \(u\) is pushed into the stack at the first and the second time, respectively. We have \(u.bar = k-S1+2\) after u is unstacked at the first time. As there is no new output, the propagation of barrier values will not be invoked. Thus, \(u.bar\) remains the same when \(u\) is pushed to stack at the second time. As \(u\) passes the barrier-based pruning in the second visit, we have \(S2 + u.bar \le k\), and hence \(S2 < S1\).
However, this argument does not correctly account for the interleaving of \(\mathop{\mathrm{\mathrm{\small Search}}}\) and \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\) (here: \(\mathrm{\small UpdateBarrier}\)) calls while the recursion unwinds. As a result, the claimed monotonicity property is false: barrier values may change between two visits of the same vertex even when no new output is produced. A counter-example demonstrating this behavior is depicted in 9.
The graph \(Y\) is stored in adjacency-list format in alphabetical order. The complete execution trace of \(\mathrm{\small BC-DFS}(G,s,t,k)\) with \(G = Y\), \(s = E\), \(t = C\), \(k = 6\) is given in [list:bcdfs-counterexample-Y]; the barrier vector \((b[A], b[B], b[C], b[D], b[E], b[F])\) is shown after every step. \(\mathrm{\small BC-DFS}\) produces all three \(s\)-\(t\)-paths \((E, A, D, C)\), \((E, B, D, C)\), and \((E, D, C)\), so completeness is not at issue in this example.
We focus on the node \(F\). In the interval between the second output \((E, B, D, C)\) and the third \((E, D, C)\), two observations are crucial.
First, after the second output \((E, B, D, C)\), the recursion unwinds and the call \(\mathop{\mathrm{\mathrm{\small Search}}}(B)\) at search path \((E, B)\) returns fruitful — its fruitfulness stems from that earlier output, produced within it at greater depth. Its \(\mathrm{\small UpdateBarrier}\) cascade is therefore invoked during the unwind, although no new output has been produced since. The cascade lowers \(b[B] \gets 2\) and \(b[F] \gets 3\). This already contradicts the premise of the quoted argument — that in the absence of a new output “the propagation of barrier values will not be invoked”: between two consecutive outputs, cascades of fruitful calls returning on the spine of the previous output do run.
Second, and within the same interval, \(F\) is unstacked fruitless twice. It is first searched fruitless at search path \((E, B, F)\), of length \(2\), setting \(b[F] \gets 5\); later, after the cascade has reset it to \(3\), it is searched fruitless again at search path \((E, D, B, F)\), of greater length \(3\), setting \(b[F] \gets 4\). So the two stack sizes at which \(F\) is unstacked within one interval satisfy \(S_2 > S_1\), directly contradicting the claimed \(S_2 < S_1\). The barrier of \(F\) is correspondingly non-monotone, moving \(5 \to 3 \to 4\).
Because barrier propagation is invoked without a new output, the step “\(u.bar\) remains the same when \(u\) is pushed to stack the second time” fails, and with it the conclusion \(S_2 < S_1\). The postulated interval delay bound of \(O(km)\) therefore does not follow, and remains open for \(\mathrm{\small BC-DFS}\).
Note that monotonicity does hold in the first interval, where no spine path unwinds and hence no \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\) cascade runs.
The trace for \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) on this graph is similar, with additional cascade updates, but the non-monotone assignments to \(b[F]\) are the same. Accounting correctly for the interleaved \(\mathop{\mathrm{\mathrm{\small Search}}}\) and \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\) calls across all intervals is the key point of our \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) delay-bound proof.
We conducted a preliminary experimental study to quantify the frequency of paths missed by \(\mathrm{\small BC-DFS}\) under random graph models. All experiments were implemented using the NetworkX library [16]. The source code used in the evaluation is publicly available in our GitHub repository [18]. The ground-truth was calculated using a depth-limited depth-first search, not pruned by barrier values, the trivial scheme from 7.1.
We begin with random Erdős–Rényi graphs [21], [22]. For the parameter settings considered, the ratio of missed paths increased with the path-length bound \(k\), exceeding \(10\%\) for \(k=10\); see ¿tbl:table:experiments95er?.
Next, we considered a directed variant of random Watts-Strogatz graphs [23], modelling small-world networks which are closer to the applications intended for BC-DFS. Here, the mean missed path ratio is rapidly growing to over 33% for \(k=10\), see ¿tbl:table:watts-strogatz-experiment?.
The observed total runtime (wall-clock) for \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) and \(\mathrm{\small BC-DFS}\) in these experiments was in the same order of magnitude, with \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) using roughly 50% more time than \(\mathrm{\small BC-DFS}\).
To isolate the source of this overhead, we instrumented BC-DFS and a minimal repaired variant, kick-start. The code is identical except for one added line setting \(b[v] \gets k+1\) before the origin call of \(\mathrm{\small UpdateBarrier}\), which makes its first assignment unconditional, mimicking the unconditional \(b[v] \gets sd\) of \(\mathop{\mathrm{\mathrm{\small Fruitful}}}\) (3) while leaving the rest of the BC-DFS implementation untouched. Kick-start produced the ground-truth output on all tested instances. Normalized per output, the two variants perform nearly the same number of search calls and successor probes, whereas BC-DFS performs less than \(6\%\) of kick-start’s predecessor probes and barrier writes; detailed counts are available at [18]. The runtime overhead of the complete algorithms is thus attributable to the proper barrier propagation that completeness requires — work whose omission is precisely what causes the missed outputs quantified above.
We presented \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\), a bounded-scope depth-first search that enumerates all simple \(s\)-\(t\)-paths — and, via node splitting, all simple \(s\)-cycles — of length at most \(k\) in a directed graph, with a worst-case delay of \(O(k(n+m))\) per output (3). The algorithm follows the line of barrier-based methods initiated by Johnson and refined by Peng et al.and by Gupta and Suzumura, but it is built around a single explicit invariant, edge-consistency: the barrier of an off-path node never exceeds one plus the barrier of any off-path successor. Read as a heuristic in the sense of \(A^*\), edge-consistency is exactly admissibility maintained as a search-time invariant, and it yields a transparent completeness argument — an admissible barrier never prunes a path that respects the budget.
The same invariant organizes a whole family of schemes that differ only in how barriers are revised (7). The tight scheme deposits exact distances and pays for its delay bound with a correctness proof in which completeness, the exact return value, and preservation of edge-consistency are mutually entangled. At the other end, the loose (7.2) and lazy (7.3) schemes discard distance information by resetting fruitful nodes to zero; this trades barrier precision for a markedly simpler correctness argument, since zero is the most admissible value and no exact-value claim is needed. The lazy scheme additionally shows that the backward cascade can be driven by dependency lists accumulated during fruitless search and consumed on success, while preserving edge-consistency. We regard this uniform treatment as evidence that edge-consistency is the right abstraction for bounded-scope search, rather than a device specific to one algorithm.
The framework also makes precise where a published algorithm goes wrong. In \(\mathrm{\small BC-DFS}\) (8) a single misplaced guard causes correct barrier relaxations to be silently dropped, breaking edge-consistency and, with it, completeness; our counter-example and the matching gap in the original proof both sit exactly at this point. The accompanying experiments (9) suggest that the resulting missed-path phenomenon is not confined to isolated counter-examples: under the graph models considered, the fraction of missed paths exceeds \(10\%\) and \(33\%\), respectively, already at \(k=10\).
As already proposed for many other path and cycle search algorithms [3], [10]–[12], [14], [15], our \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) algorithm can be combined with preprocessing steps like connected component decomposition and breadth-first search for reachability from one or both sides (bidirectional search) to further reduce the search space and improve practical performance.
A practical optimization is to initialize the barrier values in \(\mathop{\mathrm{\mathrm{\small BS-DFS}}}\) by an initial breadth-first search (BFS) from the target node \(t\) in the reverse graph, which sets the initial barrier value of each node to its distance towards \(t\). This allows for more pruning of the search space and thus practically faster execution, especially if the nodes \(x\) which cannot reach \(t\) in budget are initialized with \(b[x] = k + 1\) thus being eliminated from the search.
Several questions remain open. The most concrete is the delay of the loose and lazy schemes: both are complete and edge-consistent, yet resetting to zero re-arms nodes that were already searched fruitlessly within an interval, so the \(O(k(n+m))\) per-output bound of the tight scheme is not known to hold for them, and we make no such claim. Establishing a delay bound for either — or showing that none of the form \(O(k(n+m))\) exists — would sharpen the picture of the precision-versus-analyzability trade-off that the variant spectrum exposes. More broadly, edge-consistency is stated for unit edge weights and a single source and target; extending it to weighted budgets, to multiple targets, or to other structural constraints on the enumerated paths appears to be a natural direction, and one for which the invariant-based proof technique developed here should carry over.
For the tight scheme a linear delay bound is settled; what remains open is its constant. 3 proves \(3(k+1)(n+m)\) per interval, yet the first interval already costs only \((k+1)(n+m)\) (6.2), and the trailing and leading fruitless work of consecutive intervals appears to amortize across output boundaries. We conjecture an amortized per-output delay of \(2k(n+m)\) (1); proving it requires a global S\(\leftrightarrow\)U charging argument that the per-interval accounting does not supply.
A related question is how far edge-consistency can be relaxed: completeness needs only local admissibility (when tested for), which global edge-consistency implies but strictly exceeds, so characterizing the full class of admissible — and hence complete — bounded-scope schemes, edge-consistent or not, is open.
Our experiments are deliberately limited in scope: they use random graph models to investigate the frequency of the missed-path defect of \(\mathrm{\small BC-DFS}\), rather than to provide a thorough benchmark of running time. A broader empirical and comparative study measuring per-output delay on real-world road, social, and similar networks would require substantial code-level optimization. Such engineering work lies outside the focus of this paper and is left to future work.
S path: barriers : trace
: A B C D E :
: 0 0 0 0 0 : search(A) enter
A : 0 0 0 0 0 : .search(B) enter
AB : 0 0 0 0 0 : ..search(C) enter
ABC : 0 0 0 0 0 : ...search(B) B pruned (in S)
ABC : 0 0 0 0 0 : ...search(D) enter
ABCD : 0 0 0 0 0 : ....search(B) B pruned (in S)
ABCD : 0 0 0 0 0 : ....search(D) fruitless bar[D] := 2 (was 0)
ABC : 0 0 0 2 0 : ...search(D) exit
ABC : 0 0 0 2 0 : ...search(C) fruitless bar[C] := 3 (was 0)
AB : 0 0 3 2 0 : ..search(C) exit
AB : 0 0 3 2 0 : ..search(D) enter
ABD : 0 0 3 2 0 : ...search(B) B pruned (in S)
ABD : 0 0 3 2 0 : ...search(D) fruitless bar[D] := 3 (was 2)
AB : 0 0 3 3 0 : ..search(D) exit
AB : 0 0 3 3 0 : ..search(E) enter
ABE : 0 0 3 3 0 : ...search(E) output ['A', 'B', 'E']
AB : 0 0 3 3 0 : ..search(B) fruitful
A : 0 0 3 3 0 : .search(B) exit
A : 0 0 3 3 0 : .search(C) enter
AC : 0 0 3 3 0 : ..search(B) enter
ACB : 0 0 3 3 0 : ...search(C) C pruned (in S)
ACB : 0 0 3 3 0 : ...search(D) D pruned (5 >= k)
ACB : 0 0 3 3 0 : ...search(E) enter
ACBE : 0 0 3 3 0 : ....search(E) output ['A', 'C', 'B', 'E']
ACB : 0 0 3 3 0 : ...search(B) fruitful
AC : 0 0 3 3 0 : ..search(B) exit
AC : 0 0 3 3 0 : ..search(D) D pruned (4 >= k)
AC : 0 0 3 3 0 : ..search(C) fruitful
AC : 0 0 3 3 0 : ..update(C) bar[C] := 2 (was 3)
A : 0 0 2 3 0 : .search(C) exit
A : 0 0 2 3 0 : .search(A) fruitful
: 0 0 2 3 0 : search(A) exit
S path : barriers : trace
: A B C D E F :
: 0 0 0 0 0 0 : search(E) enter
E : 0 0 0 0 0 0 : .search(A) enter
EA : 0 0 0 0 0 0 : ..search(D) enter
EAD : 0 0 0 0 0 0 : ...search(A) A pruned (in S)
EAD : 0 0 0 0 0 0 : ...search(B) enter
EADB : 0 0 0 0 0 0 : ....search(D) D pruned (in S)
EADB : 0 0 0 0 0 0 : ....search(E) E pruned (in S)
EADB : 0 0 0 0 0 0 : ....search(F) enter
EADBF : 0 0 0 0 0 0 : .....search(B) B pruned (in S)
EADBF : 0 0 0 0 0 0 : .....search(F) fruitless bar[F] := 3 (was 0)
EADB : 0 0 0 0 0 3 : ....search(F) exit
EADB : 0 0 0 0 0 3 : ....search(B) fruitless bar[B] := 4 (was 0)
EAD : 0 4 0 0 0 3 : ...search(B) exit
EAD : 0 4 0 0 0 3 : ...search(C) enter
EADC : 0 4 0 0 0 3 : ....search(C) output ['E', 'A', 'D', 'C']
EAD : 0 4 0 0 0 3 : ...search(D) fruitful
EA : 0 4 0 0 0 3 : ..search(D) exit
EA : 0 4 0 0 0 3 : ..search(A) fruitful
E : 0 4 0 0 0 3 : .search(A) exit
E : 0 4 0 0 0 3 : .search(B) enter
EB : 0 4 0 0 0 3 : ..search(D) enter
EBD : 0 4 0 0 0 3 : ...search(A) enter
EBDA : 0 4 0 0 0 3 : ....search(D) D pruned (in S)
EBDA : 0 4 0 0 0 3 : ....search(A) fruitless bar[A] := 4 (was 0)
EBD : 4 4 0 0 0 3 : ...search(A) exit
EBD : 4 4 0 0 0 3 : ...search(B) B pruned (in S)
EBD : 4 4 0 0 0 3 : ...search(C) enter
EBDC : 4 4 0 0 0 3 : ....search(C) output ['E', 'B', 'D', 'C']
EBD : 4 4 0 0 0 3 : ...search(D) fruitful
EB : 4 4 0 0 0 3 : ..search(D) exit
EB : 4 4 0 0 0 3 : ..search(E) E pruned (in S)
EB : 4 4 0 0 0 3 : ..search(F) enter
EBF : 4 4 0 0 0 3 : ...search(B) B pruned (in S)
EBF : 4 4 0 0 0 3 : ...search(F) fruitless bar[F] := 5 (was 3)
EB : 4 4 0 0 0 5 : ..search(F) exit
EB : 4 4 0 0 0 5 : ..search(B) fruitful
EB : 4 4 0 0 0 5 : ..update(B) bar[B] := 2 (was 4)
EB : 4 2 0 0 0 5 : ..update(F) bar[F] := 3 (was 5)
E : 4 2 0 0 0 3 : .search(B) exit
E : 4 2 0 0 0 3 : .search(D) enter
ED : 4 2 0 0 0 3 : ..search(A) enter
EDA : 4 2 0 0 0 3 : ...search(D) D pruned (in S)
EDA : 4 2 0 0 0 3 : ...search(A) fruitless bar[A] := 5 (was 4)
ED : 5 2 0 0 0 3 : ..search(A) exit
ED : 5 2 0 0 0 3 : ..search(B) enter
EDB : 5 2 0 0 0 3 : ...search(D) D pruned (in S)
EDB : 5 2 0 0 0 3 : ...search(E) E pruned (in S)
EDB : 5 2 0 0 0 3 : ...search(F) enter
EDBF : 5 2 0 0 0 3 : ....search(B) B pruned (in S)
EDBF : 5 2 0 0 0 3 : ....search(F) fruitless bar[F] := 4 (was 3)
EDB : 5 2 0 0 0 4 : ...search(F) exit
EDB : 5 2 0 0 0 4 : ...search(B) fruitless bar[B] := 5 (was 2)
ED : 5 5 0 0 0 4 : ..search(B) exit
ED : 5 5 0 0 0 4 : ..search(C) enter
EDC : 5 5 0 0 0 4 : ...search(C) output ['E', 'D', 'C']
ED : 5 5 0 0 0 4 : ..search(D) fruitful
E : 5 5 0 0 0 4 : .search(D) exit
E : 5 5 0 0 0 4 : .search(E) fruitful
: 5 5 0 0 0 4 : search(E) exit