Add Tutte-dual bridge-derivability test; rebuild artifacts
experiments/test_tutte_bridge.py: bridge-derivability test for the dual of the 46-vertex Tutte graph (a 25-vertex non-intertwining triangulation, since the Tutte graph is non-Hamiltonian) -- the conjecture's first case beyond the n=21 Holton-McKay duals. Reuses the fast integer-state bridge engine: per source labelling with bipartite parity subgraphs, run a backward bridge-orbit BFS for an Even Level Graph witness. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
@@ -0,0 +1,171 @@
|
||||
"""Bridge-derivability test for the Tutte-graph dual.
|
||||
|
||||
We take the classic 46-vertex Tutte graph (networkx `tutte_graph`), the
|
||||
1946 counterexample to Tait's conjecture, dualize it to a 25-vertex
|
||||
triangulation D, and ask whether D -- which is NOT an intertwining tree,
|
||||
since its dual is non-Hamiltonian -- is a *bridge-derived level graph*.
|
||||
This is the conjecture's first test outside the n=21 Holton-McKay duals.
|
||||
|
||||
Method (reuses the fast integer-state bridge engine in fast_decide):
|
||||
for each source s of D we form the BFS-parity labelling L (level mod 2),
|
||||
keep only those L for which both parity subgraphs of D are bipartite
|
||||
(a necessary condition, since bridge switches preserve bipartiteness),
|
||||
and run a backward bridge-orbit BFS looking for an Even Level Graph whose
|
||||
BFS-parity equals L. A witness proves D is bridge-derived; the BFS depth
|
||||
of the witness is the number of bridge switches from the ELG to D (the
|
||||
quantity tabulated for the n=21 duals). Not finding one within the
|
||||
state/time budget is inconclusive, not a disproof.
|
||||
"""
|
||||
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 tutte_dual_treecolor import dual_triangulation
|
||||
from fast_bridge import EdgeCode
|
||||
from fast_decide import expand_and_check
|
||||
|
||||
|
||||
def characterize(D):
|
||||
n = D.number_of_nodes()
|
||||
m = D.number_of_edges()
|
||||
is_tri = (m == 3 * n - 6)
|
||||
planar, _ = nx.check_planarity(D)
|
||||
# A triangulation is 4-connected iff it has no separating triangle,
|
||||
# i.e. iff #triangles == #faces == 2n-4. Extra triangles are separating
|
||||
# (dually: the cubic graph has a non-trivial 3-cut -> cyclically
|
||||
# 3-connected, not 5-connected).
|
||||
n_triangles = sum(nx.triangles(D).values()) // 3
|
||||
faces = 2 * n - 4
|
||||
sep_triangles = n_triangles - faces
|
||||
return {
|
||||
'n': n, 'm': m, 'is_triangulation': is_tri, 'planar': planar,
|
||||
'triangles': n_triangles, 'faces': faces,
|
||||
'separating_triangles': sep_triangles,
|
||||
'four_connected': sep_triangles == 0,
|
||||
}
|
||||
|
||||
|
||||
def valid_parity_partitions_via_coloring(D, max_partitions=400,
|
||||
max_colorings=2_000_000):
|
||||
"""A partition V = even u odd with both parity subgraphs bipartite is
|
||||
exactly a proper 4-coloring of D grouped {0,1}|{2,3} (each parity class
|
||||
is then 2-colored, hence bipartite). Enumerate proper 4-colorings by
|
||||
backtracking (fixing colour of the first vertex to break the 4! colour
|
||||
symmetry only partially) and collect the distinct induced partitions."""
|
||||
nodes = sorted(D.nodes())
|
||||
adj = {v: set(D.neighbors(v)) for v in nodes}
|
||||
# colour high-degree vertices first -> heavier pruning
|
||||
order = sorted(nodes, key=lambda v: -len(adj[v]))
|
||||
colors = {}
|
||||
parts = {} # canonical partition key -> labels dict
|
||||
n_col = [0]
|
||||
|
||||
def record():
|
||||
n_col[0] += 1
|
||||
even = frozenset(v for v in nodes if colors[v] in (0, 1))
|
||||
odd = frozenset(nodes) - even
|
||||
if not odd:
|
||||
return
|
||||
key = min((even, odd), key=lambda s: (len(s), tuple(sorted(s))))
|
||||
if key not in parts:
|
||||
parts[key] = {v: (0 if v in even else 1) for v in nodes}
|
||||
|
||||
def bt(i):
|
||||
if len(parts) >= max_partitions or n_col[0] >= max_colorings:
|
||||
return
|
||||
if i == len(order):
|
||||
record()
|
||||
return
|
||||
v = order[i]
|
||||
used = {colors[u] for u in adj[v] if u in colors}
|
||||
cap = 1 if i == 0 else 4 # fix first vertex's colour to 0
|
||||
for c in range(cap):
|
||||
if c in used:
|
||||
continue
|
||||
colors[v] = c
|
||||
bt(i + 1)
|
||||
del colors[v]
|
||||
if len(parts) >= max_partitions or n_col[0] >= max_colorings:
|
||||
return
|
||||
|
||||
bt(0)
|
||||
return list(parts.values()), n_col[0]
|
||||
|
||||
|
||||
def search_partition(code, labels, n, cap, time_limit):
|
||||
"""Backward bridge-orbit BFS tracking depth. Returns
|
||||
(status, n_states, depth_of_witness_or_None)."""
|
||||
s0 = code.state0
|
||||
seen = {s0}
|
||||
frontier = [s0]
|
||||
depth = 0
|
||||
t0 = time.time()
|
||||
while frontier and len(seen) < cap:
|
||||
if time.time() - t0 > time_limit:
|
||||
return 'timeout', len(seen), None
|
||||
new = []
|
||||
for st in frontier:
|
||||
wit, neigh = expand_and_check(st, code, labels, n)
|
||||
if wit:
|
||||
return 'found', len(seen), depth
|
||||
for ns in neigh:
|
||||
if ns not in seen:
|
||||
seen.add(ns)
|
||||
new.append(ns)
|
||||
if len(seen) >= cap:
|
||||
break
|
||||
if len(seen) >= cap:
|
||||
break
|
||||
frontier = new
|
||||
depth += 1
|
||||
return ('exhausted' if not frontier else 'capped'), len(seen), None
|
||||
|
||||
|
||||
def main(cap=400_000, time_limit=120.0):
|
||||
G = nx.tutte_graph()
|
||||
D, _ = dual_triangulation(G)
|
||||
info = characterize(D)
|
||||
print('Tutte graph: |V|=%d (classic 46-vertex Tait counterexample)'
|
||||
% G.number_of_nodes())
|
||||
print('Dual D: n=%(n)d, m=%(m)d, triangulation=%(is_triangulation)s, '
|
||||
'planar=%(planar)s' % info)
|
||||
print(' triangles=%(triangles)d, faces=%(faces)d, '
|
||||
'separating triangles=%(separating_triangles)d, '
|
||||
'4-connected=%(four_connected)s' % info)
|
||||
print(' [non-intertwining-tree by Thm: dual of a non-Hamiltonian C3CP]')
|
||||
|
||||
code = EdgeCode(D.nodes())
|
||||
code.state0 = code.state_of(D)
|
||||
n = info['n']
|
||||
|
||||
parts, n_col = valid_parity_partitions_via_coloring(D)
|
||||
print('\n%d distinct valid parity partitions collected '
|
||||
'(from %d proper 4-colorings)' % (len(parts), n_col))
|
||||
if not parts:
|
||||
print('No valid parity partition found: D is not bridge-derivable.')
|
||||
return
|
||||
|
||||
t0 = time.time()
|
||||
for k, labels in enumerate(parts):
|
||||
ev = sum(1 for v in labels if labels[v] == 0)
|
||||
st, sz, depth = search_partition(code, labels, n, cap, time_limit)
|
||||
tag = {'found': 'WITNESS', 'exhausted': 'exhausted (no witness)',
|
||||
'capped': 'CAP hit', 'timeout': 'TIMEOUT'}[st]
|
||||
if st == 'found' or (k + 1) % 20 == 0 or st in ('capped', 'timeout'):
|
||||
print(' partition %3d (even=%2d odd=%2d): %s [orbit>=%d, %.0fs]'
|
||||
% (k, ev, n - ev, tag, sz, time.time() - t0))
|
||||
if st == 'found':
|
||||
print('\n==> Tutte dual IS a bridge-derived level graph: '
|
||||
'ELG witness at %d bridge switches (partition %d).'
|
||||
% (depth, k))
|
||||
return
|
||||
print('\n==> No ELG witness found over %d valid partitions within budget '
|
||||
'(cap=%d, %.0fs/partition). INCONCLUSIVE.'
|
||||
% (len(parts), cap, time_limit))
|
||||
|
||||
|
||||
if __name__ == '__main__':
|
||||
main()
|
||||
Reference in New Issue
Block a user