Metric Dimension is NP-complete on Graphs of Treewidth Two
Tristan Benoit
cs.CC
Oct 15, 2026 · v3
cs.DM
TL;DR
The main results (connectivity, treewidth at most two, exact metric dimension of the reduction graph) are formalized in Lean 4 with Mathlib, with no unproved statements.
Abstract
The metric dimension of a connected graph is the least number of vertices whose distance vectors distinguish all vertices. We show that deciding whether the metric dimension of a graph is at most a given integer is NP-complete on graphs of treewidth at most two, and even on two-connected two-terminal series-parallel graphs of pathwidth at most five. As the problem is polynomial on trees, the graphs of treewidth one, this settles the treewidth threshold of its hardness, which was known to lie between two and twenty-four. The reduction is from satisfiability of formulas in which every literal occurs at most twice. To such a formula with $n$ clauses and $r$ variables it associates a two-terminal series-parallel graph $G_\varphi$ with $O((n+r)^2)$ vertices and pathwidth at most five, whose metric dimension is $2(n+r)+7$ if the formula is satisfiable and $2(n+r)+8$ otherwise.
Problem
The complexity of Metric Dimension on graphs of bounded treewidth was open. Hardness was known only for treewidth at most twenty-four, while the problem is polynomial on trees.
Approach
A reduction from satisfiability of formulas in which every literal occurs at most twice. Each formula is mapped to a two-terminal series-parallel graph built from copies of path-like templates with crossings and ears. Distances are proved using distance certificates. The research and paper were produced with a large language model, which also independently produced a Lean 4/Mathlib formalisation of the main results.
Results
Metric Dimension is NP-complete on graphs of treewidth two, and even on two-connected series-parallel graphs of pathwidth at most five. This settles the treewidth threshold. The Lean formalisation proves the graph's connectivity, its treewidth bound, the metric dimension dichotomy, and the preservation of satisfiability under normalisation, using only the standard axioms.
