"""For every chord-apex+Kempe colouring of every reduced dual (up to
|V(G)| ≤ 18), check whether there exists a "deciding face": a face f
of the reduced dual whose boundary lies entirely in V(K_b) ∪ V(K_c)
and whose length is not divisible by 3.

If a deciding face exists, then under the (hypothetical) constancy
hypothesis h_φ ≡ ε on V(K_b) ∪ V(K_c), Heawood's face-sum identity
gives ε · |f| ≡ 0 (mod 3), which forces ε ≡ 0 since |f| ≢ 0 (mod 3) --
contradicting ε ∈ {±1}. So existence of a deciding face in every
chord-apex+Kempe colouring of every reduced dual would *prove*
Conjecture 5.1 via the contrapositive of Lemma 5.3.

This script reports, per (n_G, colouring): does a deciding face exist?
And if not, why not (insufficient coverage, all in-coverage faces have
length ≡ 0 mod 3, etc.).

Run with: sage experiments/check_deciding_face.py
"""
import os
import sys
import time

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

HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)

from check_conj_final_scaled import (
    apply_reduction,
    proper_3_edge_colorings,
    matches_chord_apex_kempe,
    kempe_cycle_set,
    edge_idx,
)
from check_heawood_on_kempe import (
    dual_of, vertices_of_kempe,
)


def find_deciding_face(H, V_union):
    """Return (face, |face| mod 3) of a deciding face (all boundary in
    V_union, length not divisible by 3). None if no such face exists."""
    for face in H.faces():
        verts = {u for (u, v) in face} | {v for (u, v) in face}
        if not verts.issubset(V_union):
            continue
        L = len(face)
        if L % 3 != 0:
            return face, L, L % 3
    return None


def test_one(D):
    D.is_planar(set_embedding=True)
    n_col = 0
    n_with_deciding = 0
    no_deciding_examples = []
    deciding_lengths = {}   # |f| of deciding face -> count
    for face in D.faces():
        if len(face) != 5: continue
        for i_red in range(5):
            res = apply_reduction(D, face, i_red, 9999)
            if res is None: continue
            H = res['H']; named = res['named']
            H.is_planar(set_embedding=True)
            edges, colorings = proper_3_edge_colorings(H)
            cand = [c for c in colorings
                    if matches_chord_apex_kempe(edges, c, named)]
            for col in cand:
                n_col += 1
                merged_idx = edge_idx(edges, named['merged'])
                a = col[merged_idx]
                bs = [c for c in range(3) if c != a]
                kc_b = kempe_cycle_set(edges, col, merged_idx, (a, bs[0]))
                kc_c = kempe_cycle_set(edges, col, merged_idx, (a, bs[1]))
                V_b = vertices_of_kempe(edges, kc_b)
                V_c = vertices_of_kempe(edges, kc_c)
                V_union = V_b | V_c
                deciding = find_deciding_face(H, V_union)
                if deciding is not None:
                    n_with_deciding += 1
                    _, L, mod_r = deciding
                    deciding_lengths[L] = deciding_lengths.get(L, 0) + 1
                else:
                    cov_ratio = len(V_union) / H.order()
                    in_cov_face_lens = sorted([
                        len(f) for f in H.faces()
                        if {u for (u, v) in f} | {v for (u, v) in f}
                           <= V_union])
                    if len(no_deciding_examples) < 3:
                        no_deciding_examples.append({
                            'cov_ratio': cov_ratio,
                            'in_cov_face_lens': in_cov_face_lens,
                            'V_union_size': len(V_union),
                            'V_total': H.order(),
                        })
    return n_col, n_with_deciding, deciding_lengths, no_deciding_examples


def main(max_n=20, time_budget_per_n=1800):
    print(f"Deciding-face existence on chord-apex+Kempe colourings, "
          f"n_G ∈ [12, {max_n}]\n")
    grand_col = 0
    grand_dec = 0
    grand_lens = {}
    grand_no_dec_examples = []
    for n in range(12, max_n + 1):
        start = time.time()
        try:
            triangulations = list(graphs.triangulations(n, minimum_degree=5))
        except Exception as ex:
            print(f"n={n}: cannot enumerate ({ex})")
            continue
        n_col_n = 0
        n_dec_n = 0
        for tri_idx, G in enumerate(triangulations):
            if time.time() - start > time_budget_per_n:
                print(f"  n={n}: timeout at tri {tri_idx}/{len(triangulations)}")
                break
            G.is_planar(set_embedding=True)
            D = dual_of(G)
            ni, ndec, lens, no_dec_ex = test_one(D)
            n_col_n += ni
            n_dec_n += ndec
            for k, v in lens.items():
                grand_lens[k] = grand_lens.get(k, 0) + v
            if len(grand_no_dec_examples) < 5:
                grand_no_dec_examples.extend(
                    no_dec_ex[:5 - len(grand_no_dec_examples)])
        elapsed = time.time() - start
        pct = 100 * n_dec_n / max(n_col_n, 1)
        print(f"n={n}: {n_col_n} col., {n_dec_n} with deciding face "
              f"({pct:.2f}%) [{elapsed:.0f}s]")
        sys.stdout.flush()
        grand_col += n_col_n
        grand_dec += n_dec_n

    print()
    print("=" * 70)
    print(f"Grand totals: {grand_col} chord-apex+Kempe colourings")
    pct = 100 * grand_dec / max(grand_col, 1)
    print(f"  with deciding face: {grand_dec} ({pct:.2f}%)")
    print(f"  without          : {grand_col - grand_dec} "
          f"({100 - pct:.2f}%)")
    if grand_lens:
        print()
        print("  Deciding face length distribution:")
        for L in sorted(grand_lens):
            print(f"    |f| = {L} (mod 3 = {L % 3}): {grand_lens[L]}")
    if grand_no_dec_examples:
        print()
        print("  Sample colourings WITHOUT a deciding face:")
        for ex in grand_no_dec_examples[:5]:
            print(f"    coverage = {ex['V_union_size']}/{ex['V_total']} "
                  f"({100*ex['cov_ratio']:.0f}%); in-coverage face "
                  f"lengths = {ex['in_cov_face_lens']}")


if __name__ == '__main__':
    main()