"""Evaluates the sums in the proof of Lemma 3.5 (width-reduction transfer) for several parameters, with
exact binomial coefficients, and checks with SymPy that a 3-CNF on n variables has fewer than 8n^3
non-tautological clauses.
Usage: python check_width_reduction_sums.py   (requires SymPy)
"""
from math import comb, log2, floor, e, sqrt
import sympy as sp
# widthred: large-leaf sum and leaf count, exact big-int arithmetic
for s in [1.0,0.5,0.25]:
  for c in [1,2]:
    C=2*(c+1)/s
    for n in [16,64,256,1024,4096]:
        k=floor(C*log2(n)); m=n**c
        if k<1: continue
        R=n//k
        lhs=sum(2.0**(log2(comb(m+r,r))-s*k*r) for r in range(R+1))  # normalized by 2^{sn}; log space avoids float overflow
        leaves=sum(comb(m+r,r) for r in range(R+1))
        ex=log2(leaves)/n
        print(f"s={s} c={c} n={n} k={k}  sum/2^sn={lhs:.4f} (<=e? {lhs<=e})  log2(#leaves)/n={ex:.3f} vs s/2={s/2}  small-leaf total exp/(sn)={(log2(leaves)+sqrt(n))/(s*n):.3f}")
# 3-CNF non-tautological clause count < 8 n^3
n=sp.symbols('n',positive=True,integer=True)
cnt=2*n+4*sp.binomial(n,2)+8*sp.binomial(n,3)
print(sp.simplify(sp.expand_func(8*n**3-cnt)))
print(sp.factor(sp.expand(sp.expand_func(sum(sp.binomial(2*n,j) for j in [1,2,3])))))