Graph Theory

Motivation

Supply-chain traceability depends on firms adopting a technology together. A firm may benefit only after enough other firms in a shared supply chain have adopted; a supply chain may in turn become traceable only when a threshold number of its firms participate. Selecting firms to seed therefore couples many local adoption decisions. Blaettchen, Calmon, and Hall model this coupling as a network diffusion problem and ask for a least-cost seed set that eventually activates every firm Blaettchen, Calmon, and Hall, 2024. Their model permits overlapping supply chains and firm-specific benefits and costs, so it describes more than a single threshold rule on an ordinary graph.

The paper establishes an exact linear programming reformulation whose size depends exponentially on treewidth but only linearly on the numbers of firms and supply chains, up to parameter factors Theorem 2. This mission records that mathematical claim as a cost-independent extended formulation, together with source propositions describing the diffusion correspondence and the first binary formulation.

Setting

Let $N_F$ contain $n$ firms and let $N_{SC}$ contain $m$ supply chains. Supply chain $j$ comprises the hyperedge $e_j\subseteq N_F$. Firm $i$ has an adoption cost $c_i>0$ and receives a nonnegative integral benefit $r_{ji}$ from an incident supply chain $j$ once enough of that chain's firms are active. The chain's threshold satisfies $2\le\theta_j\le|e_j|$. The paper assumes that each firm's total incident benefit can cover its adoption cost. A seed set $S_0$ is active at time zero; every later set $S_t$ retains the already active firms and adds a firm $i$ when

$$c_i\le\sum_{j:\ i\in e_j,\ |S_t\cap e_j|\ge\theta_j-1}r_{ji}.$$

A seed set fully activates the network if $S_t=N_F$ at some finite time. Given real seeding costs $w_i$, the optimization value is

$$\operatorname{OPT}(w)=\min\left\{\sum_{i\in S}w_i:S\subseteq N_F\text{ fully activates the network}\right\}.\tag{1}$$

The auxiliary graph $G'$ has a firm vertex for each $i$ and a supply-chain vertex for each $j$, joined when $i\in e_j$. Its directed weighted version sends weight $1$ from a firm to a supply-chain vertex and weight $r_{ji}$ in the reverse direction. Firm thresholds are $c_i$; supply-chain thresholds are $\theta_j-1$. A weighted linear-threshold update activates vertices whose total incoming weight from active vertices reaches their threshold. Proposition 1 identifies the firms active after $t$ original steps with those active after $2t$ auxiliary-graph steps Proposition 1, p. 10.

A tree decomposition is a tree of vertex bags that covers every vertex, places each graph edge or hyperedge in a bag, and keeps the bags containing one vertex connected along the tree. Its width is the largest bag size minus one. Write $\omega$ for an upper bound on the treewidth of the original hypergraph and $\vartheta_{\max}=\max(\max_i c_i,\max_j(\theta_j-1))$ Definition 2, p. 13; Proposition 9, p. 18.

Formalization targets

Exact LP reformulation

The target is one finite linear system $Az\ge b$, where $z=(x,y)$ has visible seed coordinates $x\in\mathbb R^n$ and auxiliary coordinates $y$. The system is chosen from the adoption instance and is independent of $w$. Its projection onto $x$ is exactly the convex hull of fully activating seed indicators:

$$\operatorname{proj}_x\{(x,y):Az\ge b\}=\operatorname{conv}\{\mathbf1_S:S\text{ fully activates}\}.$$

Consequently, minimizing $\sum_iw_ix_i$ over the same LP yields $\operatorname{OPT}(w)$ for every real $w$. One absolute constant $C>0$, placed before all instances and treewidth parameters, bounds the total number of variables and constraints by

$$2^{C(\omega+1)^2}(\vartheta_{\max}+1)^{C(\omega+1)}C(n+m+1).$$

This is the $2^{O(\omega^2)}\vartheta_{\max}^{O(\omega)}O(n+m)$ form stated immediately after Theorem 2 p. 18. The source's more detailed displayed bracket is not used as the target because its fixed exponents do not match the asymptotic bound obtained from the propositions cited in the proof.

Supporting results

The milestones follow the proof of Theorem 2 on p. 41. Proposition 1 and Corollary 1 identify the adoption process with a weighted threshold process on $G'$. Proposition 5 gives a binary program (4) whose feasible seed vectors are exactly the fully activating seed sets. Proposition 7 replaces its global acyclicity constraints by constraints inside the bags of a tree decomposition of $G'$, formulation (5). Proposition 8 splits the long covering constraints of (5) into partial sums along a rooted binary decomposition, formulation (10). Proposition 9 bounds the treewidth of the intersection graph of (10) by $O(\omega'^2+\omega'\log_2\vartheta_{\max})$, where $\omega'$ is the width of the decomposition of $G'$. Proposition 3 gives $\operatorname{tw}(G')\le\operatorname{tw}(G)+1$, and Proposition 4 is the bounded-treewidth LP theorem for binary programs pp. 10–18.

Significance

An exact LP gives the same optimum for every seeding-cost vector while keeping the constraints fixed. The size guarantee explains why a structurally sparse supply-chain network can admit a formulation far smaller than a generic enumeration of seed sets. It also separates the economics of choosing $w$ from the combinatorics of diffusion: once the network formulation is built, different cost scenarios use the same feasible region Theorem 2 and §5.3.

The paper proves the theorem, citing Proposition 4 from Laurent (2009) and Bienstock and Muñoz (2018). Neither Theorem 2 nor Proposition 4 has a machine-checked proof on Prove2Me. The remaining work is to formalize the paper's chain of reformulations and the cited LP theorem. The tree decomposition definitions are already published as reusable Prove2Me objects from Robertson and Seymour. The diffusion model, the binary formulation, and their relationship to an LP extended formulation are the new formal objects here.

Difficulty

The first binary program represents the activation order but connects variables across many firm–supply-chain pairs. Its intersection graph has treewidth at least $nm-1$, even when the underlying supply-chain graph is sparse Proposition 6, p. 16. Applying a bounded-treewidth LP theorem directly to that program therefore loses the desired parameter bound. The source introduces a more local formulation tied to a tree decomposition, and controlling the intersection graph of that formulation is the central difficulty. Formulation (10) as printed is not exactly right: the bit count (6) is one bit short, so that an instance with $c_1=2$ loses its optimal seed set, and the root inequalities (10c), (10g) use an undeclared variable. The targets use the bit ranges of the integer program (11) in the proof of Proposition 8 and the partial sum $u$ at each subtree root.

Formalization scope

The Lean instance uses Fin n for firms, Fin m for supply chains, and natural numbers for benefits, adoption costs, and thresholds. The auxiliary graph is a simple graph on the disjoint union of these two finite types; the diffusion update retains active vertices and uses the paper's weak inequality at the threshold. Hypergraph treewidth requires every entire hyperedge in some bag and uses the published Robertson–Seymour tree decomposition predicate for the primal graph. Graph treewidth for $G'$ uses the corresponding published bound predicate.

The paper treats connectedness as without loss of generality. Here it means that the incidence graph $G'$ is connected and is included with the other standing assumptions. The gcd normalization discussed in §3.1 is a preprocessing convention, not a hypothesis. The finite family of successful seed sets always contains the all-firm set, so OPT is a genuine finite minimum. The formulation counts both auxiliary variables and inequalities. The additive shifts in the size bound handle small values of $n$, $m$, $\omega$, and $\vartheta_{\max}$; they do not change the asymptotic claim. The LP is quantified before $w$, and its projection is specified, excluding a trivial LP selected separately for each cost vector.

Formulations (4), (5) and (10) are binary feasibility predicates over natural-number variables bounded by one; the adoption inequality $c_i(1-s_i)\le\cdots$ is written as $c_i\le\cdots+c_is_i$. Constraints (5c), (5d), (10i), (10j) range over distinct vertices of a bag (with $i=j$ the printed (5c) would be infeasible). A rooted binary tree decomposition is a published tree decomposition together with a root, a parent map and at most two children per node; the subtree root $z_0^p$ is the node of the subtree nearest the root. The partitions $J^i_z$, $I^j_z$ are arbitrary data with the properties stated on p. 17, which are all the proofs use. Proposition 7 is stated for every tree decomposition of $G'$; binarity is not needed there.

The generic finite linear-system and intersection-graph definitions can be reused beyond this paper. Contributions are welcome at every milestone; Proposition 4 is a general result on binary programs and is the most widely reusable.

Selected references

• Paul Blaettchen, André P. Calmon, and George Hall, Traceability Technology Adoption in Supply Chain Networks, Management Science, 2024; preprint arXiv:2104.14818v4 (2023). arXiv
• Neil Robertson and Paul D. Seymour, Graph Minors. V. Excluding a Planar Graph, Journal of Combinatorial Theory, Series B 41, 1986. DOI
• Monique Laurent, Sums of Squares, Moment Matrices and Optimization over Polynomials, in Emerging Applications of Algebraic Geometry, IMA Vol. 149, Springer, 2009. DOI
• Daniel Bienstock and Gonzalo Muñoz, LP Formulations for Polynomial Optimization Problems, SIAM Journal on Optimization 28(2), 2018. DOI

Motivation

In atomic dynamic routing, indivisible agents (vehicles, packets, travellers) enter a network over time and travel along fixed routes. Each road admits a limited number of agents per unit of time, so agents queue at its entrance. A basic question for traffic models, packet-switching networks and dynamic routing games is how long an agent can stay in the network, its residence time. Upper bounds on residence times are what make it possible to bound queue lengths and the price of anarchy in dynamic routing games.

Greedy packet scheduling, where an edge never idles while packets wait for it, was studied by Cidon, Kutten, Mansour and Peleg (SIAM J. Comput. 1995), who showed that cycles can make delays large, and by Mansour and Patt-Shamir (J. Algorithms 1993), who bounded delivery times when every route is a shortest path. Cao, Chen, Chen and Wang (MOR 2022) prove a bound for arbitrary routes on acyclic networks. It holds under any rule that decides which waiting agent may leave next, and agents may keep entering forever. Their Theorem 1 is the goal of this mission. The paper then uses it to show that equilibria of three dynamic routing games on series-parallel networks have bounded queues (§6).

Setting

A network $G=(V,E)$ is a finite directed multigraph (parallel edges allowed) that is acyclic. Every edge has unit length and unit capacity. A path is a sequence of edges, each starting where the previous one ends. $L_{vw}$ is the number of edges of a longest $v$-$w$ path.

Time is discrete, $0,1,2,\dots$. Agents form a set $\Delta$, possibly infinite. At each time finitely many agents enter. Agent $i$ enters at time $r_i$ at his origin $o_i$ and follows a fixed route, a nonempty $o_i$-$d_i$ path. The tail of each edge holds a buffer. Two rules govern the dynamics:

• (A1) an agent reaching a vertex that is not his destination enters the buffer of his next edge at once;
• (A2) at every integer time, whenever a buffer is nonempty, exactly one agent leaves it and reaches the head of the edge one time unit later; the others wait.

No rule says which agent leaves. Every choice consistent with (A2) is an admissible run. An agent exits $G$ on reaching his destination. His residence time is his exit time minus his entry time (Definition 1).

Fix a focal agent $\zeta$ with entry time $r$. $G_\zeta$ is the subnetwork formed by all $o_\zeta$-$d_\zeta$ paths. For an integer time $r_0$:

• $A_{\zeta,p}$ is the set of agents who enter after time $r$ and use an edge of $G_\zeta$;
• $B_{\zeta,p}(r_0)$ is the set of agents $i\neq\zeta$ who entered by time $r$, are still inside $G$ at time $r_0$, and use an edge of $G_\zeta$.

An agent exits $G_\zeta$ when he reaches the head of the last edge of his route lying in $G_\zeta$.

Formalization targets

Goal: Theorem 1 (p. 7)

For every admissible run and every integer $r_0\ge r$: if no agent of $A_{\zeta,p}$ exits $G_\zeta$ before $\zeta$ exits $G$, then

$$t_\zeta\ \le\ r_0+L_{o_\zeta d_\zeta}+\bigl|B_{\zeta,p}(r_0)\bigr|,$$

where $t_\zeta$ is the exit time of $\zeta$.

Milestones (§3.2, p. 9)

When $\zeta$ is still inside $G$ at $r_0$, the proof follows tokens: imaginary markers that $\zeta$ produces from time $r_0$ on, and that travel with the agents leaving buffers ((s1), (s2), p. 8). The milestones are the paper's statements about them, with $L=L_{o_\zeta d_\zeta}$:

1. (p1) each agent holds at most one token, and a buffer never contains more tokens than agents;
2. (p2) the agent leaving $\zeta$'s buffer always holds exactly one token;
3. (p3) after $r_0$, $\zeta$ produces a new token only while he waits;
4. Claim 1 the induction step of Lemma 1 at the vertices where token $k$ departs right after a smaller token;
5. Lemma 1 token $k$ departs every vertex $v$ of its trail inside $G_\zeta$ by time $r_0+(L-L_{vd_\zeta}+k-1)$;
6. token exit token $k$ exits $G_\zeta$ by time $r_0+(L+k-1)$.

Significance

The result. The bound does not depend on the rule that selects the leaving agent, so it covers every queueing discipline at once: FIFO, global agent priorities, and the edge-priority rules of earlier dynamic routing games. With $r_0=r$ and no later entrants on $G_\zeta$, it gives Corollary 1: the residence time of $\zeta$ is at most $L_{o_\zeta d_\zeta}+|B_{\zeta,p}(r)|$. Example 1 (p. 8) shows that the bound can be attained. The freedom in $r_0$ is what §6 uses to show that queue lengths stay bounded at equilibria of dynamic routing games on series-parallel networks.

Formalizing it. The theorem is proved on paper. No machine-checked version is known to exist, and the platform has no rule-free model of atomic dynamic routing. The mission adds that model: a run is a set of leave times constrained by (A1)–(A2), not a fixed simulation. It also adds the multi-token process and the paper's chain of statements leading to Theorem 1.

Difficulty

The obvious argument is wrong. One might reason that $\zeta$ travels at most $L_{o_\zeta d_\zeta}$ edges and each earlier agent delays him at most once, giving the bound at once. The paper notes (p. 7) that this intuition fails even with two agents: a single agent can delay $\zeta$ more than $|\Delta|$ times, because delays propagate through other buffers. Bounding the total therefore means tracking chains of delays across the network rather than charging each delay to one agent.

Formally, the hard parts are:

• the run is only constrained, not determined;
• the token process is defined by recursion over time, using the unique leaver of each buffer;
• (p1)–(p3) are invariants proved by induction on time;
• Lemma 1 combines induction on the token index with longest-path inequalities in an acyclic graph.

Formalization scope

• Model. Network V E (tail and head maps) with finite V, E and a hypothesis Acyclic: no nonempty closed walk. Paths are edge lists. longest v w is the supremum of path lengths in $\mathbb N$; it is a maximum wherever it is used.

• Runs. RunData holds entry times, routes, origins and destinations, and leave times leave i j in $\mathbb N\cup\{\infty\}$ for the $j$-th edge of $i$'s route, numbered from $0$. IsADR states that:

  • routes are nonempty origin–destination paths;
  • finitely many agents enter per time;
  • nobody leaves a buffer before entering it;
  • (A2) holds, as unique existence of the leaver of each nonempty buffer at each time.

  Agents form an arbitrary type and may be infinitely many. An agent may never be served (leave time $\infty$), as in the paper, so the theorem also asserts that $\zeta$ exits.

• Derived objects. Exit times, $G_\zeta$, $A_{\zeta,p}$, $B_{\zeta,p}(r_0)$ and the exit time from $G_\zeta$ are definitions computed from the run, never free parameters. $|B_{\zeta,p}(r_0)|$ is Set.ncard of a set that is finite under IsADR.

• Tokens. The token milestones assume that $\zeta$ is inside $G$ at $r_0$, as §3.1 requires when starting the construction. Tokens are indexed from $1$. A new token gets index one plus the number produced so far. Bounds with subtraction are written additively over $\mathbb N$, e.g. $s+L_{vd_\zeta}+1\le r_0+L+k$, which is the same inequality over the integers.

• Ruled out. None of these is used, since each proves a different statement: a fixed tie-breaking rule (FIFO or priorities), exit times as free parameters, finitely many agents, or dropping acyclicity, which Remark 2 shows is necessary.

Contributions welcome: proofs of the token invariants, of Lemma 1, and of the goal. The network and run definitions can be reused for the paper's other results (Theorem 2 on uniform capacities, the routing games of §5–6).

Selected references

• Z. Cao, B. Chen, X. Chen, C. Wang, Bounding residence times for atomic dynamic routings, Mathematics of Operations Research, 2022 (accepted manuscript: WRAP 160244). https://doi.org/10.1287/moor.2021.1242 , https://wrap.warwick.ac.uk/160244
• Y. Mansour, B. Patt-Shamir, Greedy packet scheduling on shortest paths, Journal of Algorithms 14(3):449–465, 1993.
• I. Cidon, S. Kutten, Y. Mansour, D. Peleg, Greedy packet scheduling, SIAM Journal on Computing 24(1):148–157, 1995.
• T. Harks, B. Peis, D. Schmand, B. Tauer, L. Vargas Koch, Competitive packet routing with priority lists, ACM Transactions on Economics and Computation 6(1):4:1–4:26, 2018.

Motivation

Traffic, packet and evacuation networks are often studied with atomic dynamic flows: individual agents move through a network over time, queue at congested links, and each wants to reach its destination as early as possible. The deterministic queuing (Vickrey) model makes the queue at every link explicit: a link has a capacity, and agents beyond it wait in a queue. In the atomic, discrete-time version, simultaneous arrivals at a queue must be ordered by some tie-breaking rule, and that rule decides whether the resulting routing game has an equilibrium.

Hoefer, Mirrokni, Röglin and Teng (2009, 2011) and Werth, Holzhauser and Krumke (2014) studied atomic routing over time in deterministic queuing models, and found non-existence of equilibria and computational hardness in several variants; Harks, Peis, Schmand, Tauer and Vargas Koch (2018) studied competitive packet routing with priority lists. Scarsini, Schröder and Tomala (Operations Research, 2018) proved that a Nash equilibrium exists when priorities are placed on agents, in single-origin, single-destination networks. Cao, Chen, Chen and Wang (Operations Research 2021) showed that with agent priorities and several origins an equilibrium can fail to exist (their Example 3, a rock–paper–scissors cycle). They proposed instead to break ties by edge priorities at each vertex, and proved that equilibria then always exist. This mission formalizes that existence theorem.

Setting

A network instance consists of the following data.

• A finite acyclic directed multigraph $G=(V,E)$ with a destination $d$; every vertex has a path to $d$. Every edge has unit capacity and unit length.
• At each vertex $v$, a complete priority order $\prec_v$ on the edges entering $v$.
• At time $0$, an initial ranked queue $Q^0_e$ on each edge $e$.
• At each time $r\ge1$ and vertex $v$, a finite ranked set $\Delta_{r,v}$ of agents entering at origin $v$.

The agent set $\Delta$ is the disjoint union of all these, and may be infinite.

Each agent $i$ chooses at time $0$ a path $P_i$ from his starting vertex to $d$. For $i\in Q^0_e$ the path must begin with $e$; this is his strategy set $\mathcal P_i$. At every time unit only the head of the queue on an edge leaves it, and it reaches the head of the edge one unit later. Agents entering an edge are ranked by the edge-priority DQ rule, applied in this order:

• (R0) initial-queue order;
• (R1) an earlier entry ranks higher;
• (R2) among simultaneous entries through different edges, higher priority under $\prec_{u_e}$ ranks higher;
• (R3) an agent starting at $u_e$ ranks above through-traffic entering at the same time;
• (R4) agents with the same origin keep their original ranks.

$t^v_i(p)$ denotes the time agent $i$ reaches vertex $v$ under the profile $p$, and is $\infty$ if he never does.

The normal-form game $\Gamma^N$ has players $\Delta$, strategies $\mathcal P_i$, and cost $t^d_i$. A profile $p$ is a Nash equilibrium (NE) if $t^d_i(p)\le t^d_i(P'_i,p_{-i})$ for all $i$ and $P'_i\in\mathcal P_i$. It is an iteratively dominant NE (IDNE) if the agents can be reindexed $1,2,\dots$ such that for every $k$, every vertex $v$ on $P_k$ and every profile $q$ of the agents outside $[k]=\{1,\dots,k\}$,

$$t^v_k(p_{[k]},q)=\min\{t^v_j(p_{[k-1]},r): j\notin[k-1],\ r \text{ a profile of }\Delta\setminus[k-1]\}.$$

Formalization targets

Goal: Theorem 1 (p. 12)

$$\text{every } \Gamma^N \text{ admits a path profile } p \text{ that is an IDNE, and hence an NE.}$$

The goal makes no finiteness assumption on $\Delta$ and fixes no constants.

Milestones

1. Selection step (§4.1, p. 14). Given the first $k-1$ agents of the construction, the pruning (S1)–(S3) leaves exactly one candidate pair $(j,P_j)$.
2. Lemma EC.2 (p. ec6). For the selected $(k,P_k)$, any $S\subseteq\Delta\setminus[k-1]$, $j\in S$, $v\in P_k$ and any profile $q$,

$$t^v_k(p_{[k]},q_{S\setminus\{k\}})=\ell^v_k[\![k-1]\!]\le t^v_j(p_{[k-1]},q_S).$$

3. Reindexing (p. ec3). The selection can be iterated so that every agent receives an index.
4. Theorem EC.2 (p. ec8). The profile so constructed (a special IDNE) is an IDNE.
5. IDNE ⇒ NE (§4.1, p. 11).

Significance

The result. Theorem 1 gives an equilibrium for every network with edge priorities: multiple origins, initial queues and an unbounded stream of inflows are all allowed. With agent priorities, equilibrium can fail to exist in exactly this setting. The IDNE carries more structure than an NE. Arrival times along each agent's path are independent of later agents' choices, and no agent who enters later at the same origin overtakes an earlier one. The paper uses these properties in its study of subgame-perfect equilibria for adaptive agents (p. 12; §5).

Formalizing it. The result is proved in the paper; nothing here is open mathematically. To our knowledge no part of it is formalized in any proof assistant. The mission produces:

• a reusable, executable model of discrete-time deterministic queuing with priority tie-breaking;
• a formal proof of the constructive existence argument.

The paper proves Lemma EC.2 in a transformed game $\bar\Gamma^N$ on an infinite graph (Lemma EC.1). The mission instead states everything directly in $\Gamma^N$, so a complete development must either carry out the transfer or reprove the lemma natively. For infinitely many agents, the claim that every agent is eventually indexed (milestone 3) is asserted in the paper without a separate argument; the formal proof has to supply one.

Difficulty

The obvious argument fails at the no speed-up property. Adding agents to a network can make some other agent arrive earlier. The paper's Example 4 (pp. 15–16) has such a chain effect: removing an agent delays another. So the claim that agent $k$'s arrival times are unaffected by everyone after him is not monotonicity of congestion. It holds only for the specific order and paths produced by the selection procedure, and it must be proved by an induction that carries invariance (equality in (EC.2)) and domination (inequality in (EC.2)) together.

The tie-breaking is the second difficulty. The selection compares candidates backwards from $d$: by arrival time, then by incoming-edge priority, then one edge further back. The argument has to show that this order matches the queue rule (R0)–(R4) at every vertex, including (R3) for agents starting mid-network.

Formalization scope

Everything lives in the namespace AtomicDynFlow.IDNE.

• Network and agents. Instance V E A carries the graph as finite types V, E with tail, head, d, and the priorities as lists inc v of incoming edges, highest priority first. Initial queues Q0 e are listed head first, and inflows inflow r v highest original rank first. The standing hypotheses are fields:

  • acyclicity, as a height function;
  • reachability of $d$;
  • no inflow at time $0$;
  • every agent lies in exactly one source list.

  The agent type A is arbitrary and may be infinite.

• Dynamics. queue π s e is a computable, list-based simulation of the queue on each edge at each time, under a partial profile π : A → Option (List E), where none means the agent is absent. arrival π i v : ℕ∞ is $t^v_i$, with ⊤ for $\infty$ (p. ec4). The starting-vertex time is $0$ for initial-queue agents and $r$ for $\Delta_{r,v}$ (Algorithm 1, Step 2).

• Equilibria. The reindexing of Definition 2 is an injective $\sigma:\Delta\to\mathbb N$ whose range is an initial segment, with agent $a$ receiving index $\sigma(a)+1$. Definition 2 quantifies over every vertex of the path, the starting vertex included.

• Selection. The pruning (S1)–(S3) is a backward pairwise comparison of candidate pairs (Before, IsSelected). Milestones 2 and 4 are $\Gamma^N$-native versions of the e-companion statements, and Lemma EC.1 is not formalized.

Ruled out. Three encodings would trivialize the goal, and none is used:

• arrival times that ignore queuing, under which every profile would be an IDNE;
• a profile in which removed agents are frozen rather than absent;
• a reindexing that skips agents.

A sorry-free check of the paper's Example 2 shows that agent $i$ waits at $y_1$ and reaches $d$ at time $6$, and that removing agent $g$ lets him arrive at $5$.

Welcome contributions: proofs of the milestones in any order. Milestone 5 needs only the definitions. Milestones 1 and 2 are the technical core, and general lemmas about the queue simulation (FIFO within an edge, monotonicity in entry times) are reusable throughout.

Selected references

• Z. Cao, B. Chen, X. Chen, C. Wang, Atomic dynamic flow games: adaptive versus nonadaptive agents, Operations Research, 2021; accepted manuscript Oct. 2020, WRAP 143835. https://doi.org/10.1287/opre.2021.2105
• M. Scarsini, M. Schröder, T. Tomala, Dynamic atomic congestion games with seasonal flows, Operations Research 66(2):327–339, 2018.
• T. Werth, M. Holzhauser, S. Krumke, Atomic routing in a deterministic queuing model, Operations Research Perspectives 1(1):18–41, 2014.
• T. Harks, B. Peis, D. Schmand, B. Tauer, L. Vargas Koch, Competitive packet routing with priority lists, ACM Transactions on Economics and Computation 6(1):4, 2018.
• M. Hoefer, V. S. Mirrokni, H. Röglin, S.-H. Teng, Competitive routing over time, Theoretical Computer Science 412(39):5420–5432, 2011.
• W. Vickrey, Congestion theory and transport investment, American Economic Review 59(2):251–260, 1969.

Motivation

Community detection asks for a hidden partition of the nodes of a graph from its edges. Its simplest probabilistic benchmark is the two-community stochastic block model (SBM), in which the minimum bisection problem is the maximum a posteriori estimator. That problem is NP-hard, so convex relaxations are used in its place, and the question is when a relaxation still returns the hidden partition exactly. For semidefinite relaxations this question has sharp answers (Abbe, Bandeira, Hall 2016; Bandeira 2018). Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2) ask the same question for the most common linear programming relaxation of minimum bisection, the metric relaxation. They show that it recovers the planted bisection in very dense graphs when $p-q>1/2$ (their Theorem 6). This mission is their converse in the very dense and dense regimes, Theorem 7: above explicit thresholds the LP fails with high probability.

Setting

The node set is $V=\{1,\dots,n\}$, $n$ even. A bisection is a partition $V=V_1\sqcup V_2$ with $|V_1|=|V_2|=n/2$. The cut vector $\bar x\in\{0,1\}^{\binom n2}$ of $V_1,V_2$ has $\bar x_{ij}=1$ exactly when $i$ and $j$ lie on different sides. For a graph $G$ with adjacency indicators $a_{ij}$, the metric relaxation is

$$\text{(LP-P)}\qquad \min_x \sum_{i<j}a_{ij}x_{ij}\quad\text{s.t.}\quad x_{ij}\le x_{ik}+x_{jk},\quad x_{ij}+x_{ik}+x_{jk}\le2,\quad \sum_{i<j}x_{ij}=\frac{n^2}{4},$$

over $x\in\mathbb R^{\binom n2}$, with the first family over distinct $i,j,k$ with $i<j$ and the second over $i<j<k$. The LP recovers the planted bisection if $\bar x$ is its unique optimal solution.

In the SBM $\mathcal G_{n,p,q}$ a bisection $V_1,V_2$ is first drawn uniformly at random; then each pair on the same side is an edge with probability $p$ and each pair across with probability $q$, independently, with $p>q$. The Erdős–Rényi graph $\mathcal G_{n,p}$ has every pair an edge with probability $p$. The dense scaling (20) is $p=\alpha n^{-\omega}$, $q=\beta n^{-\omega}$ with $\alpha>\beta>0$, $0\le\omega<1$; $\omega=0$ is the very dense regime. An event holds with high probability (w.h.p.) if its probability tends to $1$ as $n\to\infty$.

For a graph $G$, $\rho_G(i,j)$ is the shortest-path distance ($+\infty$ across components), $\rho_{\max}(G)=\max_{i,j}\rho_G(i,j)$ is the diameter, and $\rho_{\mathrm{avg}}(G)=\frac2{n^2}\sum_{i<j}\rho_G(i,j)$ is the average distance. $E$ is the edge set of $G$, $E_0$ the set of edges across the planted bisection.

Formalization targets

Goal: Theorem 7 (pp. 15–16)

Let $p=\alpha n^{-\omega}$, $q=\beta n^{-\omega}$ with $\alpha>\beta>0$, $\omega\in[0,1)$, and $\alpha,\beta<1$ if $\omega=0$. If one of

1. $\omega=0$ and $\beta>\max\big\{\tfrac{3-\alpha-\sqrt{(3-\alpha)^2-4\alpha}}2,\ 2\alpha-1\big\}$ (22),
2. $\omega\in(0,1)$, $\tfrac1{1-\omega}\notin\mathbb N$ and $\beta>\alpha/(2\lceil\tfrac1{1-\omega}\rceil-1)$ (23),
3. $\omega=\tfrac12$ and $\beta>\max\big\{\tfrac{1-2e^{-\alpha^2}}{2-e^{-\alpha^2}},\tfrac1{3+2e^{-\alpha^2}}\big\}\alpha$ (24),
4. $\omega\in(0,1)$, $\tfrac1{1-\omega}\in\mathbb N\setminus\{2\}$ and $\beta>\alpha/\big(\tfrac2{1-\omega}-1+2e^{-\alpha^{1/(1-\omega)}}\big)$ (25)

holds, then

$$\lim_{n\to\infty}\mathbb P_{(V_1,G)\sim\mathcal G_{n,p,q}}\big[\text{(LP-P) does not recover }V_1,V_2\big]=1.$$

Milestones

1. (26), p. 16: for $p,q=\Omega(\log n/n)$ with $\lim q/p\in(0,1]$, the ratio $|E_0|/|E|$ lies in $(1\pm\epsilon)\,q/(p+q)$ w.h.p.
2. Proposition 11, p. 28: a coupling of $\mathcal G_{n,q}$, $\mathcal G_{n,q,p}$ and $\mathcal G_{n,p}$ in which the three graphs are nested.
3. Proposition 12, p. 28: w.h.p. $\rho_{\max}(\mathcal G_{n,\alpha n^{-\omega}})=1+\lfloor\frac1{1-\omega}\rfloor$.
4. Proposition 14, p. 29 (Shimizu): w.h.p. $\rho_{\mathrm{avg}}(\mathcal G_{n,\alpha n^{-\omega}})\in((1-\epsilon)\mu,(1+\epsilon)\mu)$, where $\mu=\lceil\frac1{1-\omega}\rceil+\mathbf 1\{\frac1{1-\omega}\in\mathbb N\}e^{-\alpha^{1/(1-\omega)}}$.
5. Propositions 16, 17, 18, pp. 29–30: the diameter of the very dense and dense SBM, and lower bounds on its average distance, in the three cases $\omega=0$, $\frac1{1-\omega}\notin\mathbb N$ and $\frac1{1-\omega}\in\mathbb N$.

Significance

Theorem 6 and Theorem 7 together bracket the success region of the metric relaxation in the very dense regime: recovery for $p-q>1/2$, failure above the curve (22). In the dense regime, Theorem 7 gives explicit linear thresholds $\beta>c(\omega,\alpha)\,\alpha$ above which the LP fails. The proof reduces failure to a deterministic distance criterion (Theorem 5, posed in mission 4 of this series) and turns asymptotic distance distributions of random graphs into statements about an LP.

The results are proved in the paper, partly by citing Bollobás's diameter theorems and Shimizu's average-distance theorem; none of them has a machine-checked proof. Formalizing the mission yields, besides Theorem 7, the diameter and average distance of dense Erdős–Rényi graphs (Propositions 12 and 14) and the monotone coupling between Erdős–Rényi graphs and the SBM (Proposition 11), each of which is usable beyond this paper. The coupling and (26) are also the inputs of the logarithmic-degree result (Theorem 8, mission 7).

Difficulty

The deterministic half is short: once $|E_0|/|E|$, $\rho_{\max}$ and $\rho_{\mathrm{avg}}$ are pinned down, the case computations (28)–(29) reduce to inequalities between explicit expressions in $\alpha$, $\beta$ and $\omega$. The difficulty is the random-graph input. The diameter of $\mathcal G_{n,p}$ for $p=\alpha n^{-\omega}$ needs the second-moment analysis of the number of pairs at distance greater than $d$ (Bollobás, Corollaries 10.11–10.12), and the average distance needs the finer limit law for path counts at the critical exponent $\frac1{1-\omega}\in\mathbb N$, where the constant $e^{-\alpha^{1/(1-\omega)}}$ appears. A first-moment argument gives only one side of each estimate. Concentration of $|E|$ and $|E_0|$ (26) is a Hoeffding bound, but it must hold uniformly over the random planted bisection.

Formalization scope

Nodes are Fin n and graphs SimpleGraph (Fin n). A bisection is its side $V_1$ with $2|V_1|=n$. The LP variable is a symmetric, zero-diagonal array Fin n → Fin n → ℝ, with no box constraints, so uniqueness is uniqueness over $\mathbb R^{\binom n2}$. Probabilities are finite sums over all graphs (and all bisections for the SBM). Edge probabilities are clamped into $[0,1]$, which affects only finitely many $n$. SBM limits run over even $n=2m$. Distances are in ℕ∞ and $\rho_{\mathrm{avg}}$ in $[0,\infty]$, so disconnected samples have infinite diameter and average distance; no real truncation is used.

Disclosed choices:

• Theorem 7 adds $\alpha>\beta$, the SBM's standing assumption $p>q$ (§4, p. 13), also assumed by Proposition 18 and (26).
• (26) is posed for $p=\alpha s(n)$, $q=\beta s(n)$ with $s(n)\ge c\log n/n$ and $\alpha s(n)\le1$ eventually. Then $q/p=\beta/\alpha$, which avoids the printed "$\lim p/q\in(0,1]$", a slip for $q/p$.
• Proposition 11 is posed as printed, with middle law $\mathcal G_{n,q,p}$ (within $q$, across $p$).

Two encodings would make the statements trivial, and both are excluded. Unnormalized LP variables would make uniqueness false. Reading $\rho$ in $\mathbb R$ via toReal would make the upper bounds hold for disconnected graphs.

The deterministic distance criterion (Theorem 5) is posed in mission 4 and is not restated. Contributions are welcome on the coupling, Hoeffding-type concentration of edge counts, and the Erdős–Rényi distance asymptotics. These are reusable for any finite random-graph development.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2. https://arxiv.org/abs/2006.03213
• E. Abbe, A. S. Bandeira, G. Hall, Exact recovery in the stochastic block model, IEEE Trans. Inf. Theory 62 (2016) 471–487. https://arxiv.org/abs/1405.3267
• A. S. Bandeira, Random Laplacian matrices and convex relaxations, Found. Comput. Math. 18 (2018) 345–379. https://arxiv.org/abs/1504.03987
• B. Bollobás, Random Graphs, 2nd ed., Cambridge Studies in Advanced Mathematics 73, Cambridge University Press, 2001. https://doi.org/10.1017/CBO9780511814068
• N. Shimizu, The average distance of dense homogeneous random graphs, Mathematical Engineering Technical Report, Department of Mathematical Informatics, The University of Tokyo, November 2017 (Theorem 1; reference [38] of the paper). https://www.keisu.t.u-tokyo.ac.jp/research/techrep/

Motivation

The stochastic block model (SBM) is the standard benchmark for community detection: a random graph whose vertices are split into hidden communities, with denser connections inside a community than across. For two equal communities, the best possible estimator of the hidden partition is the minimum bisection problem, which is NP-hard in the worst case. Its tractable relaxations are therefore compared by asking for which edge densities they still recover the hidden partition exactly.

For semidefinite programming the answer is complete in the logarithmic-degree regime: Abbe, Bandeira and Hall (arXiv:1405.3267) located the information-theoretic threshold $\sqrt\alpha-\sqrt\beta=\sqrt2$, and the SDP relaxation was shown to reach it by Hajek, Wu and Xu (arXiv:1412.6156) and by Bandeira (arXiv:1504.03987). Linear programming relaxations are cheaper and widely used in combinatorial optimization, but their behaviour on the SBM was not known. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research, 2023) study the most common one, the metric relaxation. This mission formalizes their result for the logarithmic-degree regime (Theorem 8): there the LP relaxation fails to recover the hidden partition with high probability, at every choice of the parameters.

Setting

Let $V=\{1,\dots,n\}$ with $n$ even. A bisection is a partition $V=V_1\sqcup V_2$ with $|V_1|=|V_2|=n/2$; its cost in a graph $G$ is the number of edges between $V_1$ and $V_2$. Given a fixed planted bisection $V_1,V_2$, an optimization problem recovers it if its unique optimal solution corresponds to $V_1,V_2$.

The cut vector $\bar x\in\{0,1\}^{\binom n2}$ of $V_1,V_2$ has $\bar x_{ij}=1$ exactly when $i,j$ lie on different sides. With $a_{ij}=1$ for edges and $0$ otherwise, the metric relaxation is

$$\text{(LP-P)}\quad \min_x \sum_{i<j}a_{ij}x_{ij}\ \ \text{s.t.}\ \ x_{ij}\le x_{ik}+x_{jk},\ \ x_{ij}+x_{ik}+x_{jk}\le2,\ \ \sum_{i<j}x_{ij}=\frac{n^2}{4},$$

the first family over distinct $i,j,k$ and the second over $i<j<k$, with $x_{ji}:=x_{ij}$. Every bisection's cut vector is feasible.

The distance $\rho_G(i,j)$ is the length of a shortest $i$–$j$ path ($+\infty$ across components). The diameter is $\rho_{\max}(G)=\max_{i,j}\rho_G(i,j)$ and the average distance is $\rho_{\mathrm{avg}}(G)=\frac{2}{n^2}\sum_{i<j}\rho_G(i,j)$.

The Erdős–Rényi model $\mathcal G_{n,p}$ draws each edge independently with probability $p$. The SBM $\mathcal G_{n,p,q}$ chooses a bisection $V_1,V_2$ uniformly at random, then draws each pair inside a side with probability $p$ and each pair across with probability $q$, independently, where $p>q$. The logarithmic-degree regime (21) is

$$p=\alpha\frac{\log n}{n},\qquad q=\beta\frac{\log n}{n},\qquad \alpha>\beta>0 .$$

An event $A_n$ holds with high probability if $\mathbb P[A_n]\to1$ as $n\to\infty$.

Formalization targets

Goal: Theorem 8 (p. 18)

$$\alpha>\beta>0\ \Longrightarrow\ \lim_{n\to\infty}\mathbb P_{\mathcal G_{n,p,q}}\big[\text{(LP-P) does not recover }V_1,V_2\big]=1 .$$

Milestones

1. The threshold of [2] (p. 14, strict cases): if $\sqrt\alpha-\sqrt\beta>\sqrt2$, the minimum bisection problem recovers $V_1,V_2$ with high probability; if $\sqrt\alpha-\sqrt\beta<\sqrt2$, it does not.
2. Proposition 13 (p. 29): for $\alpha>1$ and $G\sim\mathcal G_{n,\alpha\log n/n}$, $\rho_{\max}(G)\in\big((1-\epsilon)\frac{\log n}{\log\log n},(1+\epsilon)\frac{\log n}{\log\log n}\big)$ with high probability.
3. Proposition 15 (p. 29, Theorem 1 of Chung–Lu): for $\alpha>1$, $\rho_{\mathrm{avg}}(G)\in\big((1-\epsilon)\frac{\log n}{\log pn},(1+\epsilon)\frac{\log n}{\log pn}\big)$ with high probability.
4. Proposition 19 (p. 30): for $\alpha>\beta>0$ with $\frac{\alpha+\beta}{2}>1$ and $G\sim\mathcal G_{n,p,q}$,

$$(1-\epsilon)\frac{\log n}{\log\log n}\le\rho_{\mathrm{avg}}(G)\le\rho_{\max}(G)\le(1+\epsilon)\frac{\log n}{\log\log n}$$

with high probability.

Two results the proof of Theorem 8 uses are posed in sibling missions of this series and are not restated here: Theorem 5 (a distance-based non-recovery criterion for (LP-P), mission 4) and the coupling Proposition 11 together with the crossing-edge count (26) (mission 6).

Significance

The result. Theorem 8 separates linear from semidefinite programming on a natural statistical problem. In the logarithmic regime the SDP relaxation recovers the planted bisection whenever any method can, while the metric LP fails with high probability for all $\alpha>\beta>0$, including parameters far above the information-theoretic threshold. The paper's Theorem 6 shows that in the very dense regime (constant $p,q$) the LP does succeed when $p-q>1/2$; Theorem 8 shows that at logarithmic degree no such window exists.

Formalizing it. The theorem is proved in the paper, modulo results cited from the random-graph literature. Nothing in this mission is machine-checked yet. Formalization adds a precise account of what the cited distance asymptotics assert; Proposition 19's upper bound is justified in the paper only by reference to "a standard result on the diameter of the SBM" obtained by adapting an argument of Abbe's survey, so a complete proof of it is new work. Propositions 13 and 15 are classical facts about Erdős–Rényi graphs that have no formal proof in any library known to the curators, and are reusable well beyond community detection.

Difficulty

The LP side of the argument is deterministic and finite. The difficulty is probabilistic. The distance results require tight control of breadth-first neighbourhood growth in sparse random graphs near the connectivity threshold, where the average degree is only logarithmic, with error terms small enough to pin the diameter to a $(1\pm\epsilon)$ window. A first-moment estimate of path counts gives only one side of each bound. In the SBM the two edge probabilities make neighbourhood growth inhomogeneous, so the Erdős–Rényi results do not transfer verbatim. The threshold of [2] is a separate sharp large-deviation statement, at the level of individual vertices' in- and out-degrees.

Formalization scope

Vertices are Fin n (0-based); graphs are SimpleGraph (Fin n). A bisection is recorded by its side $V_1$ with $2|V_1|=n$. The LP variable is a symmetric, zero-diagonal array $x:V\times V\to\mathbb R$, which is a point of $\mathbb R^{\binom n2}$; no box constraints are added. LP recovery means that the planted cut vector is the unique optimal solution; minimum-bisection recovery means that every bisection of cost at most the planted one is the planted unordered partition. Distances are in $\mathbb N\cup\{\infty\}$ and the average distance in $[0,\infty]$, so a disconnected sample has infinite diameter. The random-graph laws are finite sums over all graphs; the SBM averages over all bisections. Edge probabilities are clamped into $[0,1]$, which matters only for the finitely many $n$ with $\alpha\log n/n>1$. "With high probability" is a limit of probabilities equal to $1$; for the SBM the limit runs along $n=2m$. Logarithms are natural.

Disclosed choices relative to the printed statements: Theorem 8 prints only $\alpha,\beta>0$, and $\alpha>\beta$ is added as the SBM's standing assumption $p>q$ (p. 13) and that of (21). The threshold of [2] is printed as an "if and only if"; only the two strict implications are posed, and the boundary $\sqrt\alpha-\sqrt\beta=\sqrt2$ is left out.

The statements cannot be satisfied vacuously: the laws are genuine probability distributions for every $n$, the events compare extended-valued distances without truncation, and recovery requires uniqueness over all real feasible points of (LP-P). An encoding with an empty or degenerate feasible set, or with distances truncated to finite reals, would change the theorems and is excluded.

A complete development needs: Erdős–Rényi and SBM laws, breadth-first exploration bounds for sparse random graphs, the coupling of the SBM between two Erdős–Rényi graphs (mission 6), the LP non-recovery criterion (mission 4), and the information-theoretic threshold of [2]. Contributions on the random-graph distance asymptotics are reusable on their own and especially welcome.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023. https://arxiv.org/abs/2006.03213 (v2 is the cited version)
• E. Abbe, A. S. Bandeira, G. Hall, Exact recovery in the stochastic block model, IEEE Transactions on Information Theory 62:471–487, 2016. https://arxiv.org/abs/1405.3267
• E. Abbe, Community detection and stochastic block models: recent developments, Journal of Machine Learning Research 18:1–86, 2018. https://arxiv.org/abs/1703.10146
• F. Chung, L. Lu, The diameter of sparse random graphs, Advances in Applied Mathematics 26(4):257–279, 2001. https://doi.org/10.1006/aama.2001.0720
• F. Chung, L. Lu, The average distances in random graphs with given expected degrees, PNAS 99(25):15879–15882, 2002. https://doi.org/10.1073/pnas.252631999
• B. Hajek, Y. Wu, J. Xu, Achieving exact cluster recovery threshold via semidefinite programming, IEEE Transactions on Information Theory 62(5):2788–2797, 2016. https://arxiv.org/abs/1412.6156
• A. S. Bandeira, Random Laplacian matrices and convex relaxations, Foundations of Computational Mathematics 18(2):345–379, 2018. https://arxiv.org/abs/1504.03987

Motivation

The stochastic block model (SBM), introduced by Holland, Laskey and Leinhardt (1983), is the standard random model for networks with community structure, and the basic benchmark for community-detection algorithms (Abbe 2018). In its two-community form the nodes are split into two equal halves, edges inside a half appear with probability $p$, and edges across with probability $q<p$. The task of exact recovery is to identify the hidden halves from the graph alone.

The maximum a posteriori estimator for this model is the minimum bisection problem (find a balanced cut with the fewest crossing edges), which is NP-hard in general. Abbe, Bandeira and Hall (2016) determined when it recovers the planted bisection, and showed that a semidefinite relaxation is as good as the integer program. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research 2023) ask the same question for the cheapest standard relaxation: the metric linear programming relaxation, defined by triangle inequalities. This mission is their positive result in the very dense regime.

Setting

Let $V=\{1,\dots,n\}$ with $n$ even. A bisection is a partition $V=V_1\cup V_2$ with $|V_1|=|V_2|=n/2$. For a graph $G=(V,E)$ let $a_{ij}=1$ if $(i,j)\in E$ and $0$ otherwise. The metric relaxation (LP-P) is

$$\min_{x\in\mathbb R^{\binom n2}}\ \sum_{i<j}a_{ij}x_{ij}\quad\text{s.t.}\quad x_{ij}\le x_{ik}+x_{jk},\quad x_{ij}+x_{ik}+x_{jk}\le 2,\quad \sum_{i<j}x_{ij}=\frac{n^2}{4},$$

the first constraint for all distinct $i,j,k$ with $i<j$, the second for all $i<j<k$, and $x_{ji}:=x_{ij}$. The cut vector $\bar x$ of a bisection has $\bar x_{ij}=0$ for $i,j$ on the same side and $\bar x_{ij}=1$ otherwise. (LP-P) recovers the planted bisection when $\bar x$ is its unique optimal solution.

In the Erdős–Rényi model $\mathcal G_{n,p}$ every pair of nodes is an edge independently with probability $p$. In the SBM $\mathcal G_{n,p,q}$ a bisection $V_1,V_2$ is first chosen uniformly at random; then pairs inside $V_1$ or inside $V_2$ are edges with probability $p$, pairs between them with probability $q$, all independently. $\mathcal G_{n,0,q}$ is the random bipartite graph across a random bisection. An event occurs with high probability (w.h.p.) if its probability tends to $1$ as $n\to\infty$. The graph is very dense when $p$ and $q$ are constants.

For a finite graph $G=(V,E)$ and $b\in\mathbb Z_{\ge0}^V$, a $b$-factor (or $f$-factor) is a set $F\subseteq E$ with exactly $b_v$ edges of $F$ at each node $v$; $N(U,U')$ counts edges with one endpoint in $U$ and one in $U'$; $d_{\min}$, $d_{\max}$ are the minimum and maximum degrees; and the node connectivity $\kappa(G)$ is the minimum number of nodes whose deletion disconnects $G$ (the number of nodes, for a complete graph).

Formalization targets

Goal: Theorem 6 (p. 15)

For constants $0<q<p<1$,

$$p-q>\tfrac12\ \Longrightarrow\ \mathbb P_{G\sim\mathcal G_{n,p,q}}\big[\text{(LP-P) recovers the planted bisection}\big]\xrightarrow[n\to\infty]{}1 .$$

Milestones

1. Proposition 6 (p. 20): for $G\sim\mathcal G_{2m,0,q}$ there is $C>0$ with $d_{\max}\le qm+C\sqrt{m\log m}$ w.h.p.
2. Proposition 5 (p. 20; Schrijver, Cor. 21.4a): a bipartite graph has a $b$-factor iff $N(U,U)\ge b(U)-\frac12 b(V)$ for every $U\subseteq V$.
3. Proposition 3 (p. 14): there is $C_{\mathrm{reg},2}>0$ such that for every $q\in(0,1)$, w.h.p. $G\sim\mathcal G_{n,0,q}$ is a subgraph of a regular bipartite graph with the same bipartition, of degree $d_{\mathrm{reg}}=\frac{qn}2+C_{\mathrm{reg},2}\sqrt{\frac n2\log\frac n2}$ (rounded down).
4. Proposition 8 (p. 24): for $G\sim\mathcal G_{n,p}$ there is $C>0$ with $d_{\min}\ge pn-C\sqrt{n\log n}$ w.h.p.
5. Proposition 9 (p. 24; Bollobás–Thomason): for $G\sim\mathcal G_{n,p}$, $\kappa(G)=d_{\min}$ w.h.p.
6. Proposition 7 (p. 24; Tutte's $f$-factor theorem).
7. Proposition 4 (p. 14): there is $C_{\mathrm{reg},1}>0$ such that for every $p\in(0,1)$, w.h.p. $G\sim\mathcal G_{n,p}$ contains a spanning regular subgraph of degree $d_{\mathrm{reg}}=pn-C_{\mathrm{reg},1}\sqrt{n\log n}$ (rounded up to an even integer).

The deterministic recovery criterion that the goal also depends on, Theorem 4 of the paper (regular sandwiching with $d_{\mathrm{in}}-d_{\mathrm{out}}\ge n/4$), is the goal of mission 3 of this series and is not restated here.

Significance

The result. Theorem 6 is the only positive recovery guarantee for the metric LP in the random setting of the paper. Together with the failure results of Theorems 7 and 8 (missions 6 and 7), it locates the LP strictly between trivial and information-theoretically optimal: it recovers in a region of constant $p,q$, but not up to the threshold $p>q$ that the minimum bisection problem and its SDP relaxation reach. Propositions 3 and 4, that dense random graphs sit inside, and contain, regular graphs of nearly their average degree, are of independent interest in random graph theory, as the authors note.

Formalizing it. The result is proved in the paper; none of it is machine-checked. The mission also requires three classical theorems that are not in Mathlib: the $b$-factor criterion for bipartite graphs, Tutte's $f$-factor theorem (Mathlib has only the perfect-matching case $f\equiv 1$), and the Bollobás–Thomason theorem $\kappa=d_{\min}$ for random graphs, together with degree concentration for $\mathcal G_{n,p}$ and the bipartite SBM. Each is reusable well beyond this paper.

Difficulty

The obvious argument for recovery is to exhibit a dual certificate for (LP-P), which needs regularity of the communities and of the cross edges; a random graph is not regular. The paper bridges the gap by sandwiching the random graph between regular graphs of nearly equal degree, and that step is where the difficulty lies: the existence of a regular sub- or supergraph is a global combinatorial property, characterized by factor theorems with exponentially many conditions, each of which must hold simultaneously with high probability. Degree concentration alone, the first idea, controls only the singleton conditions. Tutte's $f$-factor theorem and the bipartite $b$-factor criterion are themselves substantial combinatorial theorems, and the connectivity statement of Bollobás and Thomason is a deep result on random graphs.

Formalization scope

Nodes are Fin n (0-based). A bisection is a Finset $V_1$ with $2|V_1|=n$. Points of $\mathbb R^{\binom n2}$ are symmetric arrays with zero diagonal; (LP-P) has no box constraints $0\le x\le1$ (they are implied by the constraints and adding them would change the LP). Recovery means: $\bar x$ is optimal and every optimal solution equals $\bar x$.

The random-graph laws are finite: a probability is a weighted sum over all graphs on Fin n, with independent edge weights, and for the SBM an average over all bisections; the event may depend on the drawn bisection. Edge probabilities are clamped into $[0,1]$, which is the identity on the parameters used here. "With high probability" is Tendsto … atTop (𝓝 1), along $n=2m$ for the SBM. The standing assumption $p>q$ is not built into the law, so that $\mathcal G_{n,0,q}$ is the case $p=0$.

Disclosed readings: the printed $d_{\mathrm{reg}}$ of Propositions 3 and 4 is not an integer; Proposition 3 is posed with degree $\lfloor d_{\mathrm{reg}}\rfloor$ and Proposition 4 with $2\lceil d_{\mathrm{reg}}/2\rceil$, the least even integer $\ge d_{\mathrm{reg}}$ (the proof assumes $d_{\mathrm{reg}}$ even). $\kappa(K_n)=n$ as on p. 24. Quantifier order follows each page: in Propositions 3 and 4 the constant precedes the probability parameter, in Propositions 6 and 8 it follows it; no constant depends on $n$.

A statement in which "with high probability" is replaced by a positive probability or an eventual bound, in which the bisection is fixed rather than random, or in which the regular degree is compared with an irrational real (an empty event) is not this mission's target.

Infrastructure needed: the finite random-graph laws, Hoeffding-type concentration over them, the two factor theorems, and node connectivity. Proofs of any milestone, and of the classical results as general graph theory, are welcome.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2. https://arxiv.org/abs/2006.03213
• E. Abbe, A. S. Bandeira, G. Hall, Exact Recovery in the Stochastic Block Model, IEEE Transactions on Information Theory 62(1), 2016. https://arxiv.org/abs/1405.3267
• E. Abbe, Community Detection and Stochastic Block Models: Recent Developments, Journal of Machine Learning Research 18, 2018. https://arxiv.org/abs/1703.10146
• P. W. Holland, K. B. Laskey, S. Leinhardt, Stochastic Blockmodels: First Steps, Social Networks 5(2), 1983. https://doi.org/10.1016/0378-8733(83)90021-7
• W. T. Tutte, The Factors of Graphs, Canadian Journal of Mathematics 4, 1952. https://doi.org/10.4153/CJM-1952-028-2
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003 (Corollary 21.4a).
• B. Bollobás, A. Thomason, Random Graphs of Small Order, in Random Graphs '83, North-Holland Mathematics Studies 118, 1985 (Theorem 1).
• A. Frieze, M. Karoński, Introduction to Random Graphs, Cambridge University Press, 2016 (Chapter 3). https://doi.org/10.1017/CBO9781316339831

Motivation

The minimum bisection problem asks, for a graph on an even number $n$ of vertices, for a split of the vertices into two halves that cuts as few edges as possible. It is NP-hard, and it is the maximum a posteriori estimator for the two-community stochastic block model (SBM), the standard benchmark for community detection (Abbe, 2018). Convex relaxations are the usual way to make such estimators tractable while keeping guarantees. For the semidefinite relaxation, exact-recovery thresholds are known (Abbe, Bandeira, Hall, 2016; Hajek, Wu, Xu, 2016). Linear programming relaxations are cheaper and much used in combinatorial optimization, but their recovery properties were not understood.

Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2, Mathematics of Operations Research, 2023) study the best-known LP relaxation of minimum bisection, the metric relaxation. They give a sufficient condition for it to recover a planted bisection (Theorem 4) and a necessary one (Theorem 5). This mission formalizes the necessary condition. Its consequence, developed in §4 of the paper, is that the metric relaxation fails with high probability in most SBM regimes, including those where the minimum bisection itself succeeds.

Setting

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,n\}$, and write $(i,j)$ for an edge with $i<j$; set $a_{ij}=1$ if $(i,j)\in E$ and $a_{ij}=0$ otherwise. A bisection is a partition of $V$ into two sets $V_1,V_2$ with $|V_1|=|V_2|=n/2$. One fixed bisection, unknown to the solver, is the planted bisection; $E_0$ is the set of edges with one end in $V_1$ and the other in $V_2$.

The cut vector $\bar x\in\{0,1\}^{\binom n2}$ of the planted bisection has $\bar x_{ij}=1$ exactly when $i$ and $j$ lie on different sides. The metric relaxation is the linear program, with $x_{ji}:=x_{ij}$,

$$\min_x\ \sum_{1\le i<j\le n}a_{ij}x_{ij}\quad\text{s.t.}\quad x_{ij}\le x_{ik}+x_{jk}\ (1),\qquad x_{ij}+x_{ik}+x_{jk}\le 2\ (2),\qquad \sum_{1\le i<j\le n}x_{ij}=\frac{n^2}{4}\ (3),$$

where (1) ranges over distinct $i,j,k$ with $i<j$ and (2) over $i<j<k$. The LP recovers the planted bisection if $\bar x$ is its unique optimal solution. The objective at $\bar x$ is $|E_0|$.

The graph distance $\rho_G(i,j)$ is the length of a shortest $i$–$j$ path ($+\infty$ across components). The diameter and the average distance are

$$\rho_{\max}(G)=\max_{i,j\in V}\rho_G(i,j),\qquad \rho_{\mathrm{avg}}(G)=\frac{2}{n^2}\sum_{1\le i<j\le n}\rho_G(i,j).$$

The average is over all $n^2$ ordered pairs, the diagonal included. For $n\ge5$ define

$$c(G)=\max\Big\{0,\ \frac{3\rho_{\max}(G)-4\rho_{\mathrm{avg}}(G)}{1-4/n}\Big\}.\qquad(17)$$

Formalization targets

Goal: Theorem 5

For a connected graph $G$ on $n\ge5$ nodes with a planted bisection,

$$\frac{1+c(G)}{2\rho_{\mathrm{avg}}(G)+2c(G)(1-\frac1n)}\,|E|<|E_0|\quad(18)\qquad\Longrightarrow\qquad\text{(LP-P) does not recover the planted bisection.}$$

Milestones

The proof of Theorem 5 works with the point $\tilde x\in\mathbb R^{\binom n2}$,

$$\tilde x_{ij}=\frac{\rho_G(i,j)+c(G)}{2\rho_{\mathrm{avg}}(G)+2c(G)(1-\frac1n)}.$$

The mission poses three statements about it, for a connected $G$ on $n\ge5$ nodes:

1. display (19), p. 12: for $i<j<k$, $\displaystyle\tilde x_{ij}+\tilde x_{ik}+\tilde x_{jk}\le\frac32\cdot\frac{\rho_{\max}(G)+c(G)}{\rho_{\mathrm{avg}}(G)+c(G)(1-\frac1n)}$;
2. p. 13: $\tilde x$ is feasible for (LP-P);
3. p. 13: the objective of (LP-P) at $\tilde x$ equals $\displaystyle\frac{1+c(G)}{\rho_{\mathrm{avg}}(G)+c(G)(1-\frac1n)}\cdot\frac{|E|}{2}$.

Significance

The result. Theorem 5 is a deterministic certificate of failure, stated for any connected graph, not for a random model. It reduces the question "does the LP recover?" to comparing two numbers that depend only on the distance profile of $G$ and on the fraction of edges cut by the planted bisection. When typical distances are close to the diameter, $c(G)$ is small and (18) asks only that $|E_0|/|E|$ exceed roughly $1/(2\rho_{\mathrm{avg}}(G))$. In random graphs typical distances are close to the diameter. The paper's Theorems 7 and 8 combine Theorem 5 with known distance asymptotics of Erdős–Rényi graphs (Bollobás, Random Graphs, 2001; Chung, Lu, 2001). They show that the metric relaxation fails with high probability in the dense and logarithmic-degree SBM, in contrast with the semidefinite relaxation. Those theorems are separate missions of this series and use Theorem 5 as a black box.

Formalizing it. The result is proved in the paper; no machine-checked version is known. The mission produces a formal metric relaxation of minimum bisection, with LP recovery defined as uniqueness of the optimum, and links it to graph distances through Mathlib's SimpleGraph.edist/ediam. The definitions are written to coincide with those of the other missions of this series, so that one model layer serves the sufficient condition (Theorem 4), the necessary condition (this mission), and the random-graph consequences.

Difficulty

Theorem 5 is not deep, but it is exact. The milestones fix the witness $\tilde x$; the work is in checking it. The obvious candidate, the graph metric $\rho_G$ itself rescaled to satisfy the equality (3), satisfies the triangle inequalities (1). It can violate the perimeter constraints (2) whenever some triangle of vertices is spread out compared with the average distance. The shift by $c(G)$, which depends on $\rho_{\max}$ and on the factor $1-4/n$, is tuned so that (2) holds with no slack in the worst case. A proof has to keep track of the normalization $2/n^2$ (ordered pairs, diagonal included), the factor $1-1/n$, and the sign of $3\rho_{\max}-4\rho_{\mathrm{avg}}$, and must use $n\ge5$ wherever it divides by $1-4/n$. In Lean the further work is converting between sums over ordered pairs, unordered pairs and the edge set, and between extended-valued distances and their real values for a connected graph.

Formalization scope

• Vertices and bisections. Vertices are Fin n (0-based). The planted bisection is a finset $V_1$ with $2|V_1|=n$, and $V_2=V_1^{c}$. $|E_0|$ is the number of pairs $i<j$ adjacent in $G$ and on different sides.
• LP variables. A point of $\mathbb R^{\binom n2}$ is an array $x:\texttt{Fin } n\to\texttt{Fin } n\to\mathbb R$. Feasibility includes symmetry and a zero diagonal, so the free diagonal and lower-triangle entries cannot break uniqueness of the optimum. No bounds $0\le x\le1$ are added; they are not constraints of (LP-P).
• Recovery. LPRecovers G V1 says that the cut vector of $V_1$ is optimal and every optimal point equals it.
• Distances. $\rho_G$ is SimpleGraph.edist (in $\mathbb N\cup\{\infty\}$), $\rho_{\max}$ is SimpleGraph.ediam, and $\rho_{\mathrm{avg}}$ is the printed formula computed in $[0,\infty]$. $c(G)$ and $\tilde x$ use their real values. All statements assume $G$ connected, where these values are finite and $\rho_{\mathrm{avg}}(G)>0$.
• Standing hypotheses. Every statement carries exactly the page's hypotheses: $G$ connected and $n\ge5$, plus, for Theorem 5, the planted bisection. The bisection forces $n$ even, so in effect $n\ge6$; $n\ge5$ is kept as printed. $\tilde x$ is indexed by $i<j$ on the page and is extended symmetrically with zero diagonal.
• Ruled out. A formalization that adds box constraints, drops the symmetric zero-diagonal normalization, averages over $n(n-1)/2$ pairs instead of the printed $2/n^2$, or omits connectivity (where the real value of an infinite distance would be $0$) states a different theorem. None of these is used here.

Contributions welcome: proofs of the three milestones and the goal. Reusable lemmas include the identity $\sum_{i<j}a_{ij}x_{ij}=\sum_{(i,j)\in E}x_{ij}$ for SimpleGraph.edgeFinset, the finiteness of ediam for connected graphs on Fin n, and the bound $\rho_{\mathrm{avg}}(G)\le(1-\frac1n)\rho_{\max}(G)$.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2 (2022). https://arxiv.org/abs/2006.03213
• E. Abbe, Community Detection and Stochastic Block Models: Recent Developments, Journal of Machine Learning Research 18 (2018). https://arxiv.org/abs/1703.10146
• E. Abbe, A. S. Bandeira, G. Hall, Exact Recovery in the Stochastic Block Model, IEEE Transactions on Information Theory 62 (2016). https://arxiv.org/abs/1405.3267
• B. Hajek, Y. Wu, J. Xu, Achieving Exact Cluster Recovery Threshold via Semidefinite Programming, IEEE Transactions on Information Theory 62 (2016). https://arxiv.org/abs/1412.6156
• B. Bollobás, Random Graphs, 2nd ed., Cambridge University Press, 2001. https://doi.org/10.1017/CBO9780511814068
• F. Chung, L. Lu, The Diameter of Sparse Random Graphs, Advances in Applied Mathematics 26 (2001). https://doi.org/10.1006/aama.2001.0720