"""Search for counterexamples to the strengthened Conjecture 5.5:

   Let H be a cubic plane graph in which every face has length ≥ 5,
   with a proper 3-edge-colouring φ. If K_0 = {a,b}-Kempe cycle and
   K_1 = {a,c}-Kempe cycle share a colour-a edge, then h_φ cannot be
   constant on both V(K_0) and V(K_1).

The graphs H satisfying the face-length-≥-5 hypothesis are exactly
the duals of triangulations of the sphere with minimum degree ≥ 5.
We enumerate these via plantri (through Sage's
`graphs.triangulations(n, minimum_degree=5)`), take the planar dual,
and run the same Heawood-constancy check as
`search_smaller_counterexample.py`.

For each triangulation order n, the dual has 2n - 4 cubic vertices.
The smallest case n = 12 is the icosahedron, whose dual is the
dodecahedron (20 vertices, all faces pentagonal).

Run with:
  sage experiments/search_min_face5_counterexample.py        # default max_n=14
  sage experiments/search_min_face5_counterexample.py 16
  sage experiments/search_min_face5_counterexample.py 16 --all
"""
import sys
import time

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

# Reuse the verification machinery from the cubic-search script.
import os
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
from search_smaller_counterexample import (
    check_graph,
    min_face_length,
)


def planar_dual(G):
    """Build the planar dual of a planar graph G with its embedding
    already set via G.is_planar(set_embedding=True)."""
    faces = G.faces()
    D = Graph(multiedges=False, loops=False)
    n_faces = len(faces)
    D.add_vertices(range(n_faces))
    # Map each (undirected) edge of G to the indices of the two faces
    # that contain it.
    edge_to_faces = {}
    for i, face in enumerate(faces):
        for e in face:
            key = frozenset(e[:2])
            edge_to_faces.setdefault(key, []).append(i)
    for key, fs in edge_to_faces.items():
        if len(fs) == 2 and fs[0] != fs[1]:
            D.add_edge(fs[0], fs[1])
    return D


def main():
    args = [a for a in sys.argv[1:] if not a.startswith('--')]
    max_n = int(args[0]) if args else 14
    flag_all = '--all' in sys.argv[1:]

    print(f"Searching for counterexamples to the face-length-≥-5 form "
          f"of Conjecture 5.5.\n"
          f"Iterating over triangulations with min degree ≥ 5 for "
          f"n_T in [12, {max_n}].\n"
          f"Each dual is cubic with all faces of length ≥ 5; the dual "
          f"has 2n_T - 4 vertices.\n"
          f"{'Continuing past first hit.' if flag_all else 'Stopping at first hit.'}\n")

    first_found = None
    for n_T in range(12, max_n + 1):
        start = time.time()
        count = 0
        found = None
        try:
            gen = graphs.triangulations(n_T, minimum_degree=5)
        except Exception as ex:
            print(f"n_T={n_T:>3}: cannot enumerate ({ex})")
            continue
        for T in gen:
            T.is_planar(set_embedding=True)
            H = planar_dual(T)
            n_H = H.order()
            # Sanity: H should be cubic and planar; faces length ≥ 5.
            if max(H.degree()) != 3 or min(H.degree()) != 3:
                continue
            if not H.is_planar(set_embedding=True):
                continue
            if min_face_length(H) < 5:
                continue
            count += 1
            res = check_graph(H)
            if res is not None:
                found = (T.copy(), H.copy(), res, n_H)
                if not flag_all:
                    break
        elapsed = time.time() - start
        n_H_min = 2 * n_T - 4
        if found is None:
            print(f"n_T={n_T:>3}: checked {count} triangulation duals "
                  f"(each with {n_H_min} cubic vertices), no counterexample "
                  f"[{elapsed:.1f}s]")
        else:
            T, H, (col, K0, K1, h0, h1, a, b, c, e), n_H = found
            colour_name = {0: 'red', 1: 'blue', 2: 'green'}
            print(f"n_T={n_T:>3}: COUNTEREXAMPLE in dual #{count} "
                  f"(|V(H)| = {n_H}) [{elapsed:.1f}s]")
            print(f"  triangulation canonical graph6 = "
                  f"{T.canonical_label().graph6_string()}")
            print(f"  dual (cubic) canonical graph6 = "
                  f"{H.canonical_label().graph6_string()}")
            print(f"  dual edges    = {sorted(H.edges(labels=False))}")
            print(f"  colouring     = {col}")
            print(f"  shared colour = {colour_name[a]} ({a}), 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)})")
            if first_found is None:
                first_found = n_T
            if not flag_all:
                break
        sys.stdout.flush()

    if first_found is not None:
        print(f"\nSmallest counterexample at triangulation order n_T "
              f"= {first_found} (dual has {2 * first_found - 4} vertices).")
    else:
        print(f"\nNo counterexample found for triangulation orders ≤ "
              f"{max_n} (dual orders ≤ {2 * max_n - 4}).")


if __name__ == '__main__':
    main()