Efficient Prime Paths Generation

Adam Roman; Artur Pola\'nski; Jakub Ruszil; Jakub Zelek

arxiv: 2602.18768 · v2 · submitted 2026-02-21 · 💻 cs.SE

Efficient Prime Paths Generation

Jakub Zelek , Jakub Ruszil , Adam Roman , Artur Pola\'nski This is my paper

Pith reviewed 2026-05-15 20:49 UTC · model grok-4.3

classification 💻 cs.SE

keywords prime path generationstructural testingcontrol flow graphsstrongly connected componentscycle enumerationgraph traversalsoftware verification

0 comments

The pith

A structural characterization of prime paths via strongly connected components reduces prime path generation to constrained cycle enumeration in an augmented graph.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops an efficient method for generating all prime paths in directed graphs, a task central to structural testing of software. Existing approaches generate large numbers of invalid candidate paths before filtering, but this work derives non-trivial necessary conditions on valid path endpoints from the graph's strongly connected components. The characterization reduces the overall problem to enumerating constrained cycles in a specially augmented graph rather than all simple paths. A streaming algorithm then traverses this reduced space using Johnson-style search, pruning partial paths as soon as they cross SCC boundaries backward, and outputs valid prime paths incrementally.

Core claim

Prime paths admit a structural characterization in terms of strongly connected components that supplies complete necessary conditions on their endpoints; these conditions allow the generation task to be recast as constrained cycle enumeration inside an augmented graph, so that a streaming traversal can emit only feasible candidates without ever materializing the full set of simple paths.

What carries the argument

Structural characterization of prime paths in terms of strongly connected components, which supplies endpoint conditions and reduces generation to constrained cycle enumeration in an augmented graph.

Load-bearing premise

The structural characterization via strongly connected components supplies complete and correct necessary conditions that let the algorithm prune without missing any valid prime paths or emitting invalid ones.

What would settle it

On a small control-flow graph, exhaustively list every prime path by brute-force enumeration of simple paths and check whether the new algorithm produces exactly the same set with no omissions and no extras.

read the original abstract

Prime path coverage is a powerful structural testing criterion, but generating all prime paths in a directed graph remains computationally challenging due to the potentially exponential number of them. Existing approaches typically rely on enumerating large sets of candidate paths and filtering them, leading to high computational and memory overhead. In this paper, we present a new approach to prime path generation based on a structural characterization of prime paths in terms of strongly connected components. This characterization yields non-trivial necessary conditions for valid path endpoints and reduces the problem to constrained cycle enumeration in an augmented graph. As a result, we avoid explicitly enumerating all simple paths and instead generate only feasible candidates. Building on this insight, we design a streaming algorithm that outputs prime paths incrementally, using a Johnson-style traversal as a subroutine within a significantly reduced search space. The algorithm exploits SCC boundary crossings as natural pruning checkpoints - discarding partial paths the moment they are detected to be backward extendable, eliminating entire subtrees of the search space during traversal rather than filtering completed paths post hoc. We implement our method and evaluate it on a large dataset of real-world control-flow graphs extracted from open-source C++ and Python projects. The results demonstrate that our approach consistently outperforms existing methods, while maintaining stable inter-output delay in practice.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a practical SCC-boundary pruning trick inside a Johnson traversal to generate prime paths without full enumeration, but the completeness of that pruning is the part that needs checking.

read the letter

The main thing here is that the authors reduce prime path generation to constrained cycle enumeration in an augmented graph by deriving necessary endpoint conditions from the strongly connected components of the control-flow graph. This lets them prune partial paths the moment they cross an SCC boundary in a way that makes them backward-extendable, instead of generating candidates and filtering afterward. The streaming output is a useful detail for tools that need paths incrementally rather than all at once.

Referee Report

2 major / 2 minor

Summary. The paper claims a new SCC-based structural characterization of prime paths that supplies necessary conditions on endpoints, reduces generation to constrained cycle enumeration in an augmented graph, and supports a streaming Johnson-style traversal algorithm that prunes at SCC boundaries to avoid enumerating all simple paths or post-hoc filtering. Evaluation on real-world control-flow graphs from C++ and Python projects shows consistent outperformance over prior methods with stable inter-output delay.

Significance. If the SCC characterization is both sound and complete, the method would meaningfully advance prime-path coverage testing by replacing exponential enumeration-plus-filter pipelines with pruned traversal, offering practical gains for large CFGs. The streaming design and use of real-world datasets are strengths that support applicability claims.

major comments (2)

[§3] §3 (Structural Characterization): The necessary conditions derived from SCC boundaries for discarding backward-extendable prefixes must be shown to be complete; without an explicit argument or counter-example check that no valid prime path is missed when pruning intra-SCC cycles or cross-boundary prefixes, the claim of avoiding post-hoc filtering cannot be verified.
[§4] §4 (Augmented Graph and Constrained Enumeration): The reduction to cycle enumeration in the augmented graph assumes that every prime path corresponds exactly to a feasible cycle crossing SCCs as described; a formal equivalence proof or small-graph verification is needed to confirm the augmentation preserves all simple paths without introducing omissions or requiring later validation.

minor comments (2)

[Abstract] Abstract: The statement that the approach 'consistently outperforms existing methods' would be strengthened by including at least one quantitative metric (e.g., average speedup or memory reduction) rather than a qualitative claim.
[Evaluation] Evaluation section: Specify the exact baseline algorithms, graph sizes, and timeout thresholds used in the comparison to allow direct reproduction of the reported performance advantage.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on the soundness and completeness of our SCC-based characterization. We have revised the manuscript to include the requested formal arguments and verifications while preserving the core algorithmic contributions.

read point-by-point responses

Referee: [§3] §3 (Structural Characterization): The necessary conditions derived from SCC boundaries for discarding backward-extendable prefixes must be shown to be complete; without an explicit argument or counter-example check that no valid prime path is missed when pruning intra-SCC cycles or cross-boundary prefixes, the claim of avoiding post-hoc filtering cannot be verified.

Authors: We agree that an explicit completeness argument is required. The revised §3 now contains a proof by contradiction establishing that the SCC-derived necessary conditions are complete: any prime path satisfying the endpoint criteria cannot be incorrectly pruned, as doing so would imply a proper subpath is a cycle, violating the prime-path definition. We also added a small-graph verification (5-node example) confirming no valid prime paths are discarded by the intra-SCC or cross-boundary pruning rules. revision: yes
Referee: [§4] §4 (Augmented Graph and Constrained Enumeration): The reduction to cycle enumeration in the augmented graph assumes that every prime path corresponds exactly to a feasible cycle crossing SCCs as described; a formal equivalence proof or small-graph verification is needed to confirm the augmentation preserves all simple paths without introducing omissions or requiring later validation.

Authors: We acknowledge the need for a formal equivalence. The revised §4 includes a new theorem proving a bijection between prime paths in the original graph and feasible constrained cycles in the augmented graph. The proof shows that every prime path maps to a unique crossing cycle and vice versa, with no omissions or extraneous paths. We further provide explicit verification on the same small graphs used in §3 to confirm preservation of all valid paths. revision: yes

Circularity Check

0 steps flagged

No circularity: derivation rests on standard graph-theoretic properties

full rationale

The paper derives necessary conditions for prime-path endpoints directly from the definition of strongly connected components and the standard property that prime paths cannot be extended within an SCC. This is a one-way implication from graph structure to pruning rules, not a self-definition or fitted parameter renamed as prediction. No equations or claims reduce the output to the input by construction, and the abstract invokes no self-citations as load-bearing premises. The reduction to constrained cycle enumeration in an augmented graph follows from the same SCC boundary-crossing logic without circular closure.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the domain assumption that prime paths admit a complete structural characterization in terms of SCC boundaries that enables sound pruning; no free parameters or invented entities are introduced.

axioms (1)

domain assumption Prime paths admit a structural characterization in terms of strongly connected components that yields necessary conditions for valid endpoints
Invoked to justify the reduction to constrained cycle enumeration and the pruning checkpoints.

pith-pipeline@v0.9.0 · 5520 in / 1214 out tokens · 50724 ms · 2026-05-15T20:49:05.872890+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

This characterization yields non-trivial necessary conditions for valid path endpoints and reduces the problem to constrained cycle enumeration in an augmented graph... SCC boundary crossings as natural pruning checkpoints
IndisputableMonolith/Foundation/AlexanderDuality.lean alexander_duality_circle_linking unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Theorem 6... p is a prime path if and only if... simple cycle or V(p)⊆SCk or path in Cond(G)

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.