Optimize bridge-orbit engine (int-bitmask states, ~5x faster); measure feasibility
- fast_bridge.py: states as 210-bit integer edge-bitmasks (compact memory, O(1) set ops); build a NetworkX graph only once per state for the planar embedding; parity-subgraph bridges via one iterative DFS per state instead of per-edge subgraph copies. Validated identical orbits to the slow version; throughput ~5170 states/s vs ~1100 (graph.copy was 66% of old runtime). - fast_decide.py: integrated, gated ELG-witness check (only even-class sources with all-opposite-class neighbourhoods are tested with the ground-truth is_even_level_graph, then parity match). Witness detection validated (ELGs -> True, T*_9 -> False). - Feasibility finding: bridge orbits are ~100x smaller than full E/O orbits but still 1e5-1e6 states per labelling (partitions 0,1 of dual 0 exceed 310k and 685k without exhausting), x ~150 valid parity partitions per dual. Exhausting every orbit -- required for a conclusive NEGATIVE -- is computationally infeasible. A conclusive POSITIVE (witness ELG) remains reachable; none found so far. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
@@ -0,0 +1,136 @@
|
||||
"""Fast bridge-orbit machinery.
|
||||
|
||||
States are integer bitmasks over the 210 possible edges of a 21-vertex
|
||||
graph (edge (i,j), i<j -> a fixed bit). This makes the `seen` set and
|
||||
frontier compact and the set-difference/union O(1) int ops, eliminating
|
||||
all NetworkX graph copies. A NetworkX graph is built only once per state
|
||||
(needed for the planar embedding); parity-subgraph bridges are found with
|
||||
one iterative DFS per state instead of per-edge subgraph copies.
|
||||
"""
|
||||
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
|
||||
|
||||
|
||||
class EdgeCode:
|
||||
"""Bijection edge <-> bit index for a fixed vertex set."""
|
||||
def __init__(self, nodes):
|
||||
self.nodes = sorted(nodes)
|
||||
self.idx = {}
|
||||
self.edges = []
|
||||
b = 0
|
||||
n = len(self.nodes)
|
||||
for a in range(n):
|
||||
for c in range(a + 1, n):
|
||||
e = (self.nodes[a], self.nodes[c])
|
||||
self.idx[e] = b
|
||||
self.edges.append(e)
|
||||
b += 1
|
||||
self.nbits = b
|
||||
|
||||
def bit(self, u, v):
|
||||
return self.idx[(u, v)] if u < v else self.idx[(v, u)]
|
||||
|
||||
def state_of(self, G):
|
||||
s = 0
|
||||
for u, v in G.edges():
|
||||
s |= 1 << self.bit(u, v)
|
||||
return s
|
||||
|
||||
def edges_of(self, state):
|
||||
out = []
|
||||
s = state
|
||||
while s:
|
||||
b = (s & -s).bit_length() - 1
|
||||
out.append(self.edges[b])
|
||||
s &= s - 1
|
||||
return out
|
||||
|
||||
def graph_of(self, state):
|
||||
G = nx.Graph()
|
||||
G.add_nodes_from(self.nodes)
|
||||
G.add_edges_from(self.edges_of(state))
|
||||
return G
|
||||
|
||||
|
||||
def parity_bridges(adj_by_node):
|
||||
"""adj_by_node: dict node -> set(neighbors) for ONE parity subgraph.
|
||||
Return set of frozenset({u,v}) bridges (edges on no cycle). Iterative
|
||||
DFS lowlink."""
|
||||
bridges = set()
|
||||
visited = set()
|
||||
disc = {}
|
||||
low = {}
|
||||
timer = [0]
|
||||
for root in adj_by_node:
|
||||
if root in visited:
|
||||
continue
|
||||
# iterative DFS
|
||||
stack = [(root, None, iter(adj_by_node[root]))]
|
||||
visited.add(root)
|
||||
disc[root] = low[root] = timer[0]
|
||||
timer[0] += 1
|
||||
while stack:
|
||||
node, parent, it = stack[-1]
|
||||
advanced = False
|
||||
for nb in it:
|
||||
if nb == parent:
|
||||
continue
|
||||
if nb not in visited:
|
||||
visited.add(nb)
|
||||
disc[nb] = low[nb] = timer[0]
|
||||
timer[0] += 1
|
||||
stack.append((nb, node, iter(adj_by_node[nb])))
|
||||
advanced = True
|
||||
break
|
||||
else:
|
||||
low[node] = min(low[node], disc[nb])
|
||||
if not advanced:
|
||||
stack.pop()
|
||||
if stack:
|
||||
pnode = stack[-1][0]
|
||||
low[pnode] = min(low[pnode], low[node])
|
||||
if low[node] > disc[pnode]:
|
||||
bridges.add(frozenset((pnode, node)))
|
||||
return bridges
|
||||
|
||||
|
||||
def backward_bridge_states(state, code, labels):
|
||||
"""Yield neighbor STATES (ints) s' with s' -> state a bridge switch."""
|
||||
G = code.graph_of(state)
|
||||
ok, emb = nx.check_planarity(G)
|
||||
if not ok:
|
||||
return
|
||||
# parity adjacency for the two parity classes
|
||||
even_adj = {v: set() for v in code.nodes if labels[v] == 0}
|
||||
odd_adj = {v: set() for v in code.nodes if labels[v] == 1}
|
||||
for u, v in G.edges():
|
||||
pu, pv = labels[u], labels[v]
|
||||
if pu == 0 and pv == 0:
|
||||
even_adj[u].add(v); even_adj[v].add(u)
|
||||
elif pu == 1 and pv == 1:
|
||||
odd_adj[u].add(v); odd_adj[v].add(u)
|
||||
bridges = parity_bridges(even_adj) | parity_bridges(odd_adj)
|
||||
for u, v in G.edges():
|
||||
f1 = emb.traverse_face(u, v)
|
||||
if len(f1) != 3:
|
||||
continue
|
||||
f2 = emb.traverse_face(v, u)
|
||||
if len(f2) != 3:
|
||||
continue
|
||||
w = f1[0] if f1[0] != u and f1[0] != v else (f1[1] if f1[1] != u and f1[1] != v else f1[2])
|
||||
x = f2[0] if f2[0] != u and f2[0] != v else (f2[1] if f2[1] != u and f2[1] != v else f2[2])
|
||||
if w == x or G.has_edge(w, x):
|
||||
continue
|
||||
if labels[w] != labels[x]:
|
||||
continue # wx must be same-parity (flippable in predecessor)
|
||||
# uv is the NEW edge of switch s'->state; if same-parity it must be
|
||||
# a bridge of state's parity subgraph:
|
||||
if labels[u] == labels[v] and frozenset((u, v)) not in bridges:
|
||||
continue
|
||||
ns = state & ~(1 << code.bit(u, v))
|
||||
ns |= 1 << code.bit(w, x)
|
||||
yield ns
|
||||
@@ -0,0 +1,149 @@
|
||||
"""Fast exhaustive bridge-derivability decision for a dual.
|
||||
|
||||
For each valid parity partition L, exhaust the backward bridge-orbit
|
||||
(integer states) and look for an ELG witness with BFS-parity L. The ELG
|
||||
check is gated by a cheap filter: an ELG source s lies in one parity
|
||||
class and ALL its neighbours lie in the other (they are level 1), so only
|
||||
such candidate sources are fully tested.
|
||||
|
||||
YES (bridge-derived) as soon as any partition yields a witness; NO
|
||||
(conclusive) if all partitions' orbits are fully exhausted with no
|
||||
witness; INCONCLUSIVE if any orbit hits the cap.
|
||||
"""
|
||||
import sys
|
||||
import os
|
||||
import time
|
||||
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
|
||||
from collections import deque
|
||||
from load_holton_mckay import parse_planar_code
|
||||
from tutte_dual_treecolor import dual_triangulation
|
||||
from exhaustive_bridge import valid_parity_partitions
|
||||
from fast_bridge import EdgeCode, parity_bridges
|
||||
from test_conjecture import is_even_level_graph
|
||||
|
||||
|
||||
def _bfs_parity(adj, s, n):
|
||||
"""BFS distance parity from s over adjacency dict; returns dict v->parity
|
||||
or None if graph (restricted to reached) doesn't cover all n nodes."""
|
||||
par = {s: 0}
|
||||
dq = deque([s])
|
||||
while dq:
|
||||
u = dq.popleft()
|
||||
for w in adj[u]:
|
||||
if w not in par:
|
||||
par[w] = par[u] ^ 1
|
||||
dq.append(w)
|
||||
if len(par) != n:
|
||||
return None
|
||||
return par
|
||||
|
||||
|
||||
def expand_and_check(state, code, labels, n):
|
||||
"""Build G once; return (is_witness, list_of_neighbor_states)."""
|
||||
G = code.graph_of(state)
|
||||
adj = {v: set(G.neighbors(v)) for v in code.nodes}
|
||||
# --- ELG witness check (gated) ---
|
||||
# Necessary condition for BFS-parity(s)==L: s's whole neighbourhood is
|
||||
# the opposite class (level 1). Only such s are fully tested with the
|
||||
# ground-truth ELG check (all level subgraphs bipartite) + parity match.
|
||||
witness = False
|
||||
for s in code.nodes:
|
||||
cs = labels[s]
|
||||
nbrs = adj[s]
|
||||
if not nbrs or any(labels[w] == cs for w in nbrs):
|
||||
continue
|
||||
ok, lvls = is_even_level_graph(G, frozenset({s}))
|
||||
if not ok:
|
||||
continue
|
||||
if all((lvls[v] % 2 == 0) == (labels[v] == cs) for v in code.nodes):
|
||||
witness = True
|
||||
break
|
||||
# --- neighbours (backward bridge switches) ---
|
||||
neigh = []
|
||||
ok, emb = nx.check_planarity(G)
|
||||
if ok:
|
||||
even_adj = {v: set() for v in code.nodes if labels[v] == 0}
|
||||
odd_adj = {v: set() for v in code.nodes if labels[v] == 1}
|
||||
for u in code.nodes:
|
||||
for v in adj[u]:
|
||||
if u < v and labels[u] == labels[v]:
|
||||
if labels[u] == 0:
|
||||
even_adj[u].add(v); even_adj[v].add(u)
|
||||
else:
|
||||
odd_adj[u].add(v); odd_adj[v].add(u)
|
||||
bridges = parity_bridges(even_adj) | parity_bridges(odd_adj)
|
||||
for u, v in G.edges():
|
||||
f1 = emb.traverse_face(u, v)
|
||||
if len(f1) != 3:
|
||||
continue
|
||||
f2 = emb.traverse_face(v, u)
|
||||
if len(f2) != 3:
|
||||
continue
|
||||
w = next(a for a in f1 if a != u and a != v)
|
||||
x = next(b for b in f2 if b != u and b != v)
|
||||
if w == x or G.has_edge(w, x):
|
||||
continue
|
||||
if labels[w] != labels[x]:
|
||||
continue
|
||||
if labels[u] == labels[v] and frozenset((u, v)) not in bridges:
|
||||
continue
|
||||
ns = (state & ~(1 << code.bit(u, v))) | (1 << code.bit(w, x))
|
||||
neigh.append(ns)
|
||||
return witness, neigh
|
||||
|
||||
|
||||
def decide_partition(code, labels, n, cap):
|
||||
s0 = code.state0
|
||||
seen = {s0}
|
||||
frontier = [s0]
|
||||
while frontier and len(seen) < cap:
|
||||
new = []
|
||||
for st in frontier:
|
||||
wit, neigh = expand_and_check(st, code, labels, n)
|
||||
if wit:
|
||||
return 'found', len(seen)
|
||||
for ns in neigh:
|
||||
if ns not in seen:
|
||||
seen.add(ns)
|
||||
new.append(ns)
|
||||
frontier = new
|
||||
return ('exhausted' if not frontier else 'capped'), len(seen)
|
||||
|
||||
|
||||
def decide_dual(i, cap=4_000_000, log=print):
|
||||
graphs = parse_planar_code('experiments/nonham38m4.pc')
|
||||
G, _ = dual_triangulation(graphs[i][0])
|
||||
n = G.number_of_nodes()
|
||||
code = EdgeCode(G.nodes())
|
||||
code.state0 = code.state_of(G)
|
||||
parts = list(valid_parity_partitions(G))
|
||||
log(f'dual {i}: {len(parts)} partitions, n={n}', flush=True)
|
||||
t0 = time.time()
|
||||
any_capped = False
|
||||
max_orbit = 0
|
||||
for j, labels in enumerate(parts):
|
||||
st, sz = decide_partition(code, labels, n, cap)
|
||||
if st == 'found':
|
||||
log(f' partition {j}: WITNESS -> dual {i} IS bridge-derived '
|
||||
f'(orbit>={sz}, {time.time()-t0:.0f}s)', flush=True)
|
||||
return 'bridge-derived'
|
||||
if st == 'capped':
|
||||
any_capped = True
|
||||
log(f' partition {j}: CAP {sz} (inconclusive)', flush=True)
|
||||
else:
|
||||
max_orbit = max(max_orbit, sz)
|
||||
if (j + 1) % 10 == 0:
|
||||
log(f' ...{j+1}/{len(parts)} done, max_orbit={max_orbit}, '
|
||||
f'{time.time()-t0:.0f}s', flush=True)
|
||||
verdict = 'INCONCLUSIVE (cap hit)' if any_capped else 'NOT bridge-derived'
|
||||
log(f' dual {i}: {verdict} (max_orbit={max_orbit}, {time.time()-t0:.0f}s)',
|
||||
flush=True)
|
||||
return verdict
|
||||
|
||||
|
||||
if __name__ == '__main__':
|
||||
for idx in sys.argv[1:]:
|
||||
decide_dual(int(idx))
|
||||
@@ -0,0 +1,53 @@
|
||||
"""Measure the per-partition bridge-orbit size distribution for a dual,
|
||||
with a modest cap, logging each partition's orbit size and time. Tells us
|
||||
whether the slowness is a few giant orbits or uniformly heavy."""
|
||||
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
|
||||
from load_holton_mckay import parse_planar_code
|
||||
from tutte_dual_treecolor import dual_triangulation
|
||||
from bridge_derived_test import sig, backward_bridge_neighbors
|
||||
from exhaustive_bridge import valid_parity_partitions
|
||||
|
||||
|
||||
def orbit_size(G, labels, cap, time_cap):
|
||||
t0 = time.time()
|
||||
seen = {sig(G)}
|
||||
frontier = [G]
|
||||
while frontier and len(seen) < cap:
|
||||
if time.time() - t0 > time_cap:
|
||||
return len(seen), time.time() - t0, 'timecap'
|
||||
new = []
|
||||
for H in frontier:
|
||||
for Hp in backward_bridge_neighbors(H, labels):
|
||||
s = sig(Hp)
|
||||
if s not in seen:
|
||||
seen.add(s)
|
||||
new.append(Hp)
|
||||
frontier = new
|
||||
return len(seen), time.time() - t0, ('exhausted' if not frontier else 'cap')
|
||||
|
||||
|
||||
def main(i, cap=400000, time_cap=30):
|
||||
graphs = parse_planar_code('experiments/nonham38m4.pc')
|
||||
G, _ = dual_triangulation(graphs[i][0])
|
||||
parts = list(valid_parity_partitions(G))
|
||||
print(f'dual {i}: {len(parts)} partitions; cap={cap} time_cap={time_cap}s',
|
||||
flush=True)
|
||||
sizes = []
|
||||
for j, labels in enumerate(parts):
|
||||
n, dt, st = orbit_size(G, labels, cap, time_cap)
|
||||
sizes.append((n, st))
|
||||
print(f' [{j}] orbit={n} {st} {dt:.1f}s', flush=True)
|
||||
exhausted = [n for n, st in sizes if st == 'exhausted']
|
||||
unfinished = [(n, st) for n, st in sizes if st != 'exhausted']
|
||||
print(f'\nexhausted: {len(exhausted)}/{len(parts)}; '
|
||||
f'largest exhausted={max(exhausted) if exhausted else 0}; '
|
||||
f'unfinished={len(unfinished)}', flush=True)
|
||||
|
||||
|
||||
if __name__ == '__main__':
|
||||
main(int(sys.argv[1]) if len(sys.argv) > 1 else 0)
|
||||
@@ -0,0 +1,72 @@
|
||||
"""Diagnostic: per-partition bridge-orbit size distribution for a dual,
|
||||
logging EVERY partition. Separates BFS time from witness-check time, and
|
||||
records whether each orbit exhausted below the cap. Also reports if any
|
||||
witness is found (early YES)."""
|
||||
import sys
|
||||
import os
|
||||
import time
|
||||
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__)))
|
||||
from load_holton_mckay import parse_planar_code
|
||||
from tutte_dual_treecolor import dual_triangulation
|
||||
from exhaustive_bridge import valid_parity_partitions
|
||||
from fast_bridge import EdgeCode
|
||||
from fast_decide import expand_and_check
|
||||
|
||||
|
||||
def run(i, cap, time_cap):
|
||||
graphs = parse_planar_code('experiments/nonham38m4.pc')
|
||||
G, _ = dual_triangulation(graphs[i][0])
|
||||
n = G.number_of_nodes()
|
||||
code = EdgeCode(G.nodes())
|
||||
code.state0 = code.state_of(G)
|
||||
parts = list(valid_parity_partitions(G))
|
||||
print(f'dual {i}: {len(parts)} partitions, cap={cap}, time_cap={time_cap}s',
|
||||
flush=True)
|
||||
sizes = []
|
||||
for j, labels in enumerate(parts):
|
||||
t0 = time.time()
|
||||
seen = {code.state0}
|
||||
frontier = [code.state0]
|
||||
wit = False
|
||||
capped = False
|
||||
while frontier and len(seen) < cap:
|
||||
if time.time() - t0 > time_cap:
|
||||
capped = True
|
||||
break
|
||||
new = []
|
||||
for st in frontier:
|
||||
w, neigh = expand_and_check(st, code, labels, n)
|
||||
if w:
|
||||
wit = True
|
||||
break
|
||||
for ns in neigh:
|
||||
if ns not in seen:
|
||||
seen.add(ns)
|
||||
new.append(ns)
|
||||
if wit:
|
||||
break
|
||||
frontier = new
|
||||
if len(seen) >= cap:
|
||||
capped = True
|
||||
st_tag = 'WITNESS' if wit else ('cap' if capped else 'exhausted')
|
||||
sizes.append((len(seen), st_tag))
|
||||
print(f' [{j}] {st_tag} orbit={len(seen)} {time.time()-t0:.1f}s',
|
||||
flush=True)
|
||||
if wit:
|
||||
print(f'dual {i}: BRIDGE-DERIVED (witness at partition {j})',
|
||||
flush=True)
|
||||
return
|
||||
exh = [s for s, t in sizes if t == 'exhausted']
|
||||
capped_ct = sum(1 for s, t in sizes if t == 'cap')
|
||||
print(f'\ndual {i}: no witness. exhausted={len(exh)}/{len(parts)}, '
|
||||
f'capped={capped_ct}, largest_exhausted={max(exh) if exh else 0}',
|
||||
flush=True)
|
||||
|
||||
|
||||
if __name__ == '__main__':
|
||||
i = int(sys.argv[1]) if len(sys.argv) > 1 else 0
|
||||
cap = int(sys.argv[2]) if len(sys.argv) > 2 else 500000
|
||||
tcap = int(sys.argv[3]) if len(sys.argv) > 3 else 60
|
||||
run(i, cap, tcap)
|
||||
Reference in New Issue
Block a user