Let \(G\) be a graph with \(n\) vertices.

(a)

If \(\Delta (G)\le 3\), then \(\operatorname{pw}(G)\le c_{3}\, n+o(n)\), where \(c_{3}=\frac{3}{4\pi }\arccos \frac56\approx 0.13982\).

(b)

If \(\Delta (G)\le 4\), then \(\operatorname{pw}(G)\le F_4\, n+o(n)\), where \(F_4\approx 0.24577\) is the maximum over the threshold of an explicit Gaussian integral, the ideal \(4\)-star function (2.2).

Lean covers part (a) without hypotheses (as Theorem 8.1); part (b) under H1 (as Theorem 7.1(a)); the Lean proof takes as hypotheses H1 of Appendix B.

Every graph \(G\) satisfies \(\operatorname{pw}(G)\le \sum _{d\ge 3}a_d\, n_d+o(n)\) for the sequence

Lean covers the whole statement, under H3 at the triple \(\mathsf{S}\); the Lean proof takes as hypotheses H3 of Appendix B.

Every graph \(G\) with \(\Delta (G)\le 3\) satisfies \(\operatorname{pw}(G)\le \operatorname {cw}(G)\le c_*n+o(n)\).

Lean covers the whole statement, with Lemma 3.2 for every graph.

Every graph \(G\) with \(\Delta (G)\le 4\) satisfies \(\operatorname{pw}(G)\le a_3\, n_3+a_4\, n_4+o(n)\) for each of the pairs

(a)

\((a_3,a_4)=(F_4,\, F_4)\), and in particular \(\operatorname{pw}(G)\le F_4\, n+o(n)\);

(b)

\((a_3,a_4)=(F_3,\, 0.2575)\);

(c)

\((a_3,a_4)=\bigl(\tfrac {5}{32},\, \tfrac 14\bigr)\).

Lean covers part (a) under H1; parts (b) and (c) under H2 at the pair; the Lean proof takes as hypotheses H1, H2 of Appendix B.

Every graph \(G\) with \(\Delta (G)\le 5\) satisfies \(\operatorname{pw}(G)\le a_3\, n_3+a_4\, n_4+a_5\, n_5+o(n)\) for each of the triples

\(\mathsf{P}\)

\((a_3,a_4,a_5)=(F_3,\, 0.2575,\, 0.3667)\);

\(\mathsf{R}\)

\((a_3,a_4,a_5)=(0.1455,\, 0.2530,\, 0.3600)\);

\(\mathsf{S}\)

\((a_3,a_4,a_5)=\bigl(\tfrac {5}{32},\, \tfrac 14,\, \tfrac {11}{32}\bigr)\).

Lean covers the triples \(\mathsf{P}\), \(\mathsf{R}\) and \(\mathsf{S}\), under H3 at the triple; the Lean proof takes as hypotheses H3 of Appendix B.

Every graph \(G\) with \(\Delta (G)\le 3\) satisfies \(\operatorname{pw}(G)\le c_{3}\, n+o(n)\).

Lean covers the whole statement.

Every graph \(G\) with \(\Delta (G)\le 4\) satisfies \(\operatorname{pw}(G)\le c_{3}\, n_3+0.2627\, n_4+o(n)\).

Lean covers the whole statement, under H6 and H7; the Lean proof takes as hypotheses H6, H7 of Appendix B.

Each of the following six tuples is a pathwidth sequence:

Lean covers \(\mathsf{C}\) without hypotheses; \(\mathsf{F}\) under H1; \(\mathsf{P}\), \(\mathsf{R}\) and \(\mathsf{S}\) under H3 at the triple; \(\mathsf{M}\) under H6 and H7; the Lean proof takes as hypotheses H1, H3, H6, H7 of Appendix B.

In each case listed above there are a nondecreasing function \(\rho \colon \mathbb {N}\to [0,\infty )\) with \(\rho (n)=o(n)\) and two algorithms that, given \(G\in \mathcal C\), output a path decomposition of \(G\) in interval form, of width at most \(\beta (G)+\rho (n)\), and in the general case also at most \(\frac7{48}m+\rho (2m)\):

(a)

a Las Vegas algorithm, in expected \(n^{1+o(1)}\) bit operations;

(b)

a deterministic algorithm, in \(n^{2+o(1)}\) bit operations.

In the bootstrap and general cases, each algorithm uses in addition \(O(n(n+m))\) operations on integers of \(O(\log n)\) bits.

Lean covers for a Lean port of the implementation: every output is a path decomposition; no fallback on the inputs of these cases; the width bounds; and the bounds of Part I attained for some labeling (under the hypotheses of the attained theorem). Not the computation of the labels or the running times; the Lean proof takes as hypotheses H1, H2, H3 of Appendix B.

Let \(G\) be the constraint graph of an instance of Max \((r,2)\)-CSP, or of a semiring version, with \(n\) variables and \(m\) constraints. The instance can be solved in time and space

(1)

\(O^{*}\bigl(r^{\beta (R)+o(n)}\bigr)\) for the final graph \(R\) of some maximal sequence of reduction operations applied to \(G\), and hence \(O^{*}\bigl(r^{\beta (G)+o(n)}\bigr)\);

(2)

\(O^{*}\bigl(r^{(7/48)m+o(m)}\bigr)\);

(3)

\(O^{*}\bigl(r^{c_{3}n_3+o(n)}\bigr)\) if \(\Delta (G)\le 3\), and \(O^{*}\bigl(r^{\beta _4(G)+o(n)}\bigr)\) and \(O^{*}\bigl(r^{3F_4m/(2+16F_4)+o(m)}\bigr)\) if \(\Delta (G)\le 4\);

(4)

\(O^{*}\bigl(r^{n\, A(\bar d)+o(n)}\bigr)\), and hence

\[ O^{*}\Bigl(r^{(1-\frac{111}{28(\bar d+1)})n+o(n)}\Bigr)\ \text{if }\bar d\ge 7, \qquad O^{*}\Bigl(r^{(1-\frac{4}{\bar d+1})n+o(n)}\Bigr)\ \text{if }\bar d\ge 11. \]

Computer-assisted: constants.py.

Let \(G\) be a graph with \(n\) vertices.

(a)

If \(\Delta (G)\le 3\), then in time and space \(O^{*}(3^{c_{3}n_3+o(n)})=O(1.1661^n)\) one can count the dominating sets of \(G\) of each size, find a minimum weight dominating set and count the dominating sets of minimum weight.

(b)

A maximum weight independent set of \(G\) can be found, and the maximum weight independent sets counted, in time and space \(O^{*}(2^{c_{3}n_3+o(n)})=O(1.1018^n)\) if \(\Delta (G)\le 3\), and \(O^{*}(2^{\beta _4(G)+o(n)})=O(1.1858^n)\) if \(\Delta (G)\le 4\).

(c)

If \(\Delta (G)\le 3\), then, in time and space \(O^{*}(2^{c_{3}n_3+o(n)})=O(1.1018^n)\), one can find \(k\) vertices that cover the most edges (Max \(k\)-Vertex Cover); in time and space \(O^{*}(3^{c_{3}n_3+o(n)})=O(1.1661^n)\), a minimum independent dominating set; and in time and space \(O^{*}(6^{c_{3}n_3+o(n)})=O(1.2848^n)\), a minimal dominating set of maximum size (Upper Domination). If \(\Delta (G)\le 4\), a minimum independent dominating set can be found in time and space \(O^{*}(3^{\beta _4(G)+o(n)})=O(1.3100^n)\).

(d)

If \(\Delta (G)\le 3\), a minimum edge dominating set and a minimum maximal matching of \(G\) can be found in time and space \(O^{*}(3^{c_{3}n_3+o(n)})=O(1.1661^n)\).

(e)

A minimum odd cycle transversal of \(G\) can be found by a deterministic algorithm in time \(O^{*}(2^{m/6+o(n)})=O(1.2600^n)\) if \(\Delta (G)\le 4\) and in time \(O^{*}(2^{\gamma _5m+o(n)})=O(1.4262^n)\) if \(\Delta (G)\le 5\), where \(m=|E(G)|\) and \(\gamma _5{\lt}0.20484\) is the constant of Theorem 3.6.

Computer-assisted: constants.py, connectivity_bases.py.

The numbers of dominating sets of each size of an \(n\)-vertex graph can be computed deterministically in time and space \(O(1.4815^n)\). If the vertices carry real weights with \(n^{O(1)}\) distinct subset sums, the same holds for the numbers of dominating sets of each size and each weight.

Computer-assisted: nrd_dominating_set.py, nrd_weighted_check.py.

In every lazy configuration of the following classes, one of the three candidate vectors \((a,b)\) satisfies \(2^{-a}+2^{-b}\le 1\):

(1)

\(\Delta =4\), any minimizing section \(k\), an admissible type for section \(k\), and \(C^+=(N[x]\setminus \{ y,z\} )\cup E\) with \(|E|\le 2\);

(2)

\(\Delta \in \{ 5,6\} \), an admissible type, and \(C^+=N[x]\setminus \{ y,z\} \);

(3)

\(\Delta =5\), an admissible type, and \(C^+=(N[x]\setminus \{ y,z\} )\cup E\) with \(|E|\le 1\);

in classes (2) and (3) with both weight vectors (C.12) and (C.13), and in each class optionally with one further vertex \(p\in C^+\) with \(N(p)=\{ y,z\} \).

Computer-assisted: g2_enumeration.py.