diff --git a/papers/face_monochromatic_pairs/experiments/check_v_neighbour_degrees.py b/papers/face_monochromatic_pairs/experiments/check_v_neighbour_degrees.py new file mode 100644 index 0000000..00cd975 --- /dev/null +++ b/papers/face_monochromatic_pairs/experiments/check_v_neighbour_degrees.py @@ -0,0 +1,147 @@ +"""For every reduction (G, v, i) underlying a chord-apex+Kempe +colouring (up to |V(G)| ≤ 20), check the degrees of v's five +neighbours in G. + +This determines whether the partial structural proof of the +deciding-face conjecture (Theorem~\\ref{thm:deciding-face-partial} in +the paper) covers ALL configurations empirically: + + - If every (G, v) we encounter has at least one neighbour of v with + deg_G(·) ≤ 6, the partial proof (which requires at least one + n_k ∈ {5, 6}, equivalently at least one u_{k+1} with deg_G ≤ 6) + handles every chord-apex+Kempe colouring up to |V(G)| ≤ 20. + + - If some (G, v) has all five neighbours of degree ≥ 7, we'd need + the unproved merged-side argument for those. + +Reports per n_G: number of (G, v) pairs with all-≥-7 neighbours. + +Run with: sage experiments/check_v_neighbour_degrees.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) + + +def cyclic_neighbour_degrees(G, v): + """Return the cyclic sequence of degrees of v's neighbours, in + their CW order around v in G's planar embedding.""" + G.is_planar(set_embedding=True) + emb = G.get_embedding() + return [G.degree(u) for u in emb[v]] + + +def main(max_n=20, time_budget_per_n=1200): + print("For every (G, v, i) underlying a chord-apex+Kempe colouring, " + "check the\ndegrees of v's neighbours in G.\n") + print("Each reduction index i ∈ {0,…,4} picks two consecutive " + "neighbours\n(u_{i+1}, u_{i+2}) of v whose degrees become the\n" + "two flank-face adjacent G'-face lengths n_i, n_{i+1}.\n") + print(f"n_G in [12, {max_n}]\n") + + grand_triples = 0 # total (G, v, i) triples + grand_bad_triples = 0 # both n_i, n_{i+1} ≥ 7 + grand_pairs = 0 # (G, v) pairs + grand_all_ge_7 = 0 # (G, v) pairs with all 5 neighbours deg ≥ 7 + grand_dist_min = {} # min neighbour deg over (G, v) + grand_dist_consec = {} # min over consecutive pair (n_i, n_{i+1}) for some i + grand_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 + triples_n = 0 + bad_triples_n = 0 + pairs_n = 0 + all_ge_7_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 + for v in G.vertex_iterator(): + if G.degree(v) != 5: + continue + cyc = cyclic_neighbour_degrees(G, v) + pairs_n += 1 + m_all = min(cyc) + grand_dist_min[m_all] = grand_dist_min.get(m_all, 0) + 1 + if m_all >= 7: + all_ge_7_n += 1 + worst_consec_min = max(min(cyc[i], cyc[(i+1) % 5]) + for i in range(5)) + grand_dist_consec[worst_consec_min] = ( + grand_dist_consec.get(worst_consec_min, 0) + 1) + for i in range(5): + triples_n += 1 + n_i = cyc[(i + 1) % 5] + n_ip1 = cyc[(i + 2) % 5] + if n_i >= 7 and n_ip1 >= 7: + bad_triples_n += 1 + if len(grand_examples) < 5: + grand_examples.append({ + 'n_G': n, 'tri_idx': tri_idx, 'v': v, 'i': i, + 'cyclic_degs': cyc, 'n_i': n_i, 'n_ip1': n_ip1, + 'graph6': G.canonical_label().graph6_string(), + }) + elapsed = time.time() - start + print(f"n={n}: {pairs_n} (G,v) pairs, {triples_n} (G,v,i) triples; " + f"{bad_triples_n} triples with both flank-adj deg ≥ 7 " + f"[{elapsed:.0f}s]") + sys.stdout.flush() + grand_pairs += pairs_n + grand_triples += triples_n + grand_bad_triples += bad_triples_n + grand_all_ge_7 += all_ge_7_n + + print() + print("=" * 70) + print(f"Grand totals across n_G in [12, {max_n}]:") + print(f" (G, v) pairs: {grand_pairs}") + print(f" (G, v, i) triples: {grand_triples}") + pct = 100 * grand_all_ge_7 / max(grand_pairs, 1) + print(f" pairs with all 5 neighbours deg ≥ 7: " + f"{grand_all_ge_7} ({pct:.2f}%)") + pct = 100 * grand_bad_triples / max(grand_triples, 1) + print(f" triples with BOTH flank-adj deg ≥ 7: " + f"{grand_bad_triples} ({pct:.2f}%)") + print() + print(" Distribution of min(all 5 neighbour degs) per (G, v):") + for m in sorted(grand_dist_min): + c = grand_dist_min[m] + ppct = 100 * c / max(grand_pairs, 1) + bar = '#' * max(1, int(ppct)) + print(f" {m}: {c:>6} ({ppct:5.2f}%) {bar[:50]}") + print() + print(" Distribution of MAX over i of " + "min(n_i, n_{i+1}) per (G, v)\n" + " (i.e., the worst-case consecutive-pair-min --- if this is\n" + " ≤ 6, every i has min(n_i, n_{i+1}) ≤ 6 and the partial proof\n" + " applies; if it is ≥ 7, at least one i has both flanks ≥ 7):") + for m in sorted(grand_dist_consec): + c = grand_dist_consec[m] + ppct = 100 * c / max(grand_pairs, 1) + bar = '#' * max(1, int(ppct)) + print(f" {m}: {c:>6} ({ppct:5.2f}%) {bar[:50]}") + if grand_examples: + print() + print(" Sample (G, v, i) triples where BOTH flank-adj deg ≥ 7:") + for ex in grand_examples: + print(f" n={ex['n_G']}, tri#{ex['tri_idx']}, v={ex['v']}, " + f"i={ex['i']}, " + f"cyclic degs around v = {ex['cyclic_degs']}, " + f"(n_i, n_{{i+1}}) = ({ex['n_i']}, {ex['n_ip1']})") + print(f" graph6: {ex['graph6']}") + + +if __name__ == '__main__': + main()