diff --git a/papers/coloring_nested_tire_graphs/experiments/draw_universal_level_cycle_counterexample.py b/papers/coloring_nested_tire_graphs/experiments/draw_universal_level_cycle_counterexample.py new file mode 100644 index 0000000..ed63f0b --- /dev/null +++ b/papers/coloring_nested_tire_graphs/experiments/draw_universal_level_cycle_counterexample.py @@ -0,0 +1,132 @@ +"""Draw the 8-vertex counterexample to the universal-source form. + +The figure highlights the source vertex 7, the two BFS levels, and the +level cycle (3,4,5,8) that forces all four colours for that source. +""" + +from __future__ import annotations + +import os + +import matplotlib.pyplot as plt +import networkx as nx +from matplotlib.lines import Line2D + + +OUT_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) + + +def build_graph() -> nx.Graph: + g = nx.Graph() + g.add_edges_from( + [ + (1, 2), (1, 3), (1, 4), (1, 5), (1, 6), (1, 7), + (2, 3), (2, 6), (2, 7), + (3, 4), (3, 5), (3, 6), (3, 8), + (4, 5), + (5, 6), (5, 8), + (6, 7), (6, 8), + ] + ) + return g + + +def main() -> int: + g = build_graph() + levels = nx.single_source_shortest_path_length(g, 7) + is_planar, embedding = nx.check_planarity(g) + if not is_planar: + raise RuntimeError("counterexample graph should be planar") + pos = nx.planar_layout(g, scale=3.4) + + fig, ax = plt.subplots(figsize=(8.6, 7.2)) + + nx.draw_networkx_edges(g, pos, ax=ax, edge_color="#cbd5e1", width=1.4) + + cycle_edges = [(3, 4), (4, 5), (5, 8), (8, 3)] + nx.draw_networkx_edges( + g, + pos, + ax=ax, + edgelist=cycle_edges, + edge_color="#dc2626", + width=2.8, + ) + + level_colors = {0: "#0f172a", 1: "#475569", 2: "#94a3b8"} + for v, (x, y) in pos.items(): + lev = levels[v] + ax.scatter( + [x], + [y], + s=600 if v == 7 else 500, + color=level_colors[lev], + edgecolors="black", + linewidths=1.1, + zorder=3, + ) + ax.text( + x, + y, + f"{v}\n$\\ell={lev}$", + ha="center", + va="center", + color="white", + fontsize=10, + fontweight="bold", + zorder=4, + ) + + legend = [ + Line2D( + [0], + [0], + marker="o", + color="w", + label=r"source $S=\{7\}$", + markerfacecolor=level_colors[0], + markeredgecolor="black", + markersize=12, + ), + Line2D( + [0], + [0], + marker="o", + color="w", + label=r"level $L_1$", + markerfacecolor=level_colors[1], + markeredgecolor="black", + markersize=12, + ), + Line2D( + [0], + [0], + marker="o", + color="w", + label=r"level $L_2$", + markerfacecolor=level_colors[2], + markeredgecolor="black", + markersize=12, + ), + Line2D([0], [0], color="#dc2626", lw=2.8, label=r"problem cycle $(3,4,5,8)$"), + ] + + ax.legend(handles=legend, loc="lower center", ncol=2, framealpha=0.95) + ax.set_title( + "Counterexample to the universal-source form", + fontsize=14, + pad=18, + ) + ax.set_aspect("equal") + ax.axis("off") + fig.tight_layout(rect=[0, 0.05, 1, 1]) + + out = os.path.join(OUT_DIR, "fig_universal_level_cycle_counterexample.png") + fig.savefig(out, dpi=180, bbox_inches="tight") + plt.close(fig) + print(f"wrote {out}") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/papers/coloring_nested_tire_graphs/experiments/generate_candidate_families.py b/papers/coloring_nested_tire_graphs/experiments/generate_candidate_families.py new file mode 100644 index 0000000..726d7b4 --- /dev/null +++ b/papers/coloring_nested_tire_graphs/experiments/generate_candidate_families.py @@ -0,0 +1,189 @@ +"""Generate and test candidate graph families for the level-cycle conjecture. + +This script builds a few rigid maximal planar families and then runs the +existing level-cycle checker on them. It is meant as a small Sage-side +driver for probing likely counterexample sources before moving on to larger +families. + +Available families: + stacked-ring concentric triangular rings like the paper's G_1 + face-stack a chain of stacked triangulations built by repeatedly + stacking a vertex into a triangular face + +Examples: + sage -python experiments/generate_candidate_families.py stacked-ring 1 6 + sage -python experiments/generate_candidate_families.py face-stack 4 12 --full +""" + +from __future__ import annotations + +import argparse +import logging +from typing import Callable + +from sage.all import Graph # type: ignore[attr-defined] # pylint: disable=no-name-in-module + +from check_level_cycle_three_color import level_sources, test_graph + + +LOGGER = logging.getLogger(__name__) + + +def build_stacked_ring(levels: int) -> Graph: + """Return the concentric triangular-ring family used in the paper figure.""" + if levels < 1: + raise ValueError("stacked-ring requires at least one ring") + + g = Graph() + g.add_vertex(0) + next_vertex = 1 + + ring1 = [next_vertex + i for i in range(3)] + next_vertex += 3 + g.add_vertices(ring1) + g.add_edges([(0, v) for v in ring1]) + g.add_edges([(ring1[i], ring1[(i + 1) % 3]) for i in range(3)]) + + inner = ring1 + for _ in range(1, levels): + outer = [next_vertex + i for i in range(3)] + next_vertex += 3 + g.add_vertices(outer) + g.add_edges([(outer[i], outer[(i + 1) % 3]) for i in range(3)]) + g.add_edges([(inner[i], outer[i]) for i in range(3)]) + g.add_edges([(inner[i], outer[(i + 1) % 3]) for i in range(3)]) + inner = outer + + expected_edges = 3 * g.n_vertices() - 6 + if g.num_edges() != expected_edges: + raise AssertionError( + f"stacked-ring is not maximal planar: |V|={g.n_vertices()}, " + f"|E|={g.num_edges()}, expected {expected_edges}" + ) + return g + + +def build_face_stack(steps: int) -> Graph: + """Return a stacked triangulation built by repeatedly subdividing one face.""" + if steps < 1: + raise ValueError("face-stack requires at least one step") + + g = Graph() + g.add_vertices([0, 1, 2, 3]) + g.add_edges([(0, 1), (1, 2), (2, 0)]) + g.add_edges([(3, 0), (3, 1), (3, 2)]) + + active_face = (0, 1, 3) + next_vertex = 4 + for _ in range(steps - 1): + v = next_vertex + next_vertex += 1 + a, b, c = active_face + g.add_vertex(v) + g.add_edges([(v, a), (v, b), (v, c)]) + active_face = (a, c, v) + + expected_edges = 3 * g.n_vertices() - 6 + if g.num_edges() != expected_edges: + raise AssertionError( + f"face-stack is not maximal planar: |V|={g.n_vertices()}, " + f"|E|={g.num_edges()}, expected {expected_edges}" + ) + return g + + +FAMILY_BUILDERS: dict[str, Callable[[int], Graph]] = { + "stacked-ring": build_stacked_ring, + "face-stack": build_face_stack, +} + + +def parse_args() -> argparse.Namespace: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("family", choices=sorted(FAMILY_BUILDERS)) + parser.add_argument("n_min", type=int, nargs="?", default=1) + parser.add_argument("n_max", type=int, nargs="?", default=6) + parser.add_argument( + "--sources", + choices=("vertex", "cycle", "all"), + default="vertex", + help="candidate source family to search", + ) + parser.add_argument( + "--quantifier", + choices=("exists-source", "all-sources"), + default="exists-source", + help="whether to test the weakened or stronger conjecture", + ) + parser.add_argument( + "--max-cycle-source-size", + type=int, + default=None, + help="optional cap on induced cycle source size", + ) + parser.add_argument( + "--max-colorings", + type=int, + default=None, + help="optional cap per graph/source; capped searches report UNKNOWN", + ) + parser.add_argument( + "--full", + action="store_true", + help="continue after failures/unknowns instead of stopping at first", + ) + return parser.parse_args() + + +def main() -> int: + args = parse_args() + builder = FAMILY_BUILDERS[args.family] + stop_first = not args.full + + total_graphs = 0 + total_sources = 0 + unknown = 0 + + for n in range(args.n_min, args.n_max + 1): + g = builder(n) + total_graphs += 1 + print( + f"{args.family} n={n}: " + f"|V|={g.n_vertices()} |E|={g.num_edges()} " + f"sources={args.sources} quantifier={args.quantifier}" + ) + sources = list( + level_sources(g, args.sources, args.max_cycle_source_size) + ) + passed, complete, checked_sources = test_graph( + g, + sources, + args.max_colorings, + stop_first, + args.quantifier, + ) + total_sources += checked_sources + if not complete: + unknown += 1 + if not passed and not args.full: + print(f"ABORT: first failure at family={args.family} n={n}") + print( + f"SUMMARY: checked {total_graphs} graphs and {total_sources} " + f"sources; unknown_graphs={unknown}" + ) + return 1 + + print( + f"SUMMARY: checked {total_graphs} graphs and {total_sources} " + f"sources; unknown_graphs={unknown}" + ) + return 0 + + +if __name__ == "__main__": + logging.basicConfig(level=logging.INFO, format="%(levelname)s: %(message)s") + try: + raise SystemExit(main()) + except Exception as exc: # pragma: no cover - surfaced to the shell + LOGGER.exception("candidate family generation failed: %s", exc) + raise diff --git a/papers/coloring_nested_tire_graphs/fig_universal_level_cycle_counterexample.png b/papers/coloring_nested_tire_graphs/fig_universal_level_cycle_counterexample.png new file mode 100644 index 0000000..89ebd2d Binary files /dev/null and b/papers/coloring_nested_tire_graphs/fig_universal_level_cycle_counterexample.png differ diff --git a/papers/coloring_nested_tire_graphs/paper.pdf b/papers/coloring_nested_tire_graphs/paper.pdf index 05300e5..138b843 100644 Binary files a/papers/coloring_nested_tire_graphs/paper.pdf and b/papers/coloring_nested_tire_graphs/paper.pdf differ diff --git a/papers/coloring_nested_tire_graphs/paper.tex b/papers/coloring_nested_tire_graphs/paper.tex index 57d0036..3eed21f 100644 --- a/papers/coloring_nested_tire_graphs/paper.tex +++ b/papers/coloring_nested_tire_graphs/paper.tex @@ -1298,6 +1298,15 @@ level source. Then $G$ admits a proper $4$-vertex-colouring with the level-cycle three-colour restriction with respect to $S$. \end{conjecture} +\begin{figure}[htbp] +\centering +\includegraphics[width=0.78\textwidth]{fig_universal_level_cycle_counterexample.png} +\caption{The $8$-vertex counterexample to the universal-source form. +With source $S=\{7\}$, the level cycle $(3,4,5,8)$ lies in $L_2$ and +forces all four colours in every proper $4$-vertex-colouring.} +\label{fig:universal-level-cycle-counterexample} +\end{figure} + \begin{example}[Counterexample to Conjecture~\ref{conj:false-universal-level-cycle-three-colour}] \label{ex:universal-level-cycle-counterexample} Let $G$ be the maximal planar graph on vertex set