math-research/papers/even_level_graph_generators/experiments/exhaustive_bridge.py

"""Exhaustive bridge-derived test for the 4 open Holton-McKay duals.

Step A (gauge): for each dual, count the valid parity partitions
(bipartitions L with both parity subgraphs bipartite) and measure a few
bridge-orbit sizes run to FULL exhaustion (no timeout).

Step B (decide): for each dual, for every valid parity partition L,
exhaust the backward bridge-orbit and look for an ELG with BFS-parity L.
YES if found for any L; NO (conclusive) if none found for all L.
"""
import sys
import os
sys.path.insert(0, '/Users/didericis/Code/math-research/papers/'
                'level_resolutions_of_maximal_planar_graphs/experiments')
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
import time
from load_holton_mckay import parse_planar_code
from tutte_dual_treecolor import dual_triangulation
from test_conjecture import is_even_level_graph
from bridge_derived_test import (
    sig, parity_subgraph, edge_is_bridge_in_parity,
    backward_bridge_neighbors,
)


def valid_parity_partitions(G):
    """Yield labels-dicts for every bipartition (fix node 0 in even class)
    such that both induced parity subgraphs are bipartite. Labels are 0
    (even) / 1 (odd)."""
    nodes = sorted(G.nodes())
    n = len(nodes)
    assert nodes[0] == 0
    for mask in range(2 ** (n - 1)):
        labels = {0: 0}
        for i in range(n - 1):
            labels[nodes[i + 1]] = (mask >> i) & 1
        even = [v for v in nodes if labels[v] == 0]
        odd = [v for v in nodes if labels[v] == 1]
        if not odd:
            continue
        if nx.is_bipartite(G.subgraph(even)) and nx.is_bipartite(G.subgraph(odd)):
            yield labels


def is_elg_with_parity(H, labels):
    """Is H an Even Level Graph for some source whose BFS-parity matches
    `labels` (up to global swap)? Only even-class vertices can be the
    source (level 0 is even)."""
    even = [v for v in H.nodes() if labels[v] == 0]
    odd_set = set(v for v in H.nodes() if labels[v] == 1)
    for s in even:
        # quick reject: all neighbours of s must be odd-class (level 1)
        if any(nb not in odd_set for nb in H.neighbors(s)):
            # could still match under global swap; handle swap separately
            pass
        ok, lvls = is_even_level_graph(H, frozenset({s}))
        if not ok:
            continue
        if all(lvls[u] % 2 == labels[u] for u in H.nodes()):
            return True
    # global swap: source in odd class, BFS-parity is complement of labels
    odd = [v for v in H.nodes() if labels[v] == 1]
    for s in odd:
        ok, lvls = is_even_level_graph(H, frozenset({s}))
        if not ok:
            continue
        if all(lvls[u] % 2 != labels[u] for u in H.nodes()):
            return True
    return False


def exhaust_bridge_orbit_for_elg(G, labels, cap=3_000_000):
    """Exhaust backward bridge-orbit (no ELG check during BFS), then scan
    for an ELG witness. Returns ('found',H) / ('exhausted',size) /
    ('capped',size)."""
    seen = {sig(G): G}
    frontier = [G]
    while frontier and len(seen) < cap:
        new = []
        for H in frontier:
            for Hp in backward_bridge_neighbors(H, labels):
                sg = sig(Hp)
                if sg not in seen:
                    seen[sg] = Hp
                    new.append(Hp)
        frontier = new
    status = 'capped' if frontier else 'exhausted'
    if status == 'exhausted':
        for H in seen.values():
            if is_elg_with_parity(H, labels):
                return 'found', H
    return status, len(seen)


def decide_dual(i, cap=3_000_000, log=print):
    graphs = parse_planar_code('experiments/nonham38m4.pc')
    G, _ = dual_triangulation(graphs[i][0])
    parts = list(valid_parity_partitions(G))
    log(f'dual {i}: {len(parts)} valid parity partitions')
    any_capped = False
    max_orbit = 0
    t0 = time.time()
    for j, labels in enumerate(parts):
        st, info = exhaust_bridge_orbit_for_elg(G, labels, cap=cap)
        if st == 'found':
            log(f'  partition {j}: FOUND ELG -> dual {i} IS bridge-derived '
                f'({time.time()-t0:.0f}s)')
            return 'bridge-derived'
        if st == 'capped':
            any_capped = True
            log(f'  partition {j}: orbit exceeded cap ({info}); inconclusive')
        else:
            max_orbit = max(max_orbit, info)
        if (j + 1) % 25 == 0:
            log(f'  ...{j+1}/{len(parts)} partitions, max orbit {max_orbit}, '
                f'{time.time()-t0:.0f}s')
    if any_capped:
        log(f'  dual {i}: no witness, but some orbits hit cap -> INCONCLUSIVE '
            f'({time.time()-t0:.0f}s)')
        return 'inconclusive'
    log(f'  dual {i}: NOT bridge-derived (all {len(parts)} orbits exhausted, '
        f'max orbit {max_orbit}, {time.time()-t0:.0f}s)')
    return 'not-bridge-derived'


def gauge(dual_indices):
    graphs = parse_planar_code('experiments/nonham38m4.pc')
    for i in dual_indices:
        G, _ = dual_triangulation(graphs[i][0])
        t0 = time.time()
        parts = list(valid_parity_partitions(G))
        print(f'dual {i}: {len(parts)} valid parity partitions '
              f'(enumerated in {time.time()-t0:.1f}s)')


if __name__ == '__main__':
    import sys as _s
    if len(_s.argv) > 1 and _s.argv[1] == 'gauge':
        gauge([0, 3, 4, 5])
    elif len(_s.argv) > 1:
        for idx in _s.argv[1:]:
            decide_dual(int(idx))