1"""Stage 5: collect the robustness artifacts into results/robustness/summary.json2and merge them under the key "robustness" of results/metrics.json (nothing else3in metrics.json is modified). Every number printed in results/robustness.md is4taken from here."""5import json6import os7import re89ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))10os.chdir(ROOT)11R = "results/robustness"121314def load(name):15 p = os.path.join(R, name)16 return json.load(open(p)) if os.path.exists(p) else None171819def parse_ff(path):20 rows = []21 if not os.path.exists(path):22 return rows23 for line in open(path):24 m = re.match(r"n=(\d+) k=5 s=(\d+) TOTAL enumerated=(\d+) forcing=(\d+)", line)25 if m:26 rows.append({"n": int(m.group(1)), "s": int(m.group(2)), "enumerated": int(m.group(3)), "forcing": int(m.group(4))})27 return rows282930def parse_times(path):31 out = []32 if not os.path.exists(path):33 return out34 for line in open(path):35 m = re.search(r"([\d.]+) real\s+([\d.]+) user", line)36 if m:37 out.append((float(m.group(1)), float(m.group(2))))38 return out394041summary = {}42ff = parse_ff(os.path.join(R, "ff_brute_stdout.txt")) + parse_ff(os.path.join(R, "ff_brute_stdout_31_40.txt"))43times = parse_times(os.path.join(R, "ff_brute_time.txt")) + parse_times(os.path.join(R, "ff_brute_time_31_40.txt"))44summary["ff_brute"] = {45 "rows": ff,46 "instances": len(ff),47 "size11_zero_forcing_n": sorted(r["n"] for r in ff if r["s"] == 11 and r["forcing"] == 0 and r["n"] >= 23),48 "largest_n_size11_exhausted": max([r["n"] for r in ff if r["s"] == 11 and r["forcing"] == 0] or [0]),49 "total_sets_tested": sum(r["enumerated"] for r in ff),50 "total_wall_seconds": round(sum(t[0] for t in times), 1),51 "total_cpu_seconds": round(sum(t[1] for t in times), 1),52 "n23_s11_enumerated": next((r["enumerated"] for r in ff if r["n"] == 23 and r["s"] == 11), None),53 "n25_s11_enumerated": next((r["enumerated"] for r in ff if r["n"] == 25 and r["s"] == 11), None),54 "n23_s12_forcing_sets": next((r["forcing"] for r in ff if r["n"] == 23 and r["s"] == 12), None),55}56# agreement with the table for n = 11..2257import csv58Z = {int(r["n"]): int(r["Z"]) for r in csv.DictReader(open("results/exact_values.csv"))}59agree = True60for n in range(11, 23):61 lo = [r for r in ff if r["n"] == n and r["s"] == Z[n] - 1]62 hi = [r for r in ff if r["n"] == n and r["s"] == Z[n]]63 agree &= bool(lo) and lo[0]["forcing"] == 0 and bool(hi) and hi[0]["forcing"] > 064summary["ff_brute"]["table_11_to_22_reproduced"] = agree6566wr = load("witness_replay.json")67summary["witness_replay"] = {"witnesses": wr["num_witnesses"], "all_ok": wr["all_ok"], "P7_range": wr["P7_range"],68 "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 None69cnt = load("enumeration_counts_check.json")70summary["enumeration_counts"] = {"rows": len(cnt["rows"]), "mismatches": cnt["mismatches"], "all_n_consistent": cnt["all_n_consistent"]} if cnt else None71enc = load("boundary_encoding_check.json")72summary["boundary_encoding"] = {"instances": enc["num_instances"], "all_ok": enc["all_ok"], "table_cells_compared": enc["table_cells_compared"],73 "table_cells_consistent": enc["table_cells_consistent"]} if enc else None74dl = load("deletion_lemma.json")75summary["deletion_lemma"] = {"D1_cases": dl["D1"]["cases"], "D1_failures": dl["D1"]["failures"], "D2_cases": dl["D2"]["cases"],76 "D2_f_undefined": dl["D2"]["f_undefined_on_N[X]"], "D2_boundary_size_changed": dl["D2"]["boundary_size_changed"],77 "D3_instances": dl["D3_instances_found"], "D3_ok": dl["D3_ok"],78 "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 None79dc = load("drat_negative_controls.json")80summary["drat_controls"] = {"controls_behave": dc["controls_behave"], "beta_18_26_exact": dc["beta_18_26_exact"],81 "truncated_rejected": not dc["C1_truncated_proof"]["verified"], "weaker_cnf_rejected": not dc["C2_weaker_formula"]["verified"],82 "wrong_cnf_rejected": not dc["C3_proof_against_n27_cnf"]["verified"], "original_verified": dc["C4_positive_original"]["verified"]} if dc else None83mg = load("margin.json")84summary["margin"] = {"n_range": [mg[0]["n"], mg[-1]["n"]], "beta_18_values": {str(r["n"]): r["beta_18"] for r in mg},85 "all_margin_zero": all(r["margin"] == 0 for r in mg)} if mg else None86ls = load("local_search_attacks.json")87summary["local_search"] = {"seed": ls["seed"], "A_instances": len(ls["attack_A"]), "A_counterexample": ls["attack_A_any_counterexample"],88 "A_controls_all_found": ls["attack_A_controls_all_found"],89 "A_max_closure_deficit_min": min(r["N"] - r["best_closure"] for r in ls["attack_A"]),90 "B_instances": len(ls["attack_B"]), "B_violation": ls["attack_B_any_violation"],91 "B_best_boundary_min": min(r["best_boundary"] for r in ls["attack_B"]),92 "B_controls": [(r["n"], r["p"], r["best_boundary"], r["expected_beta_from_table"]) for r in ls["attack_B_controls"]],93 "B_controls_reached_table_value": ls["attack_B_controls_reached_table_value"],94 "wall_seconds": ls["wall_seconds_total"]} if ls else None95# certificate re-verification96lv = json.load(open("results/lower_bound_verification.json")) if os.path.exists("results/lower_bound_verification.json") else None97summary["certificate_recheck"] = {"boundary_checked": len(lv["boundary"]), "boundary_ok": sum(1 for r in lv["boundary"] if r["ok"]),98 "fortcover_checked": len(lv["fortcover"]), "fortcover_ok": sum(1 for r in lv["fortcover"] if r["ok"]),99 "fortcover_n": sorted({r["n"] for r in lv["fortcover"]}), "all_ok": lv["all_ok"]} if lv else None100json.dump(summary, open(os.path.join(R, "summary.json"), "w"), indent=1)101m = json.load(open("results/metrics.json"))102m["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"}}103json.dump(m, open("results/metrics.json", "w"), indent=1)104print(json.dumps(m["robustness"], indent=1))105