#!/usr/bin/env python3 """M12: PC-Grad ueber GF(2) auf grossen minimalen unloesbaren Kernen (n = 24-56) -- bleibt er bei 4? M11 (n <= 20, Kerne bis 19 Variablen): PC-Grad fast immer 4, konstant. M12 verlaengert die Reihe mit dem C++-Kern m12pc (DPLL-Streich-MUS statt 2^n-Tabelle; PC-Abschluss mit AVX2-XOR). Gleiche Instanz-Konstruktion und Seed-Formel wie M7-M11 (sat3 bitgleich zu ebene1_dp.py). Hauptfrage: Ab welcher Kern-Variablenzahl reicht Grad 4 nicht mehr? Standard --dmax 4: Ergebnis je Kern "3", "4" oder ">=5" (Grad-4-Abschluss erreicht den Fixpunkt ohne die 1 -- das ist ein exakter Befund, kein Abbruch). Grad 5 selbst braucht bei 40+ Variablen viele GB je Kern -> nur gezielt mit --dmax 5, wenigen --jobs, grossem --mem. Kontrollen: Tseitin auf zufaelligen 3-regulaeren Expandern (m10-Generator; ganze Formel = Kern) und XOR auf denselben Tripeln (Klausel-Kern) -- beide muessen PC-Grad 3 haben. --pruefen: Soundness (Kern minus erste Klausel darf bis Grad pc nicht widerlegt werden) und DP-Weite auf dem Kern (Obergrenze fuer den PC-Grad: weite < pc waere ein Fehler). Konvention: Multiplikation x*p nur fuer Grad(p) < d (wie M11). Eine grosszuegigere Konvention kann den Grad um 1 senken. Bauen: g++ -O3 -march=native -o m12pc m12pc.cpp Nutzung: python3 m12_grosskern.py --ns 24,28,32,36,40,44,48,52,56 --inst 60 --alphas 4.267,5.0 --jobs 12 --mem 3 --pruefen Braucht m7_bewegung.py, m10_tseitin.py, ebene1_dp.py und das Binary ./m12pc im selben Ordner. """ import argparse, csv, math, os, subprocess, sys, time import numpy as np from multiprocessing import Pool import m7_bewegung as M import m10_tseitin as T BIN = os.path.join(os.path.dirname(os.path.abspath(__file__)), "m12pc") 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 call(args, n, cls, timeout): s = f"{n} {len(cls)}\n" + "\n".join(" ".join(map(str, c)) + " 0" for c in cls) + "\n" try: return subprocess.run([BIN] + args, input=s, capture_output=True, text=True, timeout=timeout).stdout.split() except subprocess.TimeoutExpired: return [] def kern(n, cls): o = call(["mus"], n, cls, G["mus_tmax"]) if not o: return "zeit", None if o[0] == "SAT": return "sat", None return "unsat", [cls[int(j)] for j in o[1:]] def pc(cls, dmax): """-> (grad, status, rang, sek, MB). status: ok | ge (Fixpunkt bei dmax ohne 1: grad >= dmax+1) | zeit | speicher | absturz""" k, rc = relabel(cls) o = call(["pc", "3", str(dmax), str(G["pc_tmax"]), str(G["mem"])], k, rc, G["pc_tmax"] + 60) if len(o) < 5: return float("nan"), "absturz", 0, float("nan"), 0 g, gek, rang, sek, mb = int(o[0]), int(o[1]), int(o[2]), float(o[3]), int(o[4]) st = "ok" if gek == 0 and g <= dmax else ("ge" if gek == 0 else ("zeit" if gek == 1 else "speicher")) return g, st, rang, sek, mb G = {} def _init(a): G.update(a) def job(key): typ, n, alpha, i, seed = key rows = [] if typ == "sat3": tri, cls = M.gen_sat3(n, alpha, seed) st, kc = kern(n, cls) if st != "unsat": return [dict(typ="sat3", n=n, alpha=alpha, i=i, status=st)] g, ps, rang, sek, mb = pc(kc, G["dmax"]) row = dict(typ="sat3", n=n, alpha=alpha, i=i, status="unsat", m=len(cls), mus=len(kc), kvar=relabel(kc)[0], pc=g, pc_status=ps, rang=rang, sek=sek, mb=mb, sound=float("nan"), weite=float("nan")) if G["pruefen"]: if ps == "ok": g2, ps2, _, _, _ = pc(kc[1:], g) row["sound"] = float(not (ps2 == "ok" and g2 <= g)) import ebene1_dp k, rc = relabel(kc) mx, cap, _, w = ebene1_dp.dp(k, [frozenset(c) for c in rc], "minres", 400000, G["dp_tmax"]) if not cap: row["weite"] = w rows.append(row) if G["xor"]: eq = M.gen_xor_gepaart(tri, seed); xc = M.xor_cnf(eq) st, xk = kern(n, xc) if st == "unsat": g, ps, rang, sek, mb = pc(xk, 4) rows.append(dict(typ="xor3p", n=n, alpha=alpha, i=i, status="unsat", m=len(xc), mus=len(xk), kvar=relabel(xk)[0], pc=g, pc_status=ps, rang=rang, sek=sek, mb=mb, sound=float("nan"), weite=float("nan"))) else: # Tseitin-Kontrolle, n = Kantenzahl = 3V/2 V = n; rng = np.random.default_rng(seed) E = T.graph_expander(V, rng); nn, cls = T.tseitin(V, E, rng) g, ps, rang, sek, mb = pc(cls, 4) rows.append(dict(typ="tseitin", n=nn, alpha=float("nan"), i=i, status="unsat", m=len(cls), mus=len(cls), kvar=nn, pc=g, pc_status=ps, rang=rang, sek=sek, mb=mb, sound=float("nan"), weite=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 label(r): if r["pc_status"] == "ok": return str(int(r["pc"])) if r["pc_status"] == "ge": return f">={int(r['pc'])}" return r["pc_status"] def vert(rr): from collections import Counter c = Counter(label(r) for r in rr) return " ".join(f"{k}:{c[k]}" for k in sorted(c)) or "-" def main(): ap = argparse.ArgumentParser() ap.add_argument("--ns", default="24,28,32,36,40,44,48,52,56") ap.add_argument("--inst", type=int, default=60) ap.add_argument("--alphas", default="4.267,5.0") ap.add_argument("--tseitin", default="16,20,24,28,32", help="Knotenzahlen V (Variablen = 3V/2); leer = aus") ap.add_argument("--tseitin-inst", type=int, default=20) ap.add_argument("--jobs", type=int, default=12) ap.add_argument("--seed", type=int, default=11) ap.add_argument("--dmax", type=int, default=4) ap.add_argument("--mem", type=float, default=3.0, help="GB je PC-Lauf (Basiszeilen)") ap.add_argument("--pc-tmax", type=float, default=1800.0) ap.add_argument("--mus-tmax", type=float, default=600.0) ap.add_argument("--dp-tmax", type=float, default=60.0) ap.add_argument("--ohne-xor", action="store_true") ap.add_argument("--pruefen", action="store_true") ap.add_argument("--csv", default="m12_grosskern.csv") ap.add_argument("--report", default="report_m12.txt") a = ap.parse_args() if not os.path.exists(BIN): sys.exit("m12pc fehlt: g++ -O3 -march=native -o m12pc m12pc.cpp") ns_ = [int(x) for x in a.ns.split(",")]; als = [float(x) for x in a.alphas.split(",")] tv = [int(x) for x in a.tseitin.split(",")] if a.tseitin else [] keys = [("sat3", 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 += [("tseitin", V, 0.0, i, a.seed * 1000003 + V * 7919 + i * 104729 + 77777) for V in tv for i in range(a.tseitin_inst)] keys.sort(key=lambda k: -k[1]) R, t0 = [], time.time() cfg = dict(dmax=a.dmax, mem=a.mem, pc_tmax=a.pc_tmax, mus_tmax=a.mus_tmax, dp_tmax=a.dp_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) fields = ["typ", "n", "alpha", "i", "status", "m", "mus", "kvar", "pc", "pc_status", "rang", "sek", "mb", "sound", "weite"] with open(a.csv, "w", newline="") as f: w = csv.DictWriter(f, fieldnames=fields, restval=""); w.writeheader(); w.writerows(R) S = [r for r in R if r["typ"] == "sat3" and r["status"] == "unsat"] L = [f"M12 seed={a.seed} inst={a.inst} dmax={a.dmax} mem={a.mem}GB", ""] L.append("Pruefungen:") L.append(f" sat3 MUS-Zeitueberschreitungen: {sum(1 for r in R if r.get('status') == 'zeit')}") L.append(f" PC Abbrueche (zeit/speicher/absturz): {sum(1 for r in R if r.get('pc_status') in ('zeit', 'speicher', 'absturz'))}") if a.pruefen: sv = [r["sound"] for r in S if not math.isnan(r["sound"])] L.append(f" Soundness Kern-minus-Klausel: {int(sum(sv))}/{len(sv)} in Ordnung") bad = [r for r in S if not math.isnan(r["weite"]) and r["pc_status"] in ("ok", "ge") and r["weite"] < r["pc"]] L.append(f" DP-Weite < PC-Grad (darf nie vorkommen): {len(bad)} DP-Weite Median {med([r['weite'] for r in S]):.1f}") X = [r for r in R if r["typ"] == "xor3p"]; TS = [r for r in R if r["typ"] == "tseitin"] if X: L.append(f" XOR Klausel-Kern PC: {vert(X)} (erwartet nur 3)") if TS: L.append(f" Tseitin PC: {vert(TS)} (erwartet nur 3)") L.append("") for al in als: L.append(f"===== alpha = {al} =====") L.append(" n UNSAT/N | Kern-Klauseln Kern-Var | PC-Grad | Anteil >=5 | Sek Median/Max | MB max") for n in ns_: alle = [r for r in R if r["typ"] == "sat3" and r["alpha"] == al and r["n"] == n] rr = [r for r in alle if r["status"] == "unsat"] if not rr: continue ge5 = sum(1 for r in rr if r["pc_status"] == "ge" or (r["pc_status"] == "ok" and r["pc"] >= 5)) L.append(f" {n:3d} {len(rr):3d}/{len(alle):3d} | {med([r['mus'] for r in rr]):6.1f} {med([r['kvar'] for r in rr]):8.1f} | " f"{vert(rr):26s} | {ge5/len(rr):6.2f} | {med([r['sek'] for r in rr]):6.2f}/{max(r['sek'] for r in rr):7.1f} | {max(r['mb'] for r in rr)}") L.append("") L.append("Nach Kern-Variablenzahl (alle alpha zusammen) -- die Hauptkurve:") L.append(" Kern-Var N | PC-Grad | Anteil >=5") for lo, hi in ((0, 24), (25, 29), (30, 34), (35, 39), (40, 44), (45, 49), (50, 99)): rr = [r for r in S if lo <= r["kvar"] <= hi] if not rr: continue ge5 = sum(1 for r in rr if r["pc_status"] == "ge" or (r["pc_status"] == "ok" and r["pc"] >= 5)) L.append(f" {lo:2d}-{hi:2d} {len(rr):4d} | {vert(rr):26s} | {ge5/len(rr):.2f}") if TS: L.append("") L.append("Tseitin (Expander) nach Variablen: " + " ".join(f"{n}: {vert([r for r in TS if r['n'] == n])}" for n in sorted({r['n'] for r in TS}))) L += ["", "Lesart:", " - '>=5' heisst: der vollstaendige Grad-4-Abschluss enthaelt die 1 nicht. Das ist exakt, kein Zeitabbruch.", " - Steigt der Anteil >=5 mit der Kern-Variablenzahl von 0 auf 1, ist der erste Gradsprung der PC-Schranke sichtbar.", " - Tseitin und XOR bleiben bei 3 -> die Trennung XOR / 3-SAT bleibt auf Ebene 2 bestehen, und sie waechst.", " - Konvention: Multiplikation nur fuer Grad(p) < d. Eine grosszuegigere Konvention kann den Grad um 1 senken.", " - Grad 5 und hoeher exakt: --dmax 5 mit wenigen --jobs und grossem --mem, gezielt fuer einzelne n."] txt = "\n".join(L); print(txt) open(a.report, "w").write(txt + "\n") if __name__ == "__main__": main()