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

"""Test the disjunction: every maximal planar graph is a valid derived
level graph, an intertwining tree, or both. Iterates n=6..12, stops if
a counterexample is found."""
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 time
import itertools
import networkx as nx
from triangulation_gen import enumerate_all_triangulations
from test_conjecture import (
    canonical_sig, bfs_levels, get_level_sources,
    is_even_level_graph, bfs_orbit
)


def is_intertwining_tree(G):
    """Search for a 2-partition (A, B) such that G[A] and G[B] are trees."""
    nodes = list(G.nodes())
    n = len(nodes)
    # Try all 2^(n-1) partitions (fix node 0 in A by convention)
    for mask in range(1, 2 ** (n - 1)):
        A = [nodes[0]] + [nodes[i + 1] for i in range(n - 1) if (mask >> i) & 1]
        B = [nodes[i + 1] for i in range(n - 1) if not ((mask >> i) & 1)]
        if not A or not B:
            continue
        GA = G.subgraph(A)
        GB = G.subgraph(B)
        if nx.is_tree(GA) and nx.is_tree(GB):
            return True, (tuple(A), tuple(B))
    return False, None


def derived_level_graph_iso_classes(tris):
    """Compute the set of iso class signatures that are derived level
    graphs of some Even Level Graph."""
    iso_class_sigs = {canonical_sig(T) for T in tris}
    derived = set()
    for G in tris:
        if len(derived) == len(iso_class_sigs):
            break
        for source in get_level_sources(G):
            is_elg, levels = is_even_level_graph(G, source)
            if not is_elg:
                continue
            reached, _, _ = bfs_orbit(G, levels)
            derived.update(reached)
    return derived


def test_n(n):
    t0 = time.time()
    tris = enumerate_all_triangulations(n)
    iso_sigs = [canonical_sig(T) for T in tris]
    derived = derived_level_graph_iso_classes(tris)
    n_derived = sum(1 for s in iso_sigs if s in derived)

    # For iso classes that are NOT derived, check intertwining tree
    counterexamples = []
    n_intertwining_only = 0
    n_both = 0
    for i, G in enumerate(tris):
        is_derived = iso_sigs[i] in derived
        is_inter, partition = is_intertwining_tree(G)
        if is_derived and is_inter:
            n_both += 1
        elif is_derived:
            pass  # only derived
        elif is_inter:
            n_intertwining_only += 1
        else:
            counterexamples.append((i, G))

    n_total = len(tris)
    n_only_derived = n_derived - n_both
    elapsed = time.time() - t0
    return {
        'n': n,
        'total': n_total,
        'derived': n_derived,
        'intertwining_only': n_intertwining_only,
        'both': n_both,
        'only_derived': n_only_derived,
        'counterexamples': counterexamples,
        'elapsed': elapsed,
    }


def main():
    results = []
    for n in [6, 7, 8, 9, 10, 11, 12]:
        print(f'\n=== n = {n} ===')
        r = test_n(n)
        results.append(r)
        print(f'  total iso classes:    {r["total"]}')
        print(f'  derived only:         {r["only_derived"]}')
        print(f'  intertwining only:    {r["intertwining_only"]}')
        print(f'  both:                 {r["both"]}')
        print(f'  counterexamples:      {len(r["counterexamples"])}')
        print(f'  elapsed:              {r["elapsed"]:.1f}s')
        if r['counterexamples']:
            print(f'  COUNTEREXAMPLE FOUND. Stopping.')
            for i, G in r['counterexamples'][:3]:
                print(f'    iso[{i}] degree seq = '
                      f'{sorted([G.degree(v) for v in G.nodes()], reverse=True)}')
            break

    print('\n=== Final summary ===')
    print(f'{"n":>3} {"total":>6} {"deriv":>6} {"inter":>6} {"both":>6} {"missing":>8}')
    for r in results:
        cov = r['only_derived'] + r['intertwining_only'] + r['both']
        missing = r['total'] - cov
        print(f'{r["n"]:>3} {r["total"]:>6} {r["only_derived"]:>6} '
              f'{r["intertwining_only"]:>6} {r["both"]:>6} {missing:>8}')


if __name__ == '__main__':
    main()