"""Builds results/metrics.json, results/tables/*.csv and consolidates results/counterexamples.jsonl from the raw result files. Run after build_tables.py, verify_upper_bounds.py and verify_lower_bounds.py.""" import collections import csv import json import math import os import common from build_tables import HOLDOUT, load_jsonl R = common.RESULTS T = os.path.join(R, "tables") os.makedirs(T, exist_ok=True) def main(): rows = list(csv.DictReader(open(os.path.join(R, "exact_values.csv")))) bf = json.load(open(os.path.join(R, "brute_force_values.json"))) bfr = load_jsonl("brute_force_runs.jsonl") bnd = [r for r in load_jsonl("boundary_certificates.jsonl") if "error" not in r] lbv = json.load(open(os.path.join(R, "lower_bound_verification.json"))) ubv = json.load(open(os.path.join(R, "upper_bound_verification.json"))) btab = [r for r in load_jsonl("boundary_table.jsonl") if "beta" in r] runs = load_jsonl("solver_runs.jsonl") hold = load_jsonl("holdout_results.jsonl") lemma = json.load(open(os.path.join(R, "lemma_checks.json"))) t1 = json.load(open(os.path.join(R, "t1_graph_invariants.json"))) t2 = json.load(open(os.path.join(R, "t2_order_independence.json"))) status_counts = collections.Counter(r["status"] for r in rows) certified = [int(r["n"]) for r in rows if r["status"] == "fully certified"] p18 = sorted({r["n"] for r in bnd if r["p"] == 18 and r["sat"] is False and r.get("checker_verified")}) p18_ok = sorted({x["n"] for x in lbv["boundary"] if x["p"] == 18 and x["ok"]}) window_complete = all(n in p18_ok for n in range(26, 155)) solve = [r["solve_seconds"] for r in bnd if r["p"] == 18 and r["sat"] is False] check = [r["checker_seconds"] for r in bnd if r["p"] == 18 and r["sat"] is False] plines = [r["proof_lines"] for r in bnd if r["p"] == 18 and r["sat"] is False] # window-only statistics (26 <= n <= 154; excludes the n = 24 cross-check certificate) win = [r for r in bnd if r["p"] == 18 and r["sat"] is False and 26 <= r["n"] <= 154] wsolve = [r["solve_seconds"] for r in win] wcheck = [r["checker_seconds"] for r in win] wlines = [r["proof_lines"] for r in win] wbytes = sum(os.path.getsize(os.path.join(common.ROOT, r["proof_path"])) for r in win if os.path.exists(os.path.join(common.ROOT, r["proof_path"]))) fort_ok_n = sorted({x["n"] for x in lbv["fortcover"] if x["ok"]}) bf_total_subsets = sum(r["enumerated_subsets"] for r in bfr) bf_total_wall = sum(r["wall_seconds"] for r in bfr) bf_max_n = max(int(n) for n, v in bf.items() if v["Z"] is not None) values = {int(r["n"]): (int(r["Z"]) if r["Z"] else None) for r in rows} holdout_pred_ok = all(values.get(n) == 12 for n in HOLDOUT) exceptions = {n: values[n] for n in range(11, 23)} metrics = { "utc": common.utcnow(), "k": 5, "n_range_tabulated": [11, 48], "status_counts": dict(status_counts), "fully_certified_n": certified, "largest_fully_certified_n": max(certified) if certified else None, "values_11_to_22": exceptions, "threshold_n0": 23, "value_at_and_above_threshold": 12, "Z_P22_5": values.get(22), "Z_P23_5": values.get(23), "Z_P25_5": values.get(25), "boundary_parameter_p": 18, "boundary_n1": 26, "boundary_c_max": 14, "boundary_N_max": 154, "boundary_window_instances": len(p18_ok), "boundary_window_complete_26_to_154": window_complete, "boundary_window_all_drat_verified": all(x["ok"] for x in lbv["boundary"] if x["p"] == 18), "boundary_p18_solve_seconds": {"min": min(solve), "max": max(solve), "median": sorted(solve)[len(solve) // 2], "total": round(sum(solve), 1)} if solve else None, "boundary_p18_check_seconds": {"min": min(check), "max": max(check), "median": sorted(check)[len(check) // 2], "total": round(sum(check), 1)} if check else None, "boundary_p18_proof_lines": {"min": min(plines), "max": max(plines), "total": sum(plines)} if plines else None, "boundary_window_solve_seconds": {"min": min(wsolve), "max": max(wsolve), "mean": round(sum(wsolve) / len(wsolve), 1), "total": round(sum(wsolve), 1)} if wsolve else None, "boundary_window_check_seconds": {"min": min(wcheck), "max": max(wcheck), "mean": round(sum(wcheck) / len(wcheck), 1), "total": round(sum(wcheck), 1)} if wcheck else None, "boundary_window_proof_lines": {"min": min(wlines), "max": max(wlines), "total": sum(wlines)} if wlines else None, "boundary_window_proof_bytes": wbytes, "boundary_window_proof_gigabytes": round(wbytes / 1e9, 1), "fortcover_certified_n": fort_ok_n, "fortcover_largest_n": max(fort_ok_n) if fort_ok_n else None, "boundary_p18_cnf_vars_at_154": next((r["num_vars"] for r in bnd if r["p"] == 18 and r["n"] == 154), None), "boundary_p18_cnf_clauses_at_154": next((r["num_clauses"] for r in bnd if r["p"] == 18 and r["n"] == 154), None), "boundary_obstruction_n25_p18_beta": next((r["beta"] for r in btab if r["n"] == 25 and r["p"] == 18), None), "boundary_table_cells": len(btab), "boundary_table_p_range": [min(r["p"] for r in btab), max(r["p"] for r in btab)], "boundary_table_n_range": [min(r["n"] for r in btab), max(r["n"] for r in btab)], "boundary_fails_at_25_for_all_p_tested": all(any(r["n"] == 25 and r["p"] == p and r["beta"] <= 11 for r in btab) for p in range(12, 25)), "brute_force_max_n": bf_max_n, "brute_force_total_subsets_enumerated": bf_total_subsets, "brute_force_total_wall_seconds": round(bf_total_wall, 1), "brute_force_n23_subsets_size11": next((r["enumerated_subsets"] for r in bfr if r["n"] == 23 and r["s"] == 11), None), "brute_force_n25_subsets_size11": next((r["enumerated_subsets"] for r in bfr if r["n"] == 25 and r["s"] == 11), None), "fortcover_certificates_verified": sum(1 for x in lbv["fortcover"] if x["ok"]), "fortcover_certificates_total": len(lbv["fortcover"]), "upper_witness_replays_ok": sum(1 for x in ubv["witnesses"] if x["replay_ok"]), "upper_witness_replays_total": len(ubv["witnesses"]), "P7_replays_ok_12_to_60": all(x["replay_ok"] for x in ubv["P7"]), "T1_all_ok": all(r["all_ok"] for r in t1), "T1_n_count": len(t1), "T2_passed": sum(r["passed"] for r in t2), "T2_total": sum(r["total"] for r in t2), "CS6_mismatches": lemma["CS6_boundary_identity"]["mismatches"], "CS6_total": lemma["CS6_boundary_identity"]["total"], "T8_mismatches": lemma["T8_deletion_map"]["mismatches"], "T8_total": lemma["T8_deletion_map"]["total"], "holdout": sorted(HOLDOUT), "holdout_values": {str(n): values.get(n) for n in sorted(HOLDOUT)}, "holdout_prediction_12_all_correct": holdout_pred_ok, "holdout_fortcover_search_timeouts": sum(1 for h in hold if h["sat"] is None), "holdout_fortcover_search_witness_found": sum(1 for h in hold if h["sat"]), "round_sat_unsat_agreements": sorted({r["n"] for r in runs if r.get("method") == "round_sat" and r.get("sat") is False}), "round_sat_timeouts": sorted({r["n"] for r in runs if r.get("method") == "round_sat" and r.get("sat") is None}), "versions": common.versions(), "drat_trim_source_sha256": lbv.get("drat_trim_sha256"), "worker": "M4M64c (16 cores, Apple Silicon, macOS 26.4)", } # flat copy of the scalar headline metrics under "metrics" (the platform's # metrics comparison expects a record at this key; reportedValues may point # to these keys through metricKey) metrics["metrics"] = {k: v for k, v in metrics.items() if isinstance(v, (int, float, str, bool))} # keep the platform-written registry of reported values, if present mpath = os.path.join(R, "metrics.json") if os.path.exists(mpath): try: old = json.load(open(mpath)) if "reportedValues" in old: metrics["reportedValues"] = old["reportedValues"] except Exception: pass with open(mpath, "w") as f: json.dump(metrics, f, indent=1) # tables with open(os.path.join(T, "exact_values.csv"), "w", newline="") as f: w = csv.writer(f) w.writerow(["n", "Z", "status", "lower_evidence", "upper_evidence", "known"]) for r in rows: w.writerow([r["n"], r["Z"], r["status"], r["lower_evidence"], r["upper_evidence"], ""]) with open(os.path.join(T, "boundary_table.csv"), "w", newline="") as f: w = csv.writer(f) ns = sorted({r["n"] for r in btab}) w.writerow(["p"] + ns) for p in sorted({r["p"] for r in btab}): d = {r["n"]: r["beta"] for r in btab if r["p"] == p} w.writerow([p] + [(d[n] if d.get(n, 99) <= 11 else ">=12") for n in ns]) with open(os.path.join(T, "boundary_window_p18.csv"), "w", newline="") as f: w = csv.writer(f) w.writerow(["n", "num_vars", "num_clauses", "solve_seconds", "proof_lines", "check_seconds", "verified", "cnf_sha256", "proof_sha256"]) for r in sorted((r for r in bnd if r["p"] == 18 and r["sat"] is False), key=lambda r: r["n"]): w.writerow([r["n"], r["num_vars"], r["num_clauses"], r["solve_seconds"], r["proof_lines"], r["checker_seconds"], r["checker_verified"], r["cnf_sha256"][:16], r["proof_sha256"][:16]]) with open(os.path.join(T, "brute_force.csv"), "w", newline="") as f: w = csv.writer(f) w.writerow(["n", "s", "subsets", "orbit_representatives", "forcing_representatives", "wall_seconds"]) for r in sorted(bfr, key=lambda r: (r["n"], r["s"])): if r["enumerated_subsets"]: w.writerow([r["n"], r["s"], r["enumerated_subsets"], r["orbit_representatives_tested"], r["forcing_representatives"], r["wall_seconds"]]) print(json.dumps({k: v for k, v in metrics.items() if k not in ("versions",)}, indent=1)) if __name__ == "__main__": main()