Files
math-research/papers/even_level_graph_generators/experiments/test_conjecture.py
T
didericis c947ce75ff Add Even Level Graph Generators paper + extend Level Switching reachability
- New paper papers/even_level_graph_generators/: defines Even Level
  Graph (every level cycle even), derived level graphs, intertwining
  trees, and the disjunction conjecture (every maximal planar graph is
  a derived level graph or intertwining tree). Empirically tested
  through n=11: every iso class is at least an intertwining tree, so
  the disjunction holds trivially in this range. The intertwining tree
  disjunct fails at the Tutte graph dual (n=25), so the disjunction
  becomes non-trivial past some unknown threshold.

- Level Switching paper: adds Section 4 (Reachability via edge
  switches) with the two-step argument (Sleator-Tarjan-Thurston for
  Case 1; face-merges for Case 2) and Theorem 4.1 (O(n) edge switches
  suffice to reach all-depth-0).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-21 16:44:39 -04:00

173 lines
6.0 KiB
Python

"""Empirical test of the derived-level-graph conjecture for n=6..8.
For each iso class of maximal planar graphs G':
Search for an Even Level Graph G (some iso class, some level source)
such that G' is in the iso-class orbit of G under E/O-edge switches.
"""
import sys
import os
sys.path.insert(0, '/Users/didericis/Code/math-research/papers/'
'level_resolutions_of_maximal_planar_graphs/experiments')
import time
import itertools
import networkx as nx
from triangulation_gen import enumerate_all_triangulations
def canonical_sig(G):
"""Iso-class signature: WL hash via Weisfeiler-Lehman or just sorted
edge tuples up to vertex relabelling. We use nx.weisfeiler_lehman_graph_hash."""
return nx.weisfeiler_lehman_graph_hash(G)
def labelled_sig(G, labels):
"""Signature that respects both graph structure and a vertex labelling
(even/odd). Two graphs match iff there's an iso preserving labels."""
H = G.copy()
for v in H.nodes():
H.nodes[v]['label'] = labels[v]
return nx.weisfeiler_lehman_graph_hash(H, node_attr='label')
def bfs_levels(G, source_set):
"""BFS from a set of source vertices in G. Returns dict v -> level."""
levels = {v: float('inf') for v in G.nodes()}
frontier = list(source_set)
for v in frontier:
levels[v] = 0
d = 0
while frontier:
next_frontier = []
for u in frontier:
for w in G.neighbors(u):
if levels[w] > d + 1:
levels[w] = d + 1
next_frontier.append(w)
frontier = next_frontier
d += 1
return levels
def get_level_sources(G):
"""Yield each vertex as a possible level source (singleton set)."""
for v in G.nodes():
yield frozenset({v})
def is_even_level_graph(G, source):
"""Check: every level cycle of G (BFS from source) has even length."""
levels = bfs_levels(G, source)
if any(l == float('inf') for l in levels.values()):
return False, None
max_l = max(levels.values())
for k in range(max_l + 1):
L_k_nodes = [v for v in G.nodes() if levels[v] == k]
L_k = G.subgraph(L_k_nodes)
if L_k.number_of_edges() == 0:
continue
# Check bipartiteness (equivalent to no odd cycles)
if not nx.is_bipartite(L_k):
return False, None
return True, levels
def is_valid_parity_partition(G, labels):
"""Both induced subgraphs G[V_E] and G[V_O] are bipartite."""
V_E = [v for v in G.nodes() if labels[v] % 2 == 0]
V_O = [v for v in G.nodes() if labels[v] % 2 == 1]
return nx.is_bipartite(G.subgraph(V_E)) and nx.is_bipartite(G.subgraph(V_O))
def E_O_switches(G, labels):
"""Yield all triangulations reachable from G by one E/O-edge switch.
An E/O-edge has both endpoints of the same parity in `labels`."""
ip, emb = nx.check_planarity(G)
if not ip:
return
yielded = set()
for u, v in list(G.edges()):
if labels[u] % 2 != labels[v] % 2:
continue
f1 = emb.traverse_face(u, v)
f2 = emb.traverse_face(v, u)
if len(f1) != 3 or len(f2) != 3:
continue
w = next(x for x in f1 if x != u and x != v)
x = next(y for y in f2 if y != u and y != v)
if w == x or G.has_edge(w, x):
continue
Gp = G.copy()
Gp.remove_edge(u, v)
Gp.add_edge(w, x)
sig = frozenset(frozenset(e) for e in Gp.edges())
if sig in yielded:
continue
yielded.add(sig)
yield Gp
def bfs_orbit(G_start, labels, max_states=200000):
"""BFS in E/O-switch graph starting from G_start (with given labels).
Returns the set of iso classes (unlabelled) reachable."""
seen_labelled = {frozenset(frozenset(e) for e in G_start.edges())}
iso_classes_reached = {canonical_sig(G_start)}
frontier = [G_start]
rounds = 0
while frontier and len(seen_labelled) < max_states:
new = []
for G in frontier:
for Gp in E_O_switches(G, labels):
sig = frozenset(frozenset(e) for e in Gp.edges())
if sig in seen_labelled:
continue
seen_labelled.add(sig)
iso_classes_reached.add(canonical_sig(Gp))
new.append(Gp)
frontier = new
rounds += 1
return iso_classes_reached, len(seen_labelled), rounds
def test_for_n(n):
print(f'\n=== n = {n} ===')
t0 = time.time()
tris = enumerate_all_triangulations(n)
print(f' {len(tris)} iso classes of triangulations')
iso_class_sigs = {canonical_sig(T) for T in tris}
# Set of iso classes that ARE derived level graphs (of some ELG)
derived_iso_classes = set()
for i, G in enumerate(tris):
if len(derived_iso_classes) == len(iso_class_sigs):
break # early exit: everything is already covered
for source in get_level_sources(G):
is_elg, levels = is_even_level_graph(G, source)
if not is_elg:
continue
reached, n_lbld, rnds = bfs_orbit(G, levels)
new_count = len(reached - derived_iso_classes)
derived_iso_classes.update(reached)
if new_count > 0:
print(f' iso[{i}] source={sorted(source)}: ELG, '
f'orbit adds {new_count} new iso classes '
f'(orbit size {len(reached)}, '
f'{n_lbld} labelled, {rnds} rounds, '
f'total {len(derived_iso_classes)}/'
f'{len(iso_class_sigs)})')
missing = iso_class_sigs - derived_iso_classes
print(f' TOTAL: {len(derived_iso_classes)} / {len(iso_class_sigs)} '
f'iso classes are derived level graphs')
print(f' missing: {len(missing)}')
print(f' elapsed: {time.time() - t0:.1f}s')
return len(missing) == 0
if __name__ == '__main__':
import sys
ns = [int(x) for x in sys.argv[1:]] if len(sys.argv) > 1 else [6, 7, 8]
for n in ns:
ok = test_for_n(n)
print(f' conjecture holds for n={n}: {ok}')