Path Decompositions of Sparse Graphs via Gaussian Sweeps and Faster Exponential Algorithms
Serge Gaspers
cs.DS
Nov 3, 2026 · v1
cs.DM math.CO
TL;DR
Main pathwidth theorem for max-degree-3 graphs is fully formalized in Lean 4 with Mathlib; other bounds are formalized conditionally, and a Lean port of the algorithms is verified.
Abstract
Using the bisection bound of Monien and Preis, Fomin and Høie proved in 2006 that every graph of maximum degree 3 on $n$ vertices has pathwidth at most $n/6+o(n)$. We prove that the pathwidth, bisection width and cutwidth of these graphs are at most $c_3 n+o(n)$, where $c_3=\frac{3}{4π}\arccos\frac56\approx0.1398$. For bisection width this improves the bound $n/6+o(n)$ of Monien and Preis (2006) and extends to all such graphs the bound that Lichev and Mitsche (2023) obtained for random cubic graphs. For maximum degree 4, we prove that bisection width and cutwidth are at most $n/3+o(n)$, improving the bound $2n/5+o(n)$ of Monien and Preis for 4-regular graphs, and that pathwidth is at most $0.2458n$, improving the bound $n/3$ of Fomin, Gaspers, Saurabh and Stepanov (2009). We show that every graph with $m$ edges has pathwidth at most $7m/48+o(n)$, improving the bound $13m/75$ of Scott and Sorkin (2007), and we give further bounds of the form $\sum_{d\ge3}a_d n_d+o(n)$ with $a_d<1$, where $n_d$ is the number of vertices of degree $d$. The path decompositions, and linear orderings of the stated cutwidth, can be computed in polynomial time. Instead of deriving pathwidth bounds from bisection width, we give each vertex a Gaussian label, a weighted sum of independent standard normal variables over a ball around it, and sweep a threshold through the labels; the bags are frontiers, the vertices above the threshold with a neighbor below it. We bound the probability that a vertex lies in a frontier by comparison with an explicit Gaussian model of a vertex and its neighbors. Faster exact algorithms follow: for feedback vertex set and the traveling salesperson problem on graphs of bounded maximum or average degree, and on general graphs for minimum weight dominating set (by branching until the instance is sparse), Max 2-CSP and counting subgraphs with $k$ edges (by the bound in $m$).
Problem
Twenty-year-old upper bounds on the pathwidth, bisection width and cutwidth of sparse graphs (e.g. n/6 for maximum degree 3) limit the running times of exact exponential algorithms built on path decompositions.
Approach
Each vertex gets a Gaussian label, a weighted sum of independent standard normals over a ball around it. A threshold is swept through the labels, and the frontiers at each threshold are taken as bags. Frontier probabilities are bounded by comparison with explicit Gaussian star models, and concentration then yields a good realization of the labels. Theorem 8.1 is proved unconditionally in Lean 4 with Mathlib, and further results are formalized conditional on computer-certified inputs. A Lean port of the algorithms is proved to output decompositions meeting the bounds.
Results
Graphs of maximum degree 3 have pathwidth, bisection width and cutwidth at most 0.1398n+o(n). For maximum degree 4, pathwidth is at most 0.2458n, and graphs with m edges have pathwidth at most 7m/48+o(n). These bounds give faster exact algorithms for feedback vertex set, TSP, dominating set, Max 2-CSP and subgraph counting.
| Class | Δ≤3 | Δ≤4 | d=5 (per vertex) | per edge |
|---|
| previous | 1/6 | 1/3 | 13/30 | 13/75 |
| this paper | 0.1398 | 0.2458 | 11/32 | 7/48 |
Pathwidth bound coefficients: previous vs. this paper