Dependencies

Every graph \(G\) satisfies \(\operatorname{pw}(G)\le \frac{7}{48}\, m+o(n)\).

Lean covers the \(\varepsilon \)–\(M\) form of Remark 9.14, which implies the statement, under H3 at the triple \(\mathsf{S}\); the Lean proof takes as hypotheses H3 of Appendix B.

Each row of Table 4 is a pathwidth sequence.

Computer-assisted: bootstrap_table.py.

A sequence \(a=(a_d)_{d\ge 3}\) of reals is a pathwidth sequence if there is a function \(\rho (n)=o(n)\) such that every graph \(G\) satisfies \(\operatorname{pw}(G)\le \sum _{d\ge 3}a_d\, n_d+\rho (n)\). A finite tuple \((a_3,\dots ,a_k)\) stands for the sequence that continues it with \(a_d=1\) for all \(d{\gt}k\).

Lean covers the equivalence of its \(\varepsilon \)–\(N\) form with its \(\rho (n)=o(n)\) form.

The algorithm makes at most \(n_{\ge 1}\) commits and at most \(2n_{\ge 1}\) rounds, and \(|D|+\psi ^-(R)\le \psi (G)\).

Lean covers for the Lean port of the implementation.

Let \(k\ge 3\) and let \(0\le b_3\le \dots \le b_k\) be reals with \(b_k+H_k\le 1\). Suppose that there is a function \(\rho (N)=o(N)\) such that every graph \(J\) with \(\delta (J)\ge 3\) and \(\Delta (J)\le k\) satisfies \(\operatorname{pw}(J)\le \sum _{d=3}^kb_d\, n_d(J)+\rho (|V(J)|)\). Then the bootstrap of \((b_3,\dots ,b_k)\) is a pathwidth sequence. It is nondecreasing, and all its entries are at most \(1\).

Lean covers its first claim, and the whole lemma when \((a_3,\dots ,a_k)\) is a pathwidth sequence.

Every component order is an ordering of \(Q\) that satisfies (8.3), and a component order can be computed in \(O(|Q|+|P|)\) time.

Lean covers for the Lean port of the implementation.

Let \(p\ge 3\) and \(R\ge 1\) be integers, let \(G\) be a graph with \(\Delta (G)\le p\), and let \((Y_v)\) be the padded labels of degree \(p\) (Definition 5.2(a)). Then every edge \(uv\) satisfies \(\operatorname{Corr}(Y_u,Y_v)\ge r_{pp}(1-\frac1R)\).

Lean covers the case \(p=3\).

For every \(c\in (0,1]\) the weights

satisfy every constraint of Table 9. Conversely, every solution of (12\(_c\)), (21) and (24) has \(w_r\ge \frac{2c}{1+4c}\). Hence the minimum of \(w_r\) subject to the constraints of Table 9 is exactly \(\frac{2c}{1+4c}\).

Computer-assisted: constants.py.

Let \((Y_0,Y_1,\dots ,Y_d)\) be a centered Gaussian vector with unit variances and \(\operatorname{Corr}(Y_0,Y_i)\ge r_i\) for \(1\le i\le d\).

(a)

If \(d=3\) and \((r_1,r_2,r_3)\) is a permutation of \((r_{33},r_{33},r_{34})\), then \(\Psi \le 0.1529003\).

(b)

If \(d=3\) and \((r_1,r_2,r_3)\) is a permutation of \((r_{33},r_{34},r_{34})\), then \(\Psi \le 0.165616\).

(c)

If \(d=4\), \(0\le j\le 4\), and \(j\) of the bounds \(r_i\) equal \(r_{34}\) and the other \(4-j\) equal \(r_{44}\), then \(\Psi \le 0.2627-j\, s\).

Computer-assisted: switch-lemma-degree3, switch-lemma-degree4.

Let \(F\), \(D\) and \(R\) be as in Lemma 4.5, where \(F\) has \(n\) vertices and \(m\) edges. Given \(F\), \(D\), \(V(R)\) and a path decomposition of \(R\) of width \(w\) with \(s\) bags, a path decomposition of \(F\) of width at most \(|D|+w+3\log _2n+1\) with at most \(s+n\) bags can be computed with \(O(m+s+n\log n)\) operations on integers of \(O(\log n)\) bits, where both decompositions are in interval form.

Lean covers for the Lean port of the implementation.

Each of the triples

is admissible for \(D=\{ 3,4,5\} \).

Computer-assisted: certify_star_bounds_arb_owen.py, check_star_bound_cells.py, star-bound-arb-owen, run_all.sh.

Let \((a_3,a_4)=(c_{3},0.2627)\). For every \(\tau \in [0,\frac{35}{32}]\) there is a transfer vector \(t\) with \(C_T(\tau )+\lambda _T(t)\le a_d\) for every \(\{ 3,4\} \)-type \(T=(d;k_3,k_4,0)\) other than \(T_0\).

Computer-assisted: certify_star_bounds_arb_owen.py, star-bound-arb-owen-S-switched-output.txt.

For \(\sigma =3\) and the previous weights, the set vector \(S_{4,r}\) with \(r_4=4\) is

and \(\tau (1.352437,5.215817)=1.27583{\gt}1.26089\). Also \(\tau {\gt}1.26089\) for the set vectors \(S_{4,r}\) with \((r_3,r_4)\) equal to \((3,1)\), \((2,2)\) or \((1,3)\).

Computer-assisted: nrd_dominating_set.py.

The algorithm \(\mathcal A_{3,\mathcal X_{14}}\) of Nederlof, van Rooij and van Dijk, with the decompositions of [FominGaspersSaurabhStepanov2009, Lemma 1], counts the dominating sets of each size of an \(n\)-vertex graph in time and space \(O(1.5004^n)\).

Computer-assisted: nrd_dominating_set.py.

The suprema \(F_3\) and \(F_4\) of Definition 6.7 satisfy

Computer-assisted: arb_F.py, arb_F_global.py, certify_F4.py.

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 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.

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 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.

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.

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.

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.

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.

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.

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.

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.