"""Search for the smallest cubic plane graph admitting a proper 3-edge-colouring
on which two intersecting Kempe cycles both have constant Heawood number.

The known counterexample (Figure
\\ref{fig:no-two-constant-kempe-counterexample} in paper.tex) has 40
vertices. This script searches small cubic planar graphs to see how
small a counterexample can be.

For each n in [4, max_n]:
  - enumerate all 3-connected cubic planar graphs on n vertices via
    sage's graphs.planar_graphs() with degree restrictions;
  - for each graph, set a planar embedding and enumerate all proper
    3-edge-colourings via backtracking;
  - for each colouring, compute h_φ at every vertex from the CW
    rotation;
  - try every colour-a edge as the candidate shared edge between
    K_{a,b} and K_{a,c}; trace both Kempe cycles and check whether
    h_φ is constant on V(K_{a,b}) and on V(K_{a,c}) simultaneously.

If a counterexample is found at some n < 40, print the edge list +
colouring + cycle data + Heawood values and stop searching that n
(but continue searching larger n if --all is passed).

Run with:
  sage experiments/search_smaller_counterexample.py        # default max_n=18
  sage experiments/search_smaller_counterexample.py 24     # specify max_n
  sage experiments/search_smaller_counterexample.py 24 --all   # find at every n
"""
import sys
import time

from sage.all import Graph
from sage.graphs.graph_generators import graphs


def edge_key(u, v):
    return (u, v) if u <= v else (v, u)


def all_proper_3_edge_colourings(edges, vertex_edges):
    """Yield every proper 3-edge-colouring of the given edge list as a
    tuple indexed by the edges list."""
    n = len(edges)
    colours = [None] * n
    # Symmetry break: first edge always gets colour 0.
    def backtrack(i):
        if i == n:
            yield tuple(colours)
            return
        u, v = edges[i]
        used = set()
        for j in vertex_edges[u]:
            if j != i and colours[j] is not None:
                used.add(colours[j])
        for j in vertex_edges[v]:
            if j != i and colours[j] is not None:
                used.add(colours[j])
        c_range = (0,) if i == 0 else range(3)
        for c in c_range:
            if c in used:
                continue
            colours[i] = c
            yield from backtrack(i + 1)
            colours[i] = None
    yield from backtrack(0)


def heawood_numbers(G, col_of_edge):
    """Return {v: ±1} from the CW rotation around each vertex of the
    planar embedding. col_of_edge: dict edge_key -> colour ∈ {0,1,2}."""
    emb = G.get_embedding()
    h = {}
    for v in G.vertex_iterator():
        cols = [col_of_edge[edge_key(v, u)] for u in emb[v]]
        # cyclic class
        i0 = cols.index(0)
        rot = cols[i0:] + cols[:i0]
        if rot == [0, 1, 2]:
            h[v] = +1
        elif rot == [0, 2, 1]:
            h[v] = -1
        else:
            return None
    return h


def trace_kempe(G, col_of_edge, start_edge, two_colours):
    """Trace the Kempe cycle in colours `two_colours` containing
    start_edge. Returns the vertex sequence (length = cycle length)."""
    target = set(two_colours)
    u0, v0 = start_edge
    walk = [u0, v0]
    bound = 4 * G.order() + 4
    while True:
        cur, prev = walk[-1], walk[-2]
        nxt = None
        for u in G.neighbors(cur):
            if u == prev:
                continue
            if col_of_edge[edge_key(cur, u)] in target:
                nxt = u
                break
        if nxt is None:
            return None
        if nxt == walk[0]:
            return walk
        walk.append(nxt)
        if len(walk) > bound:
            return None


def check_graph(G):
    """Return a counterexample (col, K0, K1, h_K0, h_K1, a, b, c) for G, or None."""
    if not G.is_planar(set_embedding=True):
        return None
    G.is_planar(set_embedding=True)  # ensure embedding is set
    edges = sorted([edge_key(u, v) for (u, v) in G.edge_iterator(labels=False)])
    edge_idx = {e: i for i, e in enumerate(edges)}
    vertex_edges = {
        v: [edge_idx[edge_key(v, u)] for u in G.neighbors(v)]
        for v in G.vertex_iterator()
    }

    for col in all_proper_3_edge_colourings(edges, vertex_edges):
        col_of_edge = {edges[i]: col[i] for i in range(len(edges))}
        h = heawood_numbers(G, col_of_edge)
        if h is None:
            continue
        # For each candidate shared colour a and shared edge:
        for a in range(3):
            other = [c for c in range(3) if c != a]
            b, c = other
            for e_i, e in enumerate(edges):
                if col[e_i] != a:
                    continue
                K0 = trace_kempe(G, col_of_edge, e, (a, b))
                K1 = trace_kempe(G, col_of_edge, e, (a, c))
                if K0 is None or K1 is None:
                    continue
                h0 = {h[v] for v in K0}
                h1 = {h[v] for v in K1}
                if len(h0) == 1 and len(h1) == 1:
                    return (col, K0, K1,
                            next(iter(h0)), next(iter(h1)),
                            a, b, c, e)
    return None


def min_face_length(G):
    """Min face length of G in its current planar embedding."""
    return min(len(f) for f in G.faces())


def main():
    args = [a for a in sys.argv[1:] if not a.startswith('--')]
    max_n = int(args[0]) if args else 18
    flag_all = '--all' in sys.argv[1:]
    # Parse --min-face N
    min_face = None
    for i, a in enumerate(sys.argv[1:]):
        if a == '--min-face' and i + 1 < len(sys.argv) - 1:
            min_face = int(sys.argv[i + 2])
            break
        if a.startswith('--min-face='):
            min_face = int(a.split('=', 1)[1])
            break

    print(f"Searching for cubic plane graph counterexamples to "
          f"Conjecture 5.5, n in [4, {max_n}] "
          f"({'continuing past first hit' if flag_all else 'stopping at first hit'})"
          + (f", min face length >= {min_face}" if min_face else "")
          + "\n")

    # If filtering by min face length, skip small n where impossible.
    # For all-faces-length->=L cubic plane: V - E + F = 2, E = 3V/2,
    # sum face lengths = 3V, F = V/2 + 2, so min sum = L*(V/2 + 2)
    # <= 3V gives V >= 2L*(L-3)/(3-L/2)... let's just set V >= 20 for L=5.
    if min_face is not None and min_face >= 5:
        n_start = max(4, 20)
    else:
        n_start = 4

    first_found = None
    for n in range(n_start, max_n + 1, 2):   # cubic requires n even
        start = time.time()
        count = 0
        skipped = 0
        found = None
        try:
            gen = graphs.planar_graphs(
                n,
                minimum_degree=3,
                minimum_connectivity=2,
            )
        except Exception as ex:
            print(f"n={n:>3}: cannot enumerate ({ex})")
            continue
        for G in gen:
            if max(G.degree()) != 3:
                continue   # not cubic
            if min_face is not None:
                G.is_planar(set_embedding=True)
                if min_face_length(G) < min_face:
                    skipped += 1
                    continue
            count += 1
            res = check_graph(G)
            if res is not None:
                found = (G.copy(), res)
                if not flag_all:
                    break
        elapsed = time.time() - start
        if found is None:
            extra = (f", skipped {skipped} due to small face"
                     if min_face is not None else "")
            print(f"n={n:>3}: checked {count} graphs, no counterexample"
                  f"{extra} [{elapsed:.1f}s]")
        else:
            G, (col, K0, K1, h0, h1, a, b, c, e) = found
            colour_name = {0: 'red', 1: 'blue', 2: 'green'}
            print(f"n={n:>3}: COUNTEREXAMPLE in graph #{count} [{elapsed:.1f}s]")
            print(f"  edges = {sorted(G.edges(labels=False))}")
            print(f"  colouring (sorted-edge order): {col}")
            print(f"  shared colour a = {colour_name[a]} ({a}), "
                  f"shared edge {e}")
            print(f"  K_{{a,b}} = K_{{{colour_name[a]},{colour_name[b]}}} "
                  f"= {K0}  (h = {h0:+d}, |V| = {len(K0)})")
            print(f"  K_{{a,c}} = K_{{{colour_name[a]},{colour_name[c]}}} "
                  f"= {K1}  (h = {h1:+d}, |V| = {len(K1)})")
            print(f"  canonical graph6 = "
                  f"{G.canonical_label().graph6_string()}")
            if first_found is None:
                first_found = (n, G, col, K0, K1, h0, h1, a, b, c, e)
            if not flag_all:
                break
        sys.stdout.flush()

    if first_found is not None:
        n, *_ = first_found
        print(f"\nSmallest counterexample found at n = {n}.")
    else:
        print(f"\nNo counterexample found for n ≤ {max_n}.")


if __name__ == '__main__':
    main()