#!/usr/bin/env python3
"""M11: Polynomial-Calculus-Grad ueber GF(2) auf minimalen unloesbaren Kernen -- gegen NS-Grad und Kern-DP.

Messfrage: Hilft Wiederverwendung? NS (M8) muss die Widerlegung in einem Zug als Summe schreiben,
PC darf abgeleitete Polynome weiterverrechnen. PC-Grad <= NS-Grad und PC-Grad <= Resolutionsweite.
Theorie: fuer zufaelliges 3-CNF ist der PC-Grad auch ueber GF(2) linear in n (Alekhnovich & Razborov;
Ben-Sasson & Impagliazzo fuer Charakteristik > 2) -- asymptotisch, nicht bei n <= 20.

Gleiche Instanzen und Kerne wie M9 (Seed-Formel und MUS in Index-Reihenfolge identisch, bitgleich zu ebene1_dp.py).
Braucht m7_bewegung.py, m8_nsgrad.py, m9_kern.py, ebene1_dp.py im selben Ordner.

PC-Konvention: multilinear (x^2 = x), Grad nach Multilinearisierung; Multiplikation x*p nur fuer Grad(p) < d.
Ueber GF(2) ist die Negation 1+x linear, PC und PCR haben daher denselben Grad.
Verfahren je Grad d: Spann der Klauselpolynome, abgeschlossen unter x*p (Grad(p) < d), Gauss ueber GF(2)
bis zum Fixpunkt; 1 im Spann -> in Grad d widerlegt.

Je UNSAT-sat3-Instanz:
  pc_f, pc_k       PC-Grad auf ganzer Formel / auf dem Kern (pc_f <= pc_k)
  ns_k             NS-Grad auf dem Kern (wie M9)
  l2cnf_k, weite_k DP minres auf dem Kern (wie M9)
  pc_rang          Basisgroesse beim Finden der 1 im Grad pc_k (heuristisch, haengt an der Abarbeitung)
XOR (gepaart, gleiche Tripel): PC auf Gleichungs-Kern (erwartet 3) und Klausel-Kern (Fragilitaet: NS war 4-6).
Pruefungen (immer): pc_k <= ns_k, pc_k <= weite_k, pc_f <= pc_k, XOR-Gleichungs-Kern = 3.
--pruefen: zusaetzlich Soundness -- Kern minus eine Klausel ist erfuellbar und darf bis Grad pc_k nicht widerlegt werden.
Nutzung:  python3 m11_pcgrad.py --ns 14,16,18,20 --inst 120 --alphas 4.267,5.0 --jobs 15 --pruefen
"""
import argparse, csv, math, sys, time
import numpy as np
from multiprocessing import Pool
import m7_bewegung as M
import m8_nsgrad as N
import m9_kern as K

# ---------------- PC-Grad ----------------
def relabel(cnf):
    vs = sorted({abs(l) for c in cnf for l in c}); mp = {v: j + 1 for j, v in enumerate(vs)}
    return len(vs), [tuple((1 if l > 0 else -1) * mp[abs(l)] for l in c) for c in cnf]

def pc_grad_d(k, cnf, d, tmax, t0):
    """-> (True/False/None, basisgroesse). True: 1 abgeleitet; False: Fixpunkt ohne 1; None: Zeit."""
    idx = N.monom_index(k, d); inv = {i: m for m, i in idx.items()}
    lowmax = sum(1 for m in idx if bin(m).count("1") < d)   # Indizes < lowmax haben Grad < d
    mul = [[idx[inv[i] | (1 << x)] if i < lowmax else -1 for i in range(len(idx))] for x in range(k)]
    piv, queue = {}, []
    def insert(row):
        while row:
            p = row.bit_length() - 1; q = piv.get(p)
            if q is None:
                piv[p] = row
                if p < lowmax: queue.append(row)        # Echelon nach Grad: diese Zeilen spannen V ∩ Grad<d
                return p == 0
            row ^= q
        return False
    for c in cnf:
        monos, _ = N.klausel_polynom(c); row = 0
        for mo in monos: row ^= 1 << idx[mo]
        if insert(row): return True, len(piv)
    while queue:
        r = queue.pop(); bitsr = []; x = r
        while x:
            b = x.bit_length() - 1; bitsr.append(b); x ^= 1 << b
        for v in range(k):
            mv = mul[v]; row = 0
            for b in bitsr: row ^= 1 << mv[b]
            if row and insert(row): return True, len(piv)
        if time.time() - t0 > tmax: return None, len(piv)
    return False, len(piv)

def pc_grad(cnf, dmax, tmax):
    """-> (grad, gekappt, rang). grad = dmax+1, gekappt=0: bis dmax sicher nicht widerlegt."""
    k, rc = relabel(cnf); t0 = time.time()
    for d in range(max(len(c) for c in rc), dmax + 1):
        r, rang = pc_grad_d(k, rc, d, tmax, t0)
        if r is None: return d, 1, rang                   # Grad d nicht fertig: pc >= d
        if r: return d, 0, rang
    return dmax + 1, 0, 0

# ---------------- Messung ----------------
G = {}
def _init(a): G.update(a)

def job(key):
    n, alpha, i, seed = key
    B = M.bits(n); tri, cls = M.gen_sat3(n, alpha, seed); verl = M.verletzt_sat3(B, cls)
    base, d = M.bewegung(n, verl); rows = []
    K._init(dict(cap=G["cap"], tmax=G["tmax"]))          # m9.dp liest seine Parameter aus m9.G
    if base == 0:
        kz = M.kennzahlen(base, d)
        Km = K.mus(n, verl, range(len(cls))); kc = [cls[j] for j in Km]
        t = time.time(); pk, pkg, rang = pc_grad(kc, G["dmax"], G["pc_tmax"]); tpc = time.time() - t
        pf, pfg, _ = pc_grad(cls, pk, G["pc_tmax"]) if not pkg else (float("nan"), 1, 0)
        kk, rk = relabel(kc)
        nk, nkg, _ = N.ns_grad(kk, rk, G["dmax"], G["ns_tmax"])
        ck, wk, gk = K.dp(n, kc)
        sound = float("nan")
        if G["pruefen"] and not pkg:
            sound = 1.0
            for j in sorted({0, len(kc) // 2, len(kc) - 1}):
                g2, _, _ = pc_grad(kc[:j] + kc[j + 1:], pk, G["pc_tmax"])
                if g2 <= pk: sound = 0.0
        rows.append(dict(typ="sat3", n=n, alpha=alpha, i=i, m=len(cls), frac0=kz["frac0"], krit=int((d > 0).sum()),
                         dist=kz["dist"], mus=len(kc), kvar=K.kvar(kc), pc_k=pk, pcgek_k=pkg, pc_rang=rang,
                         pc_sek=round(tpc, 2), pc_f=pf, pcgek_f=pfg, ns_k=nk, nsgek_k=nkg,
                         l2cnf_k=ck, weite_k=wk, gek_k=gk, sound=sound))
    if G["xor"]:
        eq = M.gen_xor_gepaart(tri, seed); xcls = M.xor_cnf(eq); xv = M.verletzt_sat3(B, xcls)
        xb, xd = M.bewegung(n, xv)
        if xb == 0:
            XG = K.mus(n, M.verletzt_xor(B, eq), range(len(eq))); xgc = M.xor_cnf([eq[j] for j in XG])
            XK = K.mus(n, xv, range(len(xcls))); xkc = [xcls[j] for j in XK]
            pg, pgg, _ = pc_grad(xgc, G["dmax"], G["pc_tmax"])
            pk, pkg, _ = pc_grad(xkc, G["dmax"], G["pc_tmax"])
            nk, nkg, _ = N.ns_grad(*relabel(xkc), G["dmax"], G["ns_tmax"])
            rows.append(dict(typ="xor3p", n=n, alpha=alpha, i=i, m=len(xcls), frac0=float("nan"), krit=0,
                             dist=0, mus=len(XK), kvar=K.kvar(xkc), pc_k=pk, pcgek_k=pkg, pc_rang=0, pc_sek=0,
                             pc_f=pg, pcgek_f=pgg, ns_k=nk, nsgek_k=nkg,
                             l2cnf_k=float("nan"), weite_k=float("nan"), gek_k=0, sound=float("nan")))
    return rows

def med(v):
    v = [x for x in v if not (isinstance(x, float) and math.isnan(x))]
    return float(np.median(v)) if v else float("nan")

def vert(v):
    vals, cts = np.unique([x for x in v if not math.isnan(x)], return_counts=True)
    return " ".join(f"{int(a)}:{c}" for a, c in zip(vals, cts)) or "-"

def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--ns", default="14,16,18,20")
    ap.add_argument("--inst", type=int, default=120)
    ap.add_argument("--alphas", default="4.267,5.0")
    ap.add_argument("--jobs", type=int, default=15)
    ap.add_argument("--seed", type=int, default=11)
    ap.add_argument("--cap", type=int, default=400000)
    ap.add_argument("--tmax", type=float, default=60.0, help="Sekunden je DP-Lauf")
    ap.add_argument("--dmax", type=int, default=8)
    ap.add_argument("--pc-tmax", type=float, default=600.0)
    ap.add_argument("--ns-tmax", type=float, default=300.0)
    ap.add_argument("--ohne-xor", action="store_true")
    ap.add_argument("--pruefen", action="store_true", help="Soundness: Kern minus Klausel darf nicht widerlegt werden")
    ap.add_argument("--csv", default="m11_pcgrad.csv")
    ap.add_argument("--report", default="report_m11.txt")
    a = ap.parse_args()
    ns_ = [int(x) for x in a.ns.split(",")]; als = [float(x) for x in a.alphas.split(",")]
    keys = [(n, al, i, a.seed * 1000003 + n * 7919 + i * 104729) for al in als for n in ns_ for i in range(a.inst)]
    keys.sort(key=lambda k: -k[0])
    R, t0 = [], time.time()
    cfg = dict(cap=a.cap, tmax=a.tmax, dmax=a.dmax, pc_tmax=a.pc_tmax, ns_tmax=a.ns_tmax, xor=not a.ohne_xor, pruefen=a.pruefen)
    with Pool(a.jobs, initializer=_init, initargs=(cfg,)) as p:
        for k, r in enumerate(p.imap_unordered(job, keys), 1):
            R.extend(r)
            if k % max(1, len(keys) // 40) == 0 or k == len(keys):
                el = time.time() - t0
                print(f"[{k}/{len(keys)}] {el/60:6.1f} min, Rest ~{el/k*(len(keys)-k)/60:6.1f} min", file=sys.stderr, flush=True)
    with open(a.csv, "w", newline="") as f:
        w = csv.DictWriter(f, fieldnames=list(R[0].keys())); w.writeheader(); w.writerows(R)

    sp = M.spearman
    L = [f"M11  seed={a.seed}  inst={a.inst}  dmax={a.dmax}  (Kerne wie M9)", ""]
    S_all = [r for r in R if r["typ"] == "sat3"]; X_all = [r for r in R if r["typ"] == "xor3p"]
    L.append("Pruefungen:")
    L.append(f"  sat3: pc_k > ns_k: {sum(1 for r in S_all if not r['pcgek_k'] and not r['nsgek_k'] and r['pc_k'] > r['ns_k'])}"
             f"   pc_k > weite_k: {sum(1 for r in S_all if not r['pcgek_k'] and not r['gek_k'] and r['pc_k'] > r['weite_k'])}"
             f"   pc_f > pc_k: {sum(1 for r in S_all if not r['pcgek_f'] and not r['pcgek_k'] and r['pc_f'] > r['pc_k'])}"
             f"   (alle drei muessen 0 sein)")
    if a.pruefen:
        sv = [r["sound"] for r in S_all if not math.isnan(r["sound"])]
        L.append(f"  Soundness Kern-minus-Klausel: {int(sum(sv))}/{len(sv)} in Ordnung")
    if X_all:
        L.append(f"  XOR Gleichungs-Kern PC-Grad: {vert([r['pc_f'] for r in X_all])}   (erwartet nur 3)")
    L.append(f"  gekappt: pc_k {sum(r['pcgek_k'] for r in S_all)}  ns_k {sum(r['nsgek_k'] for r in S_all)}  dp_k {sum(r['gek_k'] for r in S_all)}")
    L.append("")
    for al in als:
        L.append(f"===== alpha = {al} =====")
        L.append("   n   N | Kern-Var | PC-Grad Kern      | PC-Grad ganz     | NS-Grad Kern     | weite_k | NS-PC Median | PC-Sek Median/Max")
        for n in ns_:
            rr = [r for r in S_all if r["alpha"] == al and r["n"] == n]
            if not rr: continue
            L.append(f" {n:3d} {len(rr):3d} | {med([r['kvar'] for r in rr]):5.1f}    | {vert([r['pc_k'] for r in rr]):17s} | "
                     f"{vert([r['pc_f'] for r in rr]):16s} | {vert([r['ns_k'] for r in rr]):16s} | {med([r['weite_k'] for r in rr]):5.1f}   | "
                     f"{med([r['ns_k'] - r['pc_k'] for r in rr]):5.1f}        | {med([r['pc_sek'] for r in rr]):.2f}/{max(r['pc_sek'] for r in rr):.2f}")
        L.append("")
        L.append("Spearman, nur ungekappt (PC-Grad nimmt wenige Werte an -> rho grob; pc_rang ist heuristisch):")
        L.append("   n | rho(pc_k,ns_k) rho(pc_k,l2cnf_k) rho(pc_k,frac0) rho(pc_k,krit) rho(pc_k,kvar) | rho(pc_rang,l2cnf_k) rho(pc_rang,kvar)  [N]")
        for n in ns_:
            rr = [r for r in S_all if r["alpha"] == al and r["n"] == n and not r["pcgek_k"] and not r["nsgek_k"] and not r["gek_k"]]
            if len(rr) < 6 or len({r["pc_k"] for r in rr}) < 2:
                L.append(f" {n:3d} | PC-Grad konstant oder zu wenige ({len(rr)})" if rr else f" {n:3d} | -")
                if len(rr) >= 6:
                    g = lambda c: [float(r[c]) for r in rr]
                    L.append(f"     | rho(pc_rang,l2cnf_k) {sp(g('pc_rang'), g('l2cnf_k')):+.3f}  rho(pc_rang,kvar) {sp(g('pc_rang'), g('kvar')):+.3f}")
                continue
            g = lambda c: [float(r[c]) for r in rr]
            L.append(f" {n:3d} | {sp(g('pc_k'), g('ns_k')):+.3f}  {sp(g('pc_k'), g('l2cnf_k')):+.3f}  {sp(g('pc_k'), g('frac0')):+.3f}  "
                     f"{sp(g('pc_k'), g('krit')):+.3f}  {sp(g('pc_k'), g('kvar')):+.3f} | {sp(g('pc_rang'), g('l2cnf_k')):+.3f}  "
                     f"{sp(g('pc_rang'), g('kvar')):+.3f}  [{len(rr)}]")
        if X_all:
            L.append("")
            L.append("XOR gepaart (gleiche Tripel): PC Gleichungs-Kern | PC Klausel-Kern | NS Klausel-Kern")
            for n in ns_:
                X = [r for r in X_all if r["alpha"] == al and r["n"] == n]
                if X:
                    L.append(f" {n:3d} {len(X):3d} | {vert([r['pc_f'] for r in X]):12s} | {vert([r['pc_k'] for r in X]):16s} | {vert([r['ns_k'] for r in X])}")
        L.append("")
    L += ["Lesart:",
          " - PC deutlich unter NS auf denselben Kernen: Wiederverwendung zaehlt, der NS-Grad aus M8 hat die Haerte",
          "   ueberschaetzt. PC = NS: bei dieser Groesse bringt Wiederverwendung nichts.",
          " - Entscheidend ist, ob der PC-Grad mit n waechst (Theorie: linear, aber erst asymptotisch) oder bei n <= 20 konstant bleibt.",
          " - XOR Klausel-Kern: steigt der PC-Grad dort ueber 3 wie beim NS (4-6), ist die Fragilitaet von Ebene 2 auch in PC da;",
          "   bleibt er bei 3, repariert PC die fehlenden Klauseln selbst.",
          " - Konvention: Multiplikation nur fuer Grad(p) < d. Andere Konventionen koennen den Grad um 1 verschieben.",
          " - PC-Grad nimmt nur wenige Werte an; Korrelationen darauf sind grob. pc_rang haengt an der Abarbeitungsreihenfolge."]
    txt = "\n".join(L); print(txt)
    open(a.report, "w").write(txt + "\n")

if __name__ == "__main__":
    main()