Source-linked AI summary
Network Coding Can Beat Routing in Undirected Multiple-Unicast Networks
Xindan Zhang, Baochun Li, Zongpeng Li
TL;DR
Whether coding can outperform fractional routing in undirected multiple-unicast networks remained unresolved beyond special classes. This paper converts a short code into a reversible computation and a wire network with a strict routing certificate. It proves a finite separation and extends the advantage to high-girth network families.
Problem
Whether network coding can raise achievable rates above fractional routing in undirected multiple-unicast networks remained open in general despite results for special classes.
Source: §I · p. 1Method
The paper turns a short completion-time code into a reversible computation, makes every register a unicast demand, and uses a temporal metric on the resulting wire graph to bound routing.
Source: §I · p. 2, B. Constructing the seed and its… · p. 15Results
A finite subcubic network has a binary linear block code with common rate strictly above fractional routing, and amplified families have routing bounded by K_β/(log n)^c while coding approaches rate one.
Source: §I · pp. 1, 3Takeaways & Limitations
The integer construction works over every finite field and nontrivial finite abelian group, and its deterministic fixed-schedule common-rate supremum is one.
Source: §I · p. 2
Abstract
from arXiv · showhide
Network coding lets the nodes of a network combine messages rather than merely forward them. In undirected networks, where the two directions of an edge share its capacity, Li and Li conjectured in 2004 that coding offers no advantage over fractional routing; the conjecture has been confirmed for many special classes but never settled in general. In this paper, we disprove it by constructing a finite connected simple undirected network with unit shared edge capacities, maximum degree three, and distinct leaf terminals, on which a binary linear block code achieves a common rate strictly above the maximum fractional routing rate. The construction turns a short completion-time code into a reversible circuit whose registers all carry independent messages, and a temporal metric on its wires yields the strict routing bound. The underlying integer-coefficient construction works over every finite field and every nontrivial finite abelian group; for deterministic fixed-schedule codes the common-rate supremum is one and the closure of the rate region is the unit cube. Amplifying the gap with a degree-preserving tensor construction and an even subdivision gives, for every $0<\beta<1$, an unbounded family of connected, simple, subcubic, bipartite networks with girth at least $n^\beta$ on which coding approaches rate one while routing is bounded by $K_\beta/(\log n)^c$, with one positive exponent $c$ independent of $\beta$. The finite counterexample and the family theorem are formalized in Lean.
I. INTRODUCTION
The paper asks whether coding can outperform fractional routing in undirected multiple-unicast networks, a conjecture previously confirmed only for special classes. It gives a finite counterexample and develops a construction whose coding advantage extends across alphabets and to high-girth subcubic families.
I. INTRODUCTION
- The conjecture had held for many special network classes, while general bounds allowed coding to exceed routing by at most a logarithmic factor in the number of sessions.Before this work, whether coding helps at all for undirected unicast sessions remained open.Source: §I · p. 1
- A finite connected simple network with unit shared capacities, degree at most three, and distinct leaf terminals admits a binary linear block code whose common rate exceeds fractional routing.The separation holds at a finite block length and places the example outside the previously listed classes.Source: §I · pp. 1–2
- The construction converts a short completion-time code into a reversible computation, makes every register an independent demand, and pipelines one-use executions to beat the routing bound.A temporal metric charges the designated demands more distance than the total wire budget can support at rate one.Source: §I · p. 2
- The integer construction works over every finite field and every nontrivial finite abelian group; its deterministic fixed-schedule common-rate supremum is one, with rate-region closure equal to the unit cube.For every 0 < β < 1, the paper also constructs unbounded connected, simple, subcubic bipartite families of girth at least n^β, with routing bounded by K_β/(log n)^c and coding approaching rate one.Source: §I · pp. 2–3
A. Coding protocols and normalized rates
- The model uses finite undirected graphs with unit edge capacity shared by both directions, while fixed-schedule protocols require causal transmissions and exact sink decoding.For finite fields, linear protocols restrict local encoding and decoding to linear maps; integer-coefficient identities also interpret in the stated groups and fields.Source: §II · p. 3, A. Coding protocols and normalized rates · p. 3
B. Fractional routing and distance certificates
- Fractional routing assigns nonnegative real weights to simple paths, with both directions counted against each edge’s shared capacity; the paper’s distance certificates bound all such routings.Allowing walks does not change the maximum, since repeated-vertex portions can be deleted without increasing edge loads.Source: B. Fractional routing and distance… · p. 3
III. A FINITE COUNTEREXAMPLE
The finite counterexample is built by combining an integer completion-time code with a strict distance certificate. The auxiliary construction uses recursive composition and a colored cover to preserve a short code while increasing deleted-edge distances.
III. A FINITE COUNTEREXAMPLE
- A finite connected simple undirected network with unit shared capacities, maximum degree three, and distinct leaf terminals has a causal binary linear code whose rate exceeds maximum fractional routing.The theorem supplies positive integers B and D such that the code delivers B symbols per session in D rounds and B/D > Rroute(G).Source: §III · p. 4
- The construction obtains a short auxiliary code, implements it reversibly, turns every register into a unicast demand, and normalizes a strict routing certificate.The scalar-instance template combines bounded degree, distinct leaf terminals, long own-pair walks, and a one-use integer code.Source: §III · p. 4
A. The auxiliary completion-time code
- The auxiliary graph has many demands, a small cut set, and a code short relative to own-pair distances after deleting that set.Its seed uses h = 3 and u = 58; the displayed elementary gadget sends in three rounds and has distance five from each own pair after deleting its central edge.Source: A. The auxiliary completion-time code · pp. 4–5
- For every h ≥ 0 and rational u ≥ 5, the integer completion-time construction yields a finite connected loopless multigraph with distinct terminals and a nonempty cut set.The code duration is 32h under one symbol per direction per round, or T = 2 · 32h under a shared unit budget.Source: A. The auxiliary completion-time code · p. 4
- Recursive composition simulates each outer round with an inner execution, multiplying code times and deleted distances while maintaining the target demand-to-cut ratio.A colored high-girth incidence cover assigns inner sessions to outer edge directions and prevents short routes from bypassing them.Source: A. The auxiliary completion-time code · p. 4
B. A reversible integer circuit
The section simulates an integer communication code with a reversible circuit, then turns its registers and gates into a wire graph whose temporal routing certificate yields a strict distance bound.
B. A reversible integer circuit
- Fresh sender and receiver registers let each event copy its prepared payload across its edge, and the sink decoders recover every source coordinate on the simulated execution.The identity is first established with zero workspace; the next construction removes the need to initialize the final network’s workspace.Source: B. A reversible integer circuit · p. 5
- The compute-copy-uncompute sequence adds the source into the sink bank while restoring every workspace coordinate, regardless of its initial value.The construction uses a forward shear, its inverse transpose, and the forward shear again; local output signs recover the exchanged input.Source: B. A reversible integer circuit · p. 5
- The resulting circuit permutes all registers with output signs and uses at most 12T cross phases and 12Tf cross gates on the f cut edges.The phase structure preserves disjoint register pairs and the one-use-per-physical-edge restriction.Source: B. A reversible integer circuit · p. 5
C. The wire graph and its routing certificate
- Each register becomes a demand on its strand wires, and splitting each gate into two degree-three vertices makes the physical graph’s edges undirected with shared unit capacity.The wire graph initially may have parallel edges and degree four; unused registers receive direct input-to-output wires.Source: C. The wire graph and its routing… · p. 5, Figure 2 · p. 6
- Wire spans telescope to a baseline cost of M + 1 for every input-output walk, while any backward wire raises the cost to at least M + 3.The temporal labels are zero at inputs, the gate number at each gate, and M + 1 at outputs.Source: C. The wire graph and its routing… · p. 6
- A forward path for a designated source-sink demand must cross the cut set and incur a marked-port penalty, yielding distance bounds that certify a routing ceiling below one.The bounds give hj = M + 1 for register demands and hj = M + 3 for the k designated demands; the workspace demands preserve the baseline equality used in the certificate.Source: C. The wire graph and its routing… · p. 6
D. A connected subcubic scalar instance
The construction converts the split-graph certificate into a connected, simple, subcubic scalar instance with positive lengths and a hop-distance routing bound, then obtains a seed independent of alphabet choice.
D. A connected subcubic scalar instance
- Splitting each gate yields a simple graph with degree-three gate vertices, distinct leaf terminals, and an explicit scalar schedule that uses every edge once.The internal edge is sent before the outgoing strand wires, so the control and target symbols are available when needed.Source: D. A connected subcubic scalar instance · p. 6
- The split graph’s certificate has zero-length edges and may be disconnected, so the construction replaces it with a connected certificate having positive integer lengths and own-pair lower bounds.Length and demand scaling preserves path bounds and the positive surplus.Source: D. A connected subcubic scalar instance · pp. 6–7
- Restricting to a component with positive budget-demand difference preserves exact decoding, strict causality, locality, and the graph’s simplicity and degree bounds.Exact decoding requires each demanded source and sink to lie in the same component.Source: D. A connected subcubic scalar instance · p. 7
- Hop normalization produces a scalar instance with ρ < 1, and the resulting seed graph, schedule, and integer coefficients are chosen without selecting a field or group.The construction uses finite graph operations and integer row identities.Source: D. A connected subcubic scalar instance · p. 7
E. A finite block above the routing ceiling
A one-round-spaced pipeline turns the scalar routing certificate into a finite binary linear block code above the routing ceiling. The same integer construction also establishes alphabet-independent coding rates and rate-region results.
E. A finite block above the routing ceiling
- Starting independent scalar executions one round apart delivers B symbols per session in B + T rounds while using each edge at distinct times across blocks.Within each block, predecessors remain strictly earlier, and local expressions use only that block’s coordinates.Source: E. A finite block above the routing… · p. 7
- The finite binary block protocol delivers every session at a common rate strictly above the best possible fractional routing rate.The proof chooses a finite pipeline length from the strict certificate m0 < k0b0 and interprets the integer coefficients in F2.Source: E. A finite block above the routing… · pp. 7–8
IV. ALPHABET-UNIFORM CODING AND CAPACITY REGIONS
- The same integer instructions separate coding from routing over every nontrivial finite abelian group and every finite field, where the codes are linear.The graph, schedule, and coefficients do not depend on the alphabet.Source: §IV · p. 8
- For deterministic fixed-schedule codes over nontrivial finite abelian groups, the common-rate supremum is one and the closure of the symbol and field-linear vector regions is [0, 1]^k.The leaf bound limits each coordinate to one, while the pipeline supplies rates approaching one and vectors approaching every point of the cube.Source: §IV · p. 8
- At finite block length, exact deterministic fixed-schedule group codes and field-linear codes attain precisely the rational rate vectors in [0, 1)^k.Rate one is not attained by a finite block, although every rational vector below one is attainable.Source: §IV · p. 8
V. POLYLOGARITHMIC GAP AMPLIFICATION
The gap amplification composes scalar instances through a colored incidence cover while retaining the integer code and structural constraints. The tensor construction specifies how outer edges are replaced by inner copies and preserves connectivity, subcubic degree, and leaf terminals.
V. POLYLOGARITHMIC GAP AMPLIFICATION
- The tensor construction specializes the BGS principle to retain the integer local code, degree bound, and leaf terminals, with a colored high-girth incidence cover specifying attachments.The recursive product replaces directed uses of retained outer edges with inner-copy sessions; code times and deleted distances multiply while the target ratio is maintained.Source: §V · p. 8
A. The degree-preserving tensor construction
- Each incidence attaches an inner source and sink to an outer edge’s tail and head, respectively; the old outer edges are removed while inner physical edges remain.Outer terminal pairs become the new demands, and incidences determine which inner session serves each outer copy.Source: A. The degree-preserving tensor… · p. 9, Figure 3 · p. 9
- The attachment identifies terminal stars at outer vertices without merging distinct outer vertices, and the resulting graph is simple and connected.The inner-copy vertex maps are injective, and connectivity follows because each inner copy connects the ends of the outer edge it replaces.Source: A. The degree-preserving tensor… · p. 9
- Replacing each outer incident edge with one inner leaf edge preserves outer degrees, maximum degree three, and distinct leaf terminals.Inner nonterminals retain their old degrees, and every retained edge has a nonterminal endpoint.Source: A. The degree-preserving tensor… · p. 9
B. The composed code and its distance bound
The tensor construction composes inner and outer schedules into an exact integer scalar code, with every new edge used once and duration T1T2. Its distance bound multiplies across tensor factors, and iterating the construction yields unbounded vertex counts.
B. The composed code and its distance bound
- Synchronizing each inner copy to its outer edge-color time lets its decoder feed the outer decoders, yielding an exact integer scalar code of duration T1T2 that uses each new edge once.Each inner copy executes once; outer predecessors finish in earlier intervals and inner predecessors remain earlier within an interval.Source: B. The composed code and its distance… · p. 9
- Every undirected own-pair walk in the tensor graph has at least b1b2 edges.The proof bounds walks through cycles using the cover girth and walks through trees using nested excursions.Source: B. The composed code and its distance… · pp. 9–10
C. Iteration and the logarithmic gap
- Repeatedly tensoring the seed with itself yields unbounded vertex counts; each shortest own-pair path is at least bj edges and at most vj − 1.The passage also establishes b0 > 2.Source: C. Iteration and the logarithmic gap · p. 10
VI. BIPARTITE FAMILIES WITH POLYNOMIAL GIRTH
Subdivision addresses the gap between incidence girth and physical girth while preserving the scalar coding ceiling. Even replacement lengths make the resulting graph bipartite, and replacement length controls cycle lengths.
VI. BIPARTITE FAMILIES WITH POLYNOMIAL GIRTH
- Incidence girth controls source–sink distances but not physical cycles inside inner copies; subdivision raises physical girth and even replacement lengths ensure bipartiteness.A suitable replacement length raises physical girth to a power of the new vertex count.Source: §VI · p. 10
A. Subdividing the physical edges
- Replacing each edge by a private path of λ ≥ 2 edges preserves the ceiling m′/(kb′) = m/(kb), makes every cycle at least λ edges, and yields a bipartite graph when λ is even.The replacement preserves simplicity, connectivity, degree bounds, and leaf terminals.Source: A. Subdividing the physical edges · p. 10
- The relay schedule gives an exact scalar code using each new edge once, with duration T(mλ + 1); terminal-to-terminal path distances gain a factor λ.The new edges have private interior endpoints.Source: A. Subdividing the physical edges · p. 10
B. The simultaneous family theorem
Theorem VI.2 gives unbounded families of connected, simple, undirected, bipartite subcubic networks with growing girth and exact causal integer-coefficient block protocols. The same families support coding-rate and routing-separation results across the stated alphabets.
B. The simultaneous family theorem
- For every β in (0, 1), the theorem gives networks with more than j vertices, shared unit edge capacities, degree at most three, and pairwise distinct leaf terminals.The networks are connected, simple, undirected, and bipartite.Source: B. The simultaneous family theorem · p. 10
- Every cycle in G_j has at least n_j^β edges, while the corresponding protocol delivers B symbols per session in B + T′_j rounds for every positive integer B.The subdivision construction preserves the routing ceiling ρ_j.Source: B. The simultaneous family theorem · pp. 10–11
- For every nontrivial finite abelian group and every finite field, the common-rate supremum on G_j is one and the rate-region closure is [0, 1]^k_j.The graph, schedule, and integer coefficients are chosen independently of the alphabet.Source: B. The simultaneous family theorem · p. 11
- For some positive integer B, the protocol has common rate B/(B + T′_j), strictly above the routing ceiling ρ_j and hence above Rroute(G_j).The routing ceiling is retained under the subdivision.Source: B. The simultaneous family theorem · p. 11
- A longer subdivision yields a single family with near-linear girth, at the cost of halving the exponent.The corollary states that its cycle-length bound holds for each fixed β < 1 for sufficiently large family members.Source: B. The simultaneous family theorem · p. 11
VII. CONCLUDING REMARKS
The paper shows that coding can outperform fractional routing in undirected multiple-unicast networks, using a reversible circuit whose registers all carry demands. It extends the separation across alphabets and to high-girth network families, while leaving the size of the finite instance’s advantage unresolved.
VII. CONCLUDING REMARKS
- The reversible-circuit construction makes every register, including workspace, carry a unicast demand; temporal wire lengths then yield a strict routing bound while the code pipelines toward rate one.The total wire length equals the total baseline distance of all demands, and designated demands tip the balance against routing.Source: §VII · p. 12
- The same integer instructions work over every finite field and nontrivial finite abelian group, and the tensor construction with subdivision yields subcubic bipartite families with girth at least n^β for every 0 < β < 1.The construction also gives a single family with girth n^(1−o(1)); the finite counterexample and family theorem are formalized in Lean.Source: §VII · p. 12
- The true routing advantage of the finite instance remains unknown because its certificate bounds the routing rate only from above.The paper also leaves open whether the O(log k) upper bound is attained and whether a smaller counterexample exists.Source: §VII · p. 12
APPENDIX A FINITE COLORED COVERS
This material establishes finite high-girth colored covers and develops the auxiliary input and recursive physical product used in the construction. It also gives a base graph with an exact integer code and a deleted-edge distance bound.
APPENDIX A FINITE COLORED COVERS
- A finite colored cover of maximum degree μ and girth greater than g is obtained by extremizing girth and shortest-cycle count, then switching a distant matching edge to eliminate a shortest cycle.A neighborhood bound supplies the distant edge; taking a nonempty connected component preserves the matching conditions and girth bound.Source: Appendix A · p. 12
APPENDIX B THE RECURSIVE AUXILIARY INPUT
- The auxiliary-input proof adapts the base and recursive substitution of HWZ while retaining the integer decoding identities and exact counts needed by the reversible compiler.Source: Appendix B · p. 12
A. Base graph and exact local formulas
- The base graph is finite, connected, and loopless with distinct terminals, and its three-round protocol decodes exactly over arbitrary additive abelian groups.The deleted own-pair distance is exactly five; cycle erasure extends the lower bound to all walks.Source: A. Base graph and exact local formulas · p. 12
B. The recursive physical product
- The recursive physical product attaches inner copies to outer arcs through a connected colored cover, deletes noncut outer edges, and replaces cut edges with private paths.Its edge count is m+ = a2 nL f1 + nR m2; the construction preserves connectivity.Source: B. The recursive physical product · p. 13
C. Causal integer composition
The product composes integer protocols while preserving causality and exact decoding, then serializes the result to respect shared undirected edge capacity. Its distance proof handles both cyclic and tree-supported incidence traces to establish a product lower bound.
C. Causal integer composition
- Each outer-round payload is executed by an inner copy while cut-edge payloads are relayed along replacement paths, preserving strict local causality and exact decoding.Disjoint physical edge identities respect the full-duplex budget, and the composed code duration is a+ = a1a2.Source: C. Causal integer composition · p. 13
D. Maintaining the session-to-cut ratio
- The recursive session-to-cut ratio remains at least the target u, while the parameter U+ stays at least three and duration and distance bounds square at each step.The resulting bounds are 32^(h+1) for duration and 5^(2^(h+1)) for distance.Source: D. Maintaining the session-to-cut ratio · p. 13
E. One final serialization
- After the recursion, each full-duplex round is serialized into reference and reverse-direction subrounds, maintaining strict causality and at most one symbol per edge per subround.Source: E. One final serialization · p. 13
A. Lifting a quotient path
- To bound physical route length, the proof lifts an arbitrary walk through zero-length connectors, erases cycles, and traces connector crossings in the incidence cover.Physical inner edges count toward route length; incidence edges encode attachments rather than hops.Source: Appendix C · p. 14, A. Lifting a quotient path · p. 14
B. A cyclic incidence trace
- If the incidence-trace support contains a cycle, its girth forces at least 2b1b2 connector crossings and hence physical length at least b1b2.The argument permits backtracking and repeated visits to copies.Source: B. A cyclic incidence trace · p. 14
C. A tree-supported incidence trace
- For a tree-supported trace, paired connector crossings form nested excursions; induction gives each inner excursion cost at least b2, and root excursions then yield total physical length at least b1b2.The induction uses distinct outer endpoints without assuming they form a demanded pair.Source: C. A tree-supported incidence trace · p. 14
D. Application with deleted edges
This material applies the distance argument after deleting cut edges and describes the formal representations and proof pipeline. The Lean development checks the constructed seed, amplified families, and verification claims against the paper’s communication models.
D. Application with deleted edges
- The deleted-edge distance proof removes excursions into cut-path stubs and applies the incidence-excursion argument to the remaining inner graphs and noncut outer edges.It covers arbitrary undirected walks, including reverse edge uses and routes unrelated to the coding schedule.Source: D. Application with deleted edges · p. 14
APPENDIX D ORGANIZATION OF THE LEAN PROOF
- The formalization represents a finite network with endpoint-labeled edges and checks that the mathematical communication-model interpretation follows from those representations and operational arguments.Source: Appendix D · p. 15, D. What the verification establishes · p. 16
A. Representing the network and the two communication models
- The formalization represents networks, protocols, and routing separately, recording shared edge-round capacity, strict causality, local decoding, and integer-row identities.Evaluating the identities over additive abelian groups gives valid symbol operations; over fields they are linear maps.Source: A. Representing the network and the… · p. 15
B. Constructing the seed and its certificate
- The seed construction combines an auxiliary graph and integer code with a reversible compiler, then constructs register strands whose temporal metric yields a strict integer routing surplus.Subsequent normalization and a block pipeline turn that surplus into a finite rate comparison and a binary-field counterexample.Source: B. Constructing the seed and its… · p. 15
- Some finite choices, including component and cover selection, use classical existence arguments, although their cardinalities and durations are derived from the construction.Source: B. Constructing the seed and its… · p. 16
C. Composing the amplified family
- The tensor operation preserves graph and code properties through iteration, and even subdivision supplies bipartiteness and a cycle-length lower bound for the amplified family.The formalized family theorem also establishes coding-capacity and rate-region results for each scalar instance.Source: C. Composing the amplified family · p. 16
D. What the verification establishes
- The development builds without errors, uses only Lean’s standard axioms, and passes a fresh-environment re-check by the same Lean kernel.The audit covered 2,472 declarations and 1,755 theorems; the re-check was not by an independent verifier.Source: D. What the verification establishes · p. 16