b3b7b8cf26
- 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>
137 lines
4.6 KiB
Python
137 lines
4.6 KiB
Python
"""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
|