Exact Unary Interleaved Dyck

The Unary module contains exact algorithms for bidirected unary D1-interleaved-D1 reachability. The module name identifies the problem scope; AdaptiveSolver and FixedCounterSolver identify the algorithms.

Location: include/CFL/InterleavedDyck/Unary/, lib/CFL/InterleavedDyck/Unary/

Algorithms

AdaptiveSolver

Uses the adaptive two-arm construction. solve applies the shared quotient, decomposes it into weak components, and chooses K = 6 * n independently for each component of size n. Components are processed sequentially using quadratic finite control. solveShallow(graph, K) solves exactly inside min(counter1, counter2) <= K and preserves the caller’s K in every weak component without quotienting.

FixedCounterSolver

Implements Kjelstrøm and Pavlogiannis, POPL 2022 Algorithm 1. For n vertices in a processed weak component it stores one counter in states (v,j) for 0 <= j <= 18*n^2 + 6*n and leaves the other as a bidirected one-counter problem. It is the primary exact baseline for Adaptive.

Both algorithms share typed graph parsing, unary projection, input policy, quotient sparsification, and the bidirected-Dyck component backend. Singletons bypass lifted construction. Single-counter components use the ordinary Dyck backend directly, also for shallow queries: the unused counter stays zero.

Construction and performance

Sparsification belongs to preprocessing. On a unary input of N vertices and M arcs, its fixed two-label alphabet gives amortized O((N+M) alpha(N)) time and O(N+M) space. Hash-based unary projection before it takes expected O(N+M) time. A quotient of q vertices has at most 4q arcs: two possible closing targets per component, plus opening reverses. The implementation reuses the backend’s dense mapping and final functional closing lists, avoiding duplicate ID remapping and another scan of the original graph. Adaptive reuses those lists for its vertical parent map as well. Input reading itself requires Omega(N+M) work.

The solvers generate lifted transitions directly into the backend. Each undirected epsilon connection is emitted once and contracted before allocating closing-edge tables. The tables are indexed by compact epsilon components, not all lifted states. Final Dyck component IDs are dense; closing transitions that repeat the last target of a source/label list do not allocate pool entries.

Adaptive releases vertical state maps and parent data after labeling, releases sorting scratch before allocating the merge DSU, and constructs the horizontal arm only afterward. Counting-sort ranges use the height bound and compact component count. Both algorithms identify only the queried zero-state roots when producing their final vertex partitions.

For quotient weak-component sizes n_i, Adaptive’s finite control is O(sum n_i^2) and its running time is near-quadratic with union-find factors, plus preprocessing. FixedCounter retains O(sum n_i^3) finite control for mixed-counter components. Sequential workspace depends on the largest component. Without sparsification, Adaptive on n vertices and m arcs has construction cost O((n+m)(K+1)) up to union-find factors, so --direct with K=6n can still take cubic time on dense input.

stats().execution provides phase microseconds, weak-component sizes, fast-path counts and estimated peak construction payload. Adaptive also reports vertical, horizontal and merge times. Backend counters distinguish generated, stored and scanned closing edges and compact epsilon-component counts. State/arc counters sum actual mixed-component work, while full-solve bounds are maxima across those components; shallow queries report the supplied K. Payload estimates exclude input/component graphs, final output maps and allocator overhead. --stats additionally reports process peak RSS on macOS/Linux, including parsing and allocator retention, rather than presenting that high-water mark as per-phase memory.

Exactness and directed input

Every projected arc must have its complement-labeled reverse. Parenthesis IDs project to counter 1 and bracket IDs to counter 2. Exactness concerns balanced paths between zero-counter configurations; it does not extend to multi-type D_k-interleaved-D_k.

Both option types default to RequireBidirected. The alternative AddMissingReverseEdges is exact for the resulting symmetrized graph and a sound overapproximation for the original directed graph. The parser itself never adds reverse edges.

#include "CFL/InterleavedDyck/Core/Graph.h"
#include "CFL/InterleavedDyck/Unary/Solver.h"

using namespace lotus::cfl;

interleaved_dyck::Graph graph =
    interleaved_dyck::Graph::parseDotFile("bidirected.dot");
auto adaptive = interleaved_dyck::unary::AdaptiveSolver{}.solve(graph);
auto fixed = interleaved_dyck::unary::FixedCounterSolver{}.solve(graph);

Command line

cmake --build build --target lotus-cfl-interleaved-dyck-unary
build/bin/lotus-cfl-interleaved-dyck-unary --algorithm adaptive --stats bidirected.dot
build/bin/lotus-cfl-interleaved-dyck-unary --algorithm fixed-counter --stats bidirected.dot

--direct disables shared quotient sparsification. --shallow K applies only to Adaptive. --bidirect explicitly selects symmetrization, and output states the selected algorithm and resulting guarantee. --print-pairs groups vertices by component and streams non-reflexive pairs in O(|V| + output) time; it does not scan every unrelated vertex pair.

The existing benchmarks/real-world/CFL/InterleavedDyck corpus is directed, so exact runs require a genuinely bidirected corpus. Using --bidirect on that corpus must be reported as an overapproximate experiment.

Build and test

cmake --build build --target interleaved_dyck_unary_test
ctest --test-dir build -R interleaved_dyck_unary_test --output-on-failure