"""Brute-force checks for Lemma 4.8 (short PCPs as LD_3 samples):
  1. for w = 4..10, the chain that splits a clause of width w into clauses of width 3 can be satisfied by
     the auxiliary variables when the clause is satisfied, and otherwise exactly one chain clause is violated;
  2. on 300 random small verifiers, the size bounds hold, and the minimum over the auxiliary variables of
     the number of violated entries equals the number of rejecting random strings.
Usage: python check_pcp_reduction.py
"""
import itertools, random, math
# chain gadget: clauses as lists of (kind, idx, sign): kind 'l' lambda index 1..w, 'y' index 1..w-3
def chain(w):
    cl=[[('l',1,1),('l',2,1),('y',1,1)]]
    for t in range(2,w-2):
        cl.append([('y',t-1,0),('l',t+1,1),('y',t,1)])
    cl.append([('y',w-3,0),('l',w-1,1),('l',w,1)])
    return cl
def val(lit,lam,y):
    k,i,s=lit; v = lam[i-1] if k=='l' else y[i-1]
    return v if s==1 else 1-v
for w in range(4,11):
    C=chain(w); assert len(C)==w-2
    for lam in itertools.product([0,1],repeat=w):
        best=min(sum(1 for c in C if not any(val(l,lam,y) for l in c)) for y in itertools.product([0,1],repeat=w-3))
        if any(lam):
            assert best==0
            j=lam.index(1)+1
            # paper's y: y_i=1 iff i<=j-2 ; check for every true lambda_j
            for j in [i+1 for i in range(w) if lam[i]]:
                y=[1 if i<=j-2 else 0 for i in range(1,w-2)]
                assert all(any(val(l,lam,y) for l in c) for c in C),(w,lam,j)
        else:
            assert best==1
print("chain OK w=4..10")
# random PCP-like verifier test of lem:pcp2ld soundness counting
random.seed(1)
for trial in range(300):
    q=random.randint(1,5); R=random.randint(1,6); ell=random.randint(1,min(7,q*R))
    V=[]
    for r in range(R):
        Q=random.sample(range(ell),random.randint(1,min(q,ell)))
        D={a:random.random()<0.6 for a in itertools.product([0,1],repeat=len(Q))}
        V.append((Q,D))
    # build entries: each entry is list of literals over vars: proof var p (int) or fresh ('y',k)
    entries=[]; nfresh=0; owner=[]
    for r,(Q,D) in enumerate(V):
        for a,acc in D.items():
            if acc: continue
            lits=[(Q[i], 1-a[i]) for i in range(len(Q))]  # literal true iff pi[Q[i]] != a[i]
            w=len(lits)
            if w<=3:
                entries.append([('p',)+l for l in lits]); owner.append(r)
            else:
                ys=list(range(nfresh,nfresh+w-3)); nfresh+=w-3
                entries.append([('p',)+lits[0],('p',)+lits[1],('y',ys[0],1)]); owner.append(r)
                for t in range(2,w-2):
                    entries.append([('y',ys[t-2],0),('p',)+lits[t],('y',ys[t-1],1)]); owner.append(r)
                entries.append([('y',ys[w-4],0),('p',)+lits[w-2],('p',)+lits[w-1]]); owner.append(r)
    assert len(entries)<=q*2**q*R, "S"
    assert ell+nfresh<=q*R+q*2**q*R, "N"
    if nfresh>12: continue
    for pi in itertools.product([0,1],repeat=ell):
        rej=sum(1 for Q,D in V if not D[tuple(pi[i] for i in Q)])
        best=None
        for y in itertools.product([0,1],repeat=nfresh):
            def lv(l):
                if l[0]=='p': return 1 if pi[l[1]]==l[2] else 0
                return y[l[1]] if l[2]==1 else 1-y[l[1]]
            e=sum(1 for c in entries if not any(lv(l) for l in c))
            best=e if best is None else min(best,e)
        assert best==rej,(best,rej)
print("pcp2ld: min_y errors == #rejecting rho, counts OK")