#!/usr/bin/env python3 """M9: Beweis gegen Verfahren -- DP auf der ganzen Formel vs. DP auf einem minimalen unloesbaren Kern (MUS). Gleiche Instanzen wie M7/M8 (sat3, bitgleich zu ebene1_dp.py). Nur UNSAT-Instanzen. Keine XOR-DP (spart Zeit). Braucht m7_bewegung.py, m8_nsgrad.py, ebene1_dp.py im selben Ordner. Je UNSAT-Instanz: frac0, krit Anteil/Anzahl nicht-kritischer bzw. kritischer Klauseln (kritisch = in JEDEM MUS) mus Groesse eines MUS (Streichverfahren in Index-Reihenfolge; jeder Test = eine vektorisierte Operation) mus_r zweites MUS in umgekehrter Reihenfolge -> zeigt, wie stark die MUS-Groesse von der Wahl abhaengt l2cnf_f/weite_f DP (minres, ohne Subsumption) auf der ganzen Formel l2cnf_k/weite_k DP auf dem MUS ns_f / ns_k NS-Grad ueber GF(2) auf ganzer Formel / auf dem MUS (ns_k >= ns_f, weniger Axiome) XOR-Seite (xor3p, gleiche Tripel; Standard an, --ohne-xor zum Abschalten): MUS auf KLAUSEL-Ebene (das sieht Resolution), dazu mus_gl = MUS auf Gleichungs-Ebene, kvar = Variablen im Kern. ACHTUNG: der Klausel-Kern einer XOR-Instanz ist oft KEIN XOR-System mehr (einzelne der 4 Klauseln fallen weg). Deshalb zusaetzlich der Gleichungs-Kern (Spalten _g): minimales widerspruechliches Gleichungssystem, je 4 Klauseln. DP nur auf dem Kern (die volle XOR-DP ist ab n=16 ohnehin immer gekappt; --xor-voll erzwingt sie trotzdem). Frage: Ist XOR auf dem KERN fuer Resolution/DP so teuer wie 3-SAT? (bisheriger Ebene-1-Vergleich lief auf der ganzen Formel) Hypothese "Verfahren bezahlt Redundanz": rho(frac0,l2cnf_f) > 0 (wie M7/M8-Join), aber auf dem Kern verschwindet oder kippt der Zusammenhang, und l2cnf_k verhaelt sich wie der NS-Grad (steigt mit Kern-Enge / Kerngroesse). Nutzung: python3 m9_kern.py --ns 14,16,18,20 --inst 120 --alphas 4.267,5.0 --tmax 60 --jobs 15 """ import argparse, csv, math, sys, time import numpy as np from multiprocessing import Pool import m7_bewegung as M import m8_nsgrad as N def mus(n, verl, order): """Streich-MUS: Klausel j weglassen, wenn danach noch jede Belegung von einer Klausel verletzt wird.""" cnt = np.zeros(1 << n, np.uint16) for v in verl: cnt += v if (cnt == 0).any(): return None # erfuellbar keep = set(range(len(verl))) for j in order: v = verl[j] if not (v & (cnt == 1)).any(): # j ist fuer keine Belegung der einzige Verletzer cnt -= v; keep.discard(j) return sorted(keep) def dp(n, cls): import ebene1_dp mx, capped, _, w = ebene1_dp.dp(n, [frozenset(c) for c in cls], "minres", G["cap"], G["tmax"]) return math.log2(max(mx, 1)), w, int(capped) G = {} def _init(a): G.update(a) def kvar(cl): return len({abs(l) for c in cl for l in c}) def job(key): n, alpha, i, seed, ax = 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 = sat3_teil(n, alpha, i, B, cls, verl, base, d, ax) if base == 0 else [] if G["xor"]: eq = M.gen_xor_unabh(n, ax, seed) if ax is not None else M.gen_xor_gepaart(tri, seed) rows += xor_teil(n, alpha, i, B, eq, ax) return rows def sat3_teil(n, alpha, i, B, cls, verl, base, d, ax): k = M.kennzahlen(base, d); m = len(cls) K = mus(n, verl, range(m)); Kr = mus(n, verl, range(m - 1, -1, -1)) kcls = [cls[j] for j in K] cf, wf, gf = dp(n, cls); ck, wk, gk = dp(n, kcls) nf, nfg, _ = N.ns_grad(n, cls, G["dmax"], G["ns_tmax"]) nk, nkg, _ = N.ns_grad(n, kcls, G["dmax"], G["ns_tmax"]) return [dict(typ="sat3", n=n, alpha=alpha, alpha_x=ax, i=i, m=m, frac0=k["frac0"], krit=int((d > 0).sum()), dist=k["dist"], mus=len(K), mus_r=len(Kr), mus_gl=len(K), kvar=kvar(kcls), l2cnf_f=cf, weite_f=wf, gek_f=gf, l2cnf_k=ck, weite_k=wk, gek_k=gk, ns_f=nf, nsgek_f=nfg, ns_k=nk, nsgek_k=nkg, kvar_g=float("nan"), l2cnf_g=float("nan"), weite_g=float("nan"), gek_g=0, ns_g=float("nan"))] def xor_teil(n, alpha, i, B, eq, ax): rows = [] xcls = M.xor_cnf(eq); xv = M.verletzt_sat3(B, xcls) xb, xd = M.bewegung(n, xv) if xb == 0: xk = M.kennzahlen(xb, xd) XK = mus(n, xv, range(len(xcls))); XKr = mus(n, xv, range(len(xcls) - 1, -1, -1)) XG = mus(n, M.verletzt_xor(B, eq), range(len(eq))) xkc = [xcls[j] for j in XK] xcf, xwf, xgf = dp(n, xcls) if G["xor_voll"] else (float("nan"), float("nan"), 0) xck, xwk, xgk = dp(n, xkc) xnk, xnkg, _ = N.ns_grad(n, xkc, G["dmax"], G["ns_tmax"]) xgc = M.xor_cnf([eq[j] for j in XG]) # Gleichungs-Kern: Struktur bleibt XOR xcg, xwg, xgg = dp(n, xgc) xng, _, _ = N.ns_grad(n, xgc, G["dmax"], G["ns_tmax"]) rows.append(dict(typ="xor3p" if ax is None else "xor3", n=n, alpha=alpha, alpha_x=ax, i=i, m=len(xcls), frac0=xk["frac0"], krit=int((xd > 0).sum()), dist=xk["dist"], mus=len(XK), mus_r=len(XKr), mus_gl=len(XG), kvar=kvar(xkc), l2cnf_f=xcf, weite_f=xwf, gek_f=xgf, l2cnf_k=xck, weite_k=xwk, gek_k=xgk, ns_f=3, nsgek_f=0, ns_k=xnk, nsgek_k=xnkg, kvar_g=kvar(xgc), l2cnf_g=xcg, weite_g=xwg, gek_g=xgg, ns_g=xng)) 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 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=7) ap.add_argument("--ns-tmax", type=float, default=300.0) ap.add_argument("--ohne-xor", action="store_true") ap.add_argument("--alpha-xor", default="", help="z.B. 1.0,1.1: ungepaarte XOR (bitgleich ebene1_dp xor3) bei eigenem alpha," " der Reihe nach den --alphas zugeordnet. Leer = gepaart (gleiche Tripel).") ap.add_argument("--xor-voll", action="store_true", help="auch volle XOR-DP (teuer, ab n=16 immer gekappt)") ap.add_argument("--csv", default="m9_kern.csv") ap.add_argument("--report", default="report_m9.txt") a = ap.parse_args() ns_ = [int(x) for x in a.ns.split(",")]; als = [float(x) for x in a.alphas.split(",")] axs = [float(x) for x in a.alpha_xor.split(",")] if a.alpha_xor else [None] * len(als) if len(axs) != len(als): sys.exit("--alpha-xor braucht gleich viele Werte wie --alphas") AX = dict(zip(als, axs)) keys = [(n, al, i, a.seed * 1000003 + n * 7919 + i * 104729, AX[al]) 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(cap=a.cap, tmax=a.tmax, dmax=a.dmax, ns_tmax=a.ns_tmax, xor=not a.ohne_xor, xor_voll=a.xor_voll),)) as p: for k, r in enumerate(p.imap_unordered(job, keys), 1): if r: 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"M9 seed={a.seed} inst={a.inst} tmax={a.tmax}s (nur UNSAT sat3)", ""] for al in als: L.append(f"===== alpha = {al} =====") L.append(" n N | m krit mus mus_r | l2cnf ganz -> Kern | weite ganz -> Kern | ns ganz -> Kern | gek ganz/Kern") for n in ns_: rr = [r for r in R if r["alpha"] == al and r["n"] == n and r["typ"] == "sat3"] if not rr: continue L.append(f" {n:3d} {len(rr):3d} | {rr[0]['m']:3d} {med([r['krit'] for r in rr]):5.1f} {med([r['mus'] for r in rr]):5.1f} " f"{med([r['mus_r'] for r in rr]):5.1f} | {med([r['l2cnf_f'] for r in rr]):6.2f} -> {med([r['l2cnf_k'] for r in rr]):5.2f} | " f"{med([r['weite_f'] for r in rr]):5.1f} -> {med([r['weite_k'] for r in rr]):4.1f} | " f"{med([r['ns_f'] for r in rr]):4.1f} -> {med([r['ns_k'] for r in rr]):4.1f} | " f"{sum(r['gek_f'] for r in rr)}/{sum(r['gek_k'] for r in rr)}") L.append("") L.append("Spearman (nur nicht gekappte DP-Laeufe):") L.append(" n | rho(frac0,cnf_f) rho(frac0,cnf_k) | rho(mus,cnf_k) rho(mus,ns_f) rho(mus,ns_k) | rho(ns_k,cnf_k) | rho(frac0,mus) rho(mus,mus_r) [N]") for n in ns_: rr = [r for r in R if r["alpha"] == al and r["n"] == n and r["typ"] == "sat3" and not r["gek_f"] and not r["gek_k"]] if len(rr) < 6: L.append(f" {n:3d} | zu wenige ({len(rr)})"); continue g = lambda c: [float(r[c]) for r in rr] L.append(f" {n:3d} | {sp(g('frac0'), g('l2cnf_f')):+.3f} {sp(g('frac0'), g('l2cnf_k')):+.3f} | " f"{sp(g('mus'), g('l2cnf_k')):+.3f} {sp(g('mus'), g('ns_f')):+.3f} {sp(g('mus'), g('ns_k')):+.3f} | " f"{sp(g('ns_k'), g('l2cnf_k')):+.3f} | {sp(g('frac0'), g('mus')):+.3f} {sp(g('mus'), g('mus_r')):+.3f} [{len(rr)}]") L.append("") if not a.ohne_xor: ax = AX[al]; xt = "xor3p" if ax is None else "xor3" titel = "gepaart, gleiche Tripel" if ax is None else f"UNGEPAART, XOR bei alpha={ax}" L.append(f"XOR vs 3-SAT auf dem KERN ({titel}; Mediane ueber alle UNSAT-Instanzen):") L.append(" n N_sat/N_xor | Kern-Klauseln sat3/xor (xor Gl.) | Kern-Var sat3/xor/xorGl | l2cnf_k sat3/xor/xorGl | weite_k sat3/xor/xorGl | ns_k sat3/xor/xorGl | gek xor/xorGl | l2cnf je Kern-Var sat3/xorGl") stab = {"sat3": [], xt: []} for n in ns_: S = [r for r in R if r["alpha"] == al and r["n"] == n and r["typ"] == "sat3"] X = [r for r in R if r["alpha"] == al and r["n"] == n and r["typ"] == xt] if not S or not X: continue ms = lambda D, c: med([r[c] for r in D]) L.append(f" {n:3d} {len(S):3d}/{len(X):3d} | {ms(S,'mus'):5.1f} / {ms(X,'mus'):5.1f} ({ms(X,'mus_gl'):4.1f}) | " f"{ms(S,'kvar'):4.1f}/{ms(X,'kvar'):4.1f}/{ms(X,'kvar_g'):4.1f} | " f"{ms(S,'l2cnf_k'):5.2f}/{ms(X,'l2cnf_k'):5.2f}/{ms(X,'l2cnf_g'):5.2f} | " f"{ms(S,'weite_k'):4.1f}/{ms(X,'weite_k'):4.1f}/{ms(X,'weite_g'):4.1f} | " f"{ms(S,'ns_k'):3.1f}/{ms(X,'ns_k'):3.1f}/{ms(X,'ns_g'):3.1f} | " f"{sum(r['gek_k'] for r in X)}/{sum(r['gek_g'] for r in X)} | " f"{med([r['l2cnf_k']/r['kvar'] for r in S]):.3f} / {med([r['l2cnf_g']/r['kvar_g'] for r in X]):.3f}") stab["sat3"].append((n, ms(S, 'kvar'), ms(S, 'l2cnf_k'), ms(S, 'weite_k'))) stab[xt].append((n, ms(X, 'kvar_g'), ms(X, 'l2cnf_g'), ms(X, 'weite_g'))) for t, lab in (("sat3", "sat3 Kern "), (xt, "xor Gl.-Kern ")): v = stab[t] if len(v) >= 2: sl = lambda j: float(np.polyfit([x[0] for x in v], [x[j] for x in v], 1)[0]) L.append(f" Steigung je Variable n, {lab}: Kern-Var {sl(1):+.3f} l2cnf {sl(2):+.3f} weite {sl(3):+.3f}") L.append("") L.append("") L += ["Lesart:", " - Mit --alpha-xor: XOR bei eigenem Schwellenabstand (Schwelle 0.918; 1.0/1.1 ~ sat3 bei 4.267/5.0).", " Entscheidend sind die Steigungen der Kernkosten (l2cnf, weite je n) und l2cnf je Kern-Variable.", " - XOR-Kern: ist l2cnf_k(xor) >= l2cnf_k(sat3) bei vergleichbarer Kern-Variablenzahl, ist XOR auch auf dem Kern", " fuer Resolution nicht leichter -> Befund 'XORs Leichtigkeit liegt ganz auf Ebene 2' haelt. Faellt XOR deutlich", " darunter, war ein Teil der frueheren XOR-Ebene-1-Haerte Redundanz der Vier-Klausel-Kodierung.", " Kerne verschieden gross -> nicht nur Mediane, auch Kern-Var vergleichen (Kosten je Kern-Variable).", " - rho(frac0,cnf_f) > 0 reproduziert den M7/M8-Join (Verfahren teurer bei Redundanz).", " - Hypothese bestaetigt, wenn rho(frac0,cnf_k) gegen 0 faellt oder negativ wird und rho(mus,cnf_k) > 0:", " auf dem Kern bezahlt DP nur noch die Kern-Enge, wie der NS-Grad (rho(mus,ns_f) > 0 erwartet).", " - Bleibt rho(frac0,cnf_k) > 0, liegt der Gegenlauf NICHT an der Redundanz.", " - l2cnf ganz -> Kern: wie viel des DP-Aufwands reine Redundanz war.", " - rho(mus,mus_r) klein -> MUS-Groesse haengt stark an der Streichreihenfolge, dann ist 'mus' ein verrauschtes Mass;", " 'krit' (in jedem MUS) ist reihenfolgefrei."] txt = "\n".join(L); print(txt); open(a.report, "w").write(txt + "\n") if __name__ == "__main__": main()