Polynomial-Delay Enumeration of Fixed-Endpoint Vertex-Regular Paths in Skew-Symmetric Digraphs

Abstract

Let G = (V, E) be a finite skew-symmetric digraph with fixed-point-free involution v ↦ v̄. A directed path is vertex-regular if it contains no pair v, v̄. For prescribed vertices s, t, we give a depth-first algorithm that enumerates every vertex-regular s–t path exactly once with delay O(n²(n + m)) and polynomial space. Its extension test deletes the vertices of the current prefix and their complements and invokes linear-time regular reachability, obtained from the arc-regular algorithm of Goldberg and Karzanov by vertex splitting. This establishes the fixed-endpoint variant needed for the two-unit-clause consequence stated after Conjecture 8.1 of Kullmann and Clewer. Via their regular-path bijection, it also yields O(ℓ(F)³)-delay enumeration of the minimally unsatisfiable subsets of a 2-CNF containing two prescribed distinct unit clauses. An executable implementation and a Lean companion checking the vertex-splitting model interface and key prefix-oracle lemmas accompany the note.