Path Decompositions of Sparse Graphs via Gaussian Sweeps and Faster Exponential Algorithms
Companion site
The animation (4:32) follows the Gaussian sweep on a planar graph with 149 vertices: the cut sweep of Section 3, then the frontiers, ideal stars and median switch behind the bound \(c_3n+o(n)\) of Section 2. Watch it full screen.
The paper in brief
For graphs of maximum degree \(3\), the best upper bound on pathwidth had stood for twenty years: Fomin and Høie proved \(\frac n6+o(n)\) in 2006 through the bisection bound of Monien and Preis. The paper replaces bisection by a Gaussian sweep. Each vertex receives a Gaussian label, a weighted sum of independent standard normal variables over a ball around it, so that adjacent vertices have strongly correlated labels; sweeping a threshold through the labels gives a path decomposition whose bags are the frontiers of the threshold.
| Bound (without lower-order terms) | Previous | This paper | In the paper |
|---|---|---|---|
| pathwidth, maximum degree \(3\) | \(\frac16\approx0.1667\) | \(c_3=\frac{3}{4\pi}\arccos\frac56\approx0.1398\) | Theorem 1.1(a) |
| pathwidth, maximum degree \(4\) | \(\frac13\) | \(F_4\approx0.2458\) | Theorem 1.1(b) |
| bisection width, maximum degree \(3\) | \(\frac16\) | \(c_3\) | Corollary 1.2 |
| pathwidth per edge, all graphs | \(\frac{13}{75}\approx0.1733\) | \(\frac7{48}\approx0.1458\) | Corollary 1.4 |
Theorem 1.3 bounds the pathwidth of every graph by a sum of per-degree coefficients, and Section 9 gives several such pathwidth sequences, none best for all graphs. The decompositions can be computed in polynomial time (Theorem 10.1). Part II derives faster exact algorithms, listed in Table 2.
What is checked, and how
- Lean. The bound for maximum degree \(3\) (Theorem 8.1) is proved in Lean 4 without hypotheses; most other width bounds are proved in Lean under explicit hypotheses, which the paper proves (several by computer-assisted proofs) or which a separate formalisation proves. The formalisation page maps each statement to its Lean theorems.
- Computer-assisted proofs. The admissibility certificates, the constants \(F_3\) and \(F_4\), the switch-lemma certificates and the analyses of Part II are computed in ball arithmetic or exact rational arithmetic; the code and data are in
ancillary/.
Where to go next
- Read the paper: the full text, section by section, with the same numbering as the PDF. Statements with a Lean proof or code show it below the statement.
- Download the PDF of the same version.
- Download the short version (PDF, 28 pages): the main results with proof sketches, the complete proof of the bound \(c_3n+o(n)\) for maximum degree \(3\), and the algorithmic applications in one table.
- Formalisation and certificates: what is formalised, under which hypotheses, and how it was checked.
- Release: the exact version these files come from.