#!/usr/bin/env python3 """M8: Nullstellensatz-Grad ueber GF(2) vs. Bewegung des Loesungsraums (aus M7). Gleiche Instanzen wie M7 (bitgleich zu ebene1_dp.py; xor3p = XOR auf denselben Tripeln), beide als CNF gegeben (wie Resolution sie sieht). Braucht m7_bewegung.py und ebene1_dp.py im selben Ordner. Nullstellensatz (NS) ueber GF(2), multilinear (x^2 = x): Klausel C wird zum Polynom A_C = Produkt der Falsch-Indikatoren (positives Literal x -> 1+x, negatives -> x). Belegung verletzt C <=> A_C = 1. Widerlegung vom Grad d: Summe_C p_C * A_C = 1 mit deg(p_C * A_C) <= d. ns = kleinstes d mit Widerlegung (inkrementelle Gauss-Elimination ueber GF(2), Grad fuer Grad). gek=1 -> Zeit- oder Grad-Deckel erreicht, ns ist dann nur UNTERE Schranke. Bezug: PC-Grad <= NS-Grad. XOR-CNF ist in Grad 3 widerlegbar (vier Klauselpolynome summieren sich mod 2 zur linearen Gleichung) -> Gauss lebt in diesem System. Nur UNSAT-Instanzen haben einen NS-Grad. Dort ist die Loesungszahl 0, der Stoerfaktor aus M7 entfaellt. Nutzung: python3 m8_nsgrad.py --ns 10,12,14,16 --inst 60 --alphas 4.267,5.0 --dmax 7 --tmax 300 --jobs 15 """ import argparse, csv, math, sys, time from itertools import combinations from multiprocessing import Pool import m7_bewegung as M _IDX = {} def monom_index(n, dmax): if (n, dmax) not in _IDX: _IDX.clear(); idx = {}; k = 0 for d in range(dmax + 1): # Index waechst mit dem Grad -> Pivots hoher Grade oben for c in combinations(range(n), d): m = 0 for v in c: m |= 1 << v idx[m] = k; k += 1 _IDX[(n, dmax)] = idx return _IDX[(n, dmax)] def klausel_polynom(cl): neg, pos = 0, [] for l in cl: if l > 0: pos.append(l - 1) else: neg |= 1 << (-l - 1) monos = [] for r in range(len(pos) + 1): for c in combinations(pos, r): m = neg for v in c: m |= 1 << v monos.append(m) vmask = neg for v in pos: vmask |= 1 << v return monos, vmask def ns_grad(n, cnf, dmax, tmax): """-> (ns, gekappt, rang)""" idx = monom_index(n, dmax); piv = {}; t0 = time.time() K = [klausel_polynom(c) for c in cnf] dmin = max(len(c) for c in cnf) for d in range(dmin, dmax + 1): s = d - dmin for monos, vmask in K: rest = [v for v in range(n) if not (vmask >> v) & 1] for c in combinations(rest, s): mm = 0 for v in c: mm |= 1 << v row = 0 for mo in monos: row ^= 1 << idx[mo | mm] while row: p = row.bit_length() - 1 q = piv.get(p) if q is None: piv[p] = row; break row ^= q if 0 in piv: # Basiszeile == 1 -> 1 liegt im Erzeugnis return d, 0, len(piv) if time.time() - t0 > tmax: return d, 1, len(piv) # Grad d nicht fertig: ns >= d return dmax + 1, 1, len(piv) 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); eq = M.gen_xor_gepaart(tri, seed) rows = [] for typ, verl, cnf in (("sat3", M.verletzt_sat3(B, cls), cls), ("xor3p", M.verletzt_xor(B, eq), M.xor_cnf(eq))): base, d = M.bewegung(n, verl); k = M.kennzahlen(base, d) if base == 0: t = time.time(); ns, gek, rang = ns_grad(n, cnf, G["dmax"], G["tmax"]); dt = time.time() - t else: ns, gek, rang, dt = float("nan"), 0, 0, 0.0 rows.append(dict(n=n, alpha=alpha, i=i, typ=typ, **k, ns=ns, gek=gek, rang=rang, sek=round(dt, 2))) return rows def med(v): v = [x for x in v if not (isinstance(x, float) and math.isnan(x))] return float(sorted(v)[len(v) // 2]) if v else float("nan") def main(): ap = argparse.ArgumentParser() ap.add_argument("--ns", default="10,12,14,16") ap.add_argument("--inst", type=int, default=60) 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("--dmax", type=int, default=7) ap.add_argument("--tmax", type=float, default=300.0, help="Sekunden pro Instanz fuer die NS-Suche") ap.add_argument("--csv", default="m8_nsgrad.csv") ap.add_argument("--report", default="report_m8.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() with Pool(a.jobs, initializer=_init, initargs=(dict(dmax=a.dmax, tmax=a.tmax),)) as p: for k, rows in enumerate(p.imap_unordered(M.__dict__["job"] if False else job, keys), 1): R.extend(rows) 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) L = [f"M8 seed={a.seed} inst={a.inst} dmax={a.dmax} tmax={a.tmax}s (nur UNSAT-Instanzen haben einen NS-Grad)", ""] for al in als: L.append(f"===== alpha = {al} =====") L.append("typ n | UNSAT | NS-Grad Verteilung (Grad:Anzahl, * = untere Schranke) | ns med | gek | dist med (UNSAT) | sek med") for t in ("sat3", "xor3p"): for n in ns_: rr = [r for r in R if r["alpha"] == al and r["n"] == n and r["typ"] == t] uu = [r for r in rr if r["sol"] == 0] vert = {} for r in uu: key = f"{r['ns']}{'*' if r['gek'] else ''}"; vert[key] = vert.get(key, 0) + 1 vs = " ".join(f"{k}:{v}" for k, v in sorted(vert.items())) L.append(f"{t:5s} {n:3d} | {len(uu)/max(1,len(rr)):.2f} | {vs:40s} | {med([r['ns'] for r in uu]):5.1f} | " f"{sum(r['gek'] for r in uu):3d} | {med([r['dist'] for r in uu]):5.1f} | {med([r['sek'] for r in uu]):6.2f}") L.append("") L.append("Gepaart (Seed in beiden UNSAT): Anteil ns(sat3) > ns(xor3p) | Median Differenz") for n in ns_: S = {r["i"]: r for r in R if r["alpha"] == al and r["n"] == n and r["typ"] == "sat3" and r["sol"] == 0} X = {r["i"]: r for r in R if r["alpha"] == al and r["n"] == n and r["typ"] == "xor3p" and r["sol"] == 0} dd = [S[i]["ns"] - X[i]["ns"] for i in S if i in X] L.append(f" n={n:3d}: {sum(x > 0 for x in dd)/max(1,len(dd)):.2f} | {med(dd):+.1f} [{len(dd)}]") L.append("") L.append("Innerhalb sat3, nur UNSAT (Loesungszahl = 0, kein Stoerfaktor): Spearman") L.append(" n | rho(dist,ns) rho(H,ns) rho(frac0,ns) | Anteil gekappt [Anzahl]") for n in ns_: uu = [r for r in R if r["alpha"] == al and r["n"] == n and r["typ"] == "sat3" and r["sol"] == 0] if len(uu) < 6: L.append(f" {n:3d} | zu wenige ({len(uu)})"); continue nsv = [r["ns"] for r in uu] L.append(f" {n:3d} | {M.spearman([r['dist'] for r in uu], nsv):+.3f} {M.spearman([r['H'] for r in uu], nsv):+.3f} " f"{M.spearman([r['frac0'] for r in uu], nsv):+.3f} | {sum(r['gek'] for r in uu)/len(uu):.2f} [{len(uu)}]") L.append("") L += ["Lesart:", " - xor3p: erwartet ns = 3 immer (Gauss in GF(2) in Grad 3 ausdrueckbar). sat3: erwartet groesser und wachsend mit n.", " Das ist die Trennung, die Resolution (Weite in M7) NICHT sieht. Sieht NS sie, ist NS das richtige System fuer Lage 4.", " - rho(dist,ns) > 0 stabil ueber n: Bewegungsreichtum geht mit hohem NS-Grad -> die Bewegung misst die Haerte,", " die ein Gauss-faehiges System bezahlt. Nahe 0: auch hier getrennte Achsen.", " - Viele gekappte (*) -> ns nur untere Schranke; dann Korrelation nur fuer kleine n belastbar.", " - NS ist schwaecher als PC: hoher NS-Grad beweist keinen hohen PC-Grad. Kleiner NS-Grad ist dagegen hart (echte Widerlegung)."] txt = "\n".join(L); print(txt); open(a.report, "w").write(txt + "\n") if __name__ == "__main__": main()