Add Kempe-locked colored edge flip class survey script

Iterates min-degree-5 maximal planar graphs and, for each one G, looks
for any flip-neighbor H and proper 4-coloring phi of H satisfying the
Kempe-locked structure of Lemma 4.3 (phi(u)=phi(v) plus an {a,b}-Kempe
chain for every other color b).  For each such (H, phi), BFS the
colored edge flip class with a 50,000-graph cap and test reached
graphs for isomorphism to G.  Saves the first G for which no such (H,
phi) has G in its colored class.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

colored_edge_flip_class_survey.py

@@ -0,0 +1,197 @@
+"""Survey for min-degree-5 maximal planar graphs G such that no Kempe-locked
+proper 4-coloring of any flip-neighbor of G admits a graph isomorphic to G in
+its colored edge flip class.
+
+For each min-degree-5 maximal planar graph G of order n:
+  for each admissible edge uv of G with flip H = G^flip(uv):
+    for each proper 4-coloring phi of H satisfying:
+      (a) phi(u) == phi(v), and
+      (b) for every color b != phi(u), u and v lie in the same connected
+          component of the subgraph of H induced by vertices of color
+          phi(u) or b ({phi(u), b}-Kempe chain),
+    BFS the colored edge flip class C(H, phi) and test each reached graph
+    for isomorphism to G.
+
+If for some (H, phi) a graph isomorphic to G is reached, G is "found" and we
+move on. Otherwise we save G and stop.
+"""
+from typing import Iterator, Any, cast
+from sage.all import Graph, graphs  # type: ignore[attr-defined]  # pylint: disable=no-name-in-module
+from sage.graphs.graph_coloring import all_graph_colorings  # type: ignore[attr-defined]  # pylint: disable=no-name-in-module
+from lib.colored_graphs import canonize_and_save_graph
+
+
+BFS_LIMIT = 50000
+
+
+def face_thirds(g: Graph) -> dict[frozenset, tuple]:
+    """Map each edge {u, v} of triangulation g to (w, x), the two third vertices
+    of the triangular faces incident to uv."""
+    g_emb = g.copy()
+    if not g_emb.is_planar(set_embedding=True):
+        raise ValueError("graph is not planar")
+    incidence: dict[frozenset, list] = {}
+    for face in g_emb.faces():
+        if len(face) != 3:
+            raise ValueError("graph is not a triangulation")
+        a, b, c = face[0][0], face[1][0], face[2][0]
+        for u, v, third in [(a, b, c), (b, c, a), (c, a, b)]:
+            incidence.setdefault(frozenset((u, v)), []).append(third)
+    return {k: tuple(v) for k, v in incidence.items() if len(v) == 2}
+
+
+def edge_set(g: Graph) -> frozenset:
+    """Hashable canonical representation of g's edges, ignoring labels."""
+    return frozenset(frozenset(e) for e in g.edges(labels=False))
+
+
+def kempe_connects(h: Graph, phi: dict[Any, int], a: int, b: int, u: Any, v: Any) -> bool:
+    """True iff u and v lie in the same component of the subgraph of h
+    induced by vertices of color a or b."""
+    if phi[u] not in (a, b) or phi[v] not in (a, b):
+        return False
+    verts = [w for w in h.vertices() if phi[w] in (a, b)]
+    sub = cast(Graph, h.subgraph(verts))
+    for comp in sub.connected_components():
+        if u in comp:
+            return v in comp
+    return False
+
+
+def coloring_passes_filter(h: Graph, phi: dict[Any, int], u: Any, v: Any) -> bool:
+    """phi(u) == phi(v), and for every color b != phi(u), there is a
+    {phi(u), b}-Kempe chain in h from u to v."""
+    a = phi[u]
+    if phi[v] != a:
+        return False
+    for b in range(4):
+        if b == a:
+            continue
+        if not kempe_connects(h, phi, a, b, u, v):
+            return False
+    return True
+
+
+def color_preserving_flips(g: Graph, phi: dict[Any, int]) -> Iterator[Graph]:
+    """Yield every g^flip(u'v') such that the flip is admissible and the new
+    edge's endpoints w', x' satisfy phi(w') != phi(x') (so phi remains proper)."""
+    pairs = face_thirds(g)
+    for u, v in list(g.edges(labels=False)):
+        thirds = pairs.get(frozenset((u, v)))
+        if thirds is None or len(thirds) != 2:
+            continue
+        w, x = thirds
+        if g.has_edge(w, x):
+            continue
+        if phi[w] == phi[x]:
+            continue
+        flipped = g.copy()
+        flipped.delete_edge(u, v)
+        flipped.add_edge(w, x)
+        yield flipped
+
+
+def canonical_g6(g: Graph) -> str:
+    """Canonical graph6 string used to test isomorphism."""
+    return cast(Graph, g.canonical_label()).graph6_string()
+
+
+def class_contains_iso_to(h: Graph, phi: dict[Any, int], target_canonical: str,
+                          limit: int = BFS_LIMIT) -> tuple[bool, int, bool]:
+    """BFS the colored edge flip class of (h, phi). Return (found, visited_count,
+    hit_limit), where found is True iff some reached graph has canonical
+    graph6_string equal to target_canonical."""
+    visited: set[frozenset] = {edge_set(h)}
+    if canonical_g6(h) == target_canonical:
+        return True, len(visited), False
+    frontier: list[Graph] = [h]
+    while frontier:
+        if len(visited) >= limit:
+            return False, len(visited), True
+        cur = frontier.pop()
+        for nxt in color_preserving_flips(cur, phi):
+            es = edge_set(nxt)
+            if es in visited:
+                continue
+            visited.add(es)
+            if canonical_g6(nxt) == target_canonical:
+                return True, len(visited), False
+            frontier.append(nxt)
+    return False, len(visited), False
+
+
+def survey_graph(g: Graph, verbose: bool = False) -> tuple[bool, bool]:
+    """Test whether g admits any Kempe-locked flip witness.
+
+    Returns (filter_nonempty, found_in_class). filter_nonempty is True iff at
+    least one (H, phi) satisfies the Kempe-locked criteria. found_in_class
+    is True iff some such (H, phi) has a graph isomorphic to g in its
+    colored edge flip class. (When filter_nonempty is False, found_in_class
+    is also False but the graph should be SKIPPED, not saved.)"""
+    target_canonical = canonical_g6(g)
+    pairs = face_thirds(g)
+    filter_nonempty = False
+    total_filtered_colorings = 0
+    for u, v in list(g.edges(labels=False)):
+        thirds = pairs.get(frozenset((u, v)))
+        if thirds is None or len(thirds) != 2:
+            continue
+        w, x = thirds
+        if g.has_edge(w, x):
+            continue
+        h = g.copy()
+        h.delete_edge(u, v)
+        h.add_edge(w, x)
+        for phi in all_graph_colorings(h, 4, vertex_color_dict=True):
+            phi = cast(dict, phi)
+            if not coloring_passes_filter(h, phi, u, v):
+                continue
+            filter_nonempty = True
+            total_filtered_colorings += 1
+            found, visited, hit_limit = class_contains_iso_to(h, phi, target_canonical)
+            if verbose:
+                msg = f"    edge ({u},{v}), phi#{total_filtered_colorings}: visited={visited}{' (LIMIT)' if hit_limit else ''}"
+                print(f"{msg} -> {'found' if found else 'not found'}")
+            if found:
+                return True, True
+    if verbose and not filter_nonempty:
+        print("    no Kempe-locked colorings — skipping")
+    return filter_nonempty, False
+
+
+def survey(min_order: int, max_order: int) -> Graph | None:
+    """Iterate min-degree-5 maximal planar graphs in [min_order, max_order].
+    Return the first G failing the Kempe-locked reachability test, or None."""
+    for n in range(min_order, max_order + 1):
+        print(f"=== order {n} ===")
+        gen = graphs.planar_graphs(
+            n, minimum_connectivity=3, maximum_face_size=3, minimum_degree=5
+        )
+        checked = 0
+        skipped_vacuous = 0
+        for g in gen:
+            checked += 1
+            filter_nonempty, found = survey_graph(g, verbose=True)
+            if not filter_nonempty:
+                skipped_vacuous += 1
+                continue
+            if not found:
+                print(f"order {n}, graph #{checked}: Kempe-locked coloring exists "
+                      f"but G NOT reachable; saving and stopping")
+                return g
+            if checked % 10 == 0:
+                print(f"  order {n}: checked {checked} graphs, skipped (vacuous) {skipped_vacuous}")
+        print(f"  order {n} done: {checked} graphs checked, {skipped_vacuous} skipped (vacuous)")
+    return None
+
+
+if __name__ == "__main__":
+    import sys
+    min_order = int(sys.argv[1]) if len(sys.argv) > 1 else 12
+    max_order = int(sys.argv[2]) if len(sys.argv) > 2 else 14
+    result = survey(min_order, max_order)
+    if result is None:
+        print("No witness graph found in the surveyed range.")
+    else:
+        _, graph_dir = canonize_and_save_graph(result)
+        print(f"Saved witness to {graph_dir}")