"""Stage 5: collect the robustness artifacts into results/robustness/summary.json and merge them under the key "robustness" of results/metrics.json (nothing else in metrics.json is modified). Every number printed in results/robustness.md is taken from here.""" import json import os import re ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__)))) os.chdir(ROOT) R = "results/robustness" def load(name): p = os.path.join(R, name) return json.load(open(p)) if os.path.exists(p) else None def parse_ff(path): rows = [] if not os.path.exists(path): return rows for line in open(path): m = re.match(r"n=(\d+) k=5 s=(\d+) TOTAL enumerated=(\d+) forcing=(\d+)", line) if m: rows.append({"n": int(m.group(1)), "s": int(m.group(2)), "enumerated": int(m.group(3)), "forcing": int(m.group(4))}) return rows def parse_times(path): out = [] if not os.path.exists(path): return out for line in open(path): m = re.search(r"([\d.]+) real\s+([\d.]+) user", line) if m: out.append((float(m.group(1)), float(m.group(2)))) return out summary = {} ff = parse_ff(os.path.join(R, "ff_brute_stdout.txt")) + parse_ff(os.path.join(R, "ff_brute_stdout_31_40.txt")) times = parse_times(os.path.join(R, "ff_brute_time.txt")) + parse_times(os.path.join(R, "ff_brute_time_31_40.txt")) summary["ff_brute"] = { "rows": ff, "instances": len(ff), "size11_zero_forcing_n": sorted(r["n"] for r in ff if r["s"] == 11 and r["forcing"] == 0 and r["n"] >= 23), "largest_n_size11_exhausted": max([r["n"] for r in ff if r["s"] == 11 and r["forcing"] == 0] or [0]), "total_sets_tested": sum(r["enumerated"] for r in ff), "total_wall_seconds": round(sum(t[0] for t in times), 1), "total_cpu_seconds": round(sum(t[1] for t in times), 1), "n23_s11_enumerated": next((r["enumerated"] for r in ff if r["n"] == 23 and r["s"] == 11), None), "n25_s11_enumerated": next((r["enumerated"] for r in ff if r["n"] == 25 and r["s"] == 11), None), "n23_s12_forcing_sets": next((r["forcing"] for r in ff if r["n"] == 23 and r["s"] == 12), None), } # agreement with the table for n = 11..22 import csv Z = {int(r["n"]): int(r["Z"]) for r in csv.DictReader(open("results/exact_values.csv"))} agree = True for n in range(11, 23): lo = [r for r in ff if r["n"] == n and r["s"] == Z[n] - 1] hi = [r for r in ff if r["n"] == n and r["s"] == Z[n]] agree &= bool(lo) and lo[0]["forcing"] == 0 and bool(hi) and hi[0]["forcing"] > 0 summary["ff_brute"]["table_11_to_22_reproduced"] = agree wr = load("witness_replay.json") summary["witness_replay"] = {"witnesses": wr["num_witnesses"], "all_ok": wr["all_ok"], "P7_range": wr["P7_range"], "P7_all_ok": all(p["ok"] for p in wr["P7"]), "n_with_size_Z_witness": wr["n_with_size_Z_witness"]} if wr else None cnt = load("enumeration_counts_check.json") summary["enumeration_counts"] = {"rows": len(cnt["rows"]), "mismatches": cnt["mismatches"], "all_n_consistent": cnt["all_n_consistent"]} if cnt else None enc = load("boundary_encoding_check.json") summary["boundary_encoding"] = {"instances": enc["num_instances"], "all_ok": enc["all_ok"], "table_cells_compared": enc["table_cells_compared"], "table_cells_consistent": enc["table_cells_consistent"]} if enc else None dl = load("deletion_lemma.json") summary["deletion_lemma"] = {"D1_cases": dl["D1"]["cases"], "D1_failures": dl["D1"]["failures"], "D2_cases": dl["D2"]["cases"], "D2_f_undefined": dl["D2"]["f_undefined_on_N[X]"], "D2_boundary_size_changed": dl["D2"]["boundary_size_changed"], "D3_instances": dl["D3_instances_found"], "D3_ok": dl["D3_ok"], "D3_p16_boundary11_with_gap_at_n0": [r["n0"] for r in dl["D3"] if r["instance_found"] and r["p"] == 16]} if dl else None dc = load("drat_negative_controls.json") summary["drat_controls"] = {"controls_behave": dc["controls_behave"], "beta_18_26_exact": dc["beta_18_26_exact"], "truncated_rejected": not dc["C1_truncated_proof"]["verified"], "weaker_cnf_rejected": not dc["C2_weaker_formula"]["verified"], "wrong_cnf_rejected": not dc["C3_proof_against_n27_cnf"]["verified"], "original_verified": dc["C4_positive_original"]["verified"]} if dc else None mg = load("margin.json") summary["margin"] = {"n_range": [mg[0]["n"], mg[-1]["n"]], "beta_18_values": {str(r["n"]): r["beta_18"] for r in mg}, "all_margin_zero": all(r["margin"] == 0 for r in mg)} if mg else None ls = load("local_search_attacks.json") summary["local_search"] = {"seed": ls["seed"], "A_instances": len(ls["attack_A"]), "A_counterexample": ls["attack_A_any_counterexample"], "A_controls_all_found": ls["attack_A_controls_all_found"], "A_max_closure_deficit_min": min(r["N"] - r["best_closure"] for r in ls["attack_A"]), "B_instances": len(ls["attack_B"]), "B_violation": ls["attack_B_any_violation"], "B_best_boundary_min": min(r["best_boundary"] for r in ls["attack_B"]), "B_controls": [(r["n"], r["p"], r["best_boundary"], r["expected_beta_from_table"]) for r in ls["attack_B_controls"]], "B_controls_reached_table_value": ls["attack_B_controls_reached_table_value"], "wall_seconds": ls["wall_seconds_total"]} if ls else None # certificate re-verification lv = json.load(open("results/lower_bound_verification.json")) if os.path.exists("results/lower_bound_verification.json") else None summary["certificate_recheck"] = {"boundary_checked": len(lv["boundary"]), "boundary_ok": sum(1 for r in lv["boundary"] if r["ok"]), "fortcover_checked": len(lv["fortcover"]), "fortcover_ok": sum(1 for r in lv["fortcover"] if r["ok"]), "fortcover_n": sorted({r["n"] for r in lv["fortcover"]}), "all_ok": lv["all_ok"]} if lv else None json.dump(summary, open(os.path.join(R, "summary.json"), "w"), indent=1) m = json.load(open("results/metrics.json")) m["robustness"] = {k: v for k, v in summary.items() if k != "ff_brute"} | {"ff_brute": {k: v for k, v in summary["ff_brute"].items() if k != "rows"}} json.dump(m, open("results/metrics.json", "w"), indent=1) print(json.dumps(m["robustness"], indent=1))