"""Merges all evidence into the value tables and metrics: results/exact_values.csv n, Z, upper evidence, lower evidence, status results/known_vs_new.csv literature status per n results/tables/*.csv manuscript tables results/metrics.json headline numbers Evidence sources: results/brute_force_values.json (exhaustive, C oracle), results/upper_bound_witnesses.jsonl, results/lower_bound_certificates.jsonl (fort cover, DRAT checked), results/boundary_certificates.jsonl (DRAT checked; with Lemma 3.1 gives Z >= 12 when n >= ceil((p+11)/2)), results/solver_runs.jsonl, results/upper_bound_verification.json, results/lower_bound_verification.json. Status rule (plan ยง5): fully certified = replayed witness + (exhaustive brute force | externally checked DRAT certificate + proved lemma); solver-supported = two agreeing solver paths without external certificate; candidate = upper only. """ import csv import json import math import os import common R = common.RESULTS HOLDOUT = {32, 35, 37, 41, 44, 48} KNOWN = {11: ("6", "Rashidi et al. 2020 Thm 2.6; Krishnan 2026 exhaustive"), 14: ("8", "P(14,5) ~ P(14,3); Krishnan-Ma-Zhang 2026 Thm 1.1"), 16: ("8", "P(16,5) ~ P(16,3); Krishnan-Ma-Zhang 2026 Thm 1.1"), 19: ("10", "P(19,5) ~ P(19,4); Krishnan-Ma-Zhang 2026 Thm 1.1"), 21: ("10", "P(21,5) ~ P(21,4); Krishnan-Ma-Zhang 2026 Thm 1.1")} RASHIDI_UB = {11: 6, 12: 8, 13: 10, 14: 11, 16: 9} def load_jsonl(name): p = os.path.join(R, name) return [json.loads(l) for l in open(p)] if os.path.exists(p) else [] def main(nmax=48): bf = json.load(open(os.path.join(R, "brute_force_values.json"))) if os.path.exists(os.path.join(R, "brute_force_values.json")) else {} wit = {} for w in load_jsonl("upper_bound_witnesses.jsonl"): if w["n"] not in wit or w["size"] < wit[w["n"]]["size"]: wit[w["n"]] = w ubv = json.load(open(os.path.join(R, "upper_bound_verification.json"))) if os.path.exists(os.path.join(R, "upper_bound_verification.json")) else {"witnesses": [], "P7": []} replay_ok = {(x["n"], x["size"]): x["replay_ok"] for x in ubv["witnesses"]} p7_ok = {x["n"]: x["replay_ok"] for x in ubv["P7"]} lbv = json.load(open(os.path.join(R, "lower_bound_verification.json"))) if os.path.exists(os.path.join(R, "lower_bound_verification.json")) else {"boundary": [], "fortcover": []} bnd_ok = {(x["n"], x["p"]): x["ok"] for x in lbv["boundary"]} fort_ok = {(x["n"], x["bound"]): x["ok"] for x in lbv["fortcover"]} fort_certs = {} for c in load_jsonl("lower_bound_certificates.jsonl"): if c.get("sat") is False: fort_certs[c["n"]] = max(fort_certs.get(c["n"], -1), c["bound"]) bnd_certs = {} for c in load_jsonl("boundary_certificates.jsonl"): if c.get("sat") is False and c["n"] >= math.ceil((c["p"] + 11) / 2): bnd_certs.setdefault(c["n"], []).append(c["p"]) round_unsat = {} for r in load_jsonl("solver_runs.jsonl"): if r.get("method") == "round_sat" and r.get("sat") is False: round_unsat[r["n"]] = max(round_unsat.get(r["n"], -1), r["bound"]) rows = [] for n in range(11, nmax + 1): up = None up_src = [] if n in wit: up = wit[n]["size"] up_src.append("witness(%d)%s" % (up, "" if replay_ok.get((n, up)) else "?")) if n >= 12 and p7_ok.get(n, n == 12 and p7_ok.get(12)): if up is None or 12 < up: up = 12 up_src.append("P7") if str(n) in bf and bf[str(n)]["Z"] is not None: if up is None or bf[str(n)]["Z"] < up: up = bf[str(n)]["Z"] up_src.append("bruteforce-witness") low = 1 low_src = [] if str(n) in bf and bf[str(n)]["Z"] is not None: low = max(low, bf[str(n)]["Z"]) low_src.append("exhaustive(sizes<=%d)" % (bf[str(n)]["Z"] - 1)) if n in bnd_certs: ps = [p for p in bnd_certs[n] if bnd_ok.get((n, p))] if ps: low = max(low, 12) low_src.append("boundary-DRAT(p=%s)+Lemma3.1" % ",".join(str(p) for p in sorted(ps))) if n in fort_certs and fort_ok.get((n, fort_certs[n])): low = max(low, fort_certs[n] + 1) low_src.append("fortcover-DRAT(b=%d)" % fort_certs[n]) if n in round_unsat: low_ss = round_unsat[n] + 1 low_src.append("round-SAT-unsat(s=%d)[solver-supported]" % round_unsat[n]) else: low_ss = 1 if up is not None and low == up and low_src: status = "fully certified" Z = up elif up is not None and max(low, low_ss) == up: status = "solver-supported" Z = up elif up is not None: status = "candidate" Z = "" else: status = "unknown" Z = "" rows.append({"n": n, "Z": Z, "upper": up if up is not None else "", "upper_evidence": ";".join(up_src), "lower": low if low_src else (low_ss if low_ss > 1 else ""), "lower_evidence": ";".join(low_src), "status": status, "holdout": n in HOLDOUT, "gcd_n_5": math.gcd(n, 5), "n_mod_24": n % 24}) with open(os.path.join(R, "exact_values.csv"), "w", newline="") as f: w = csv.DictWriter(f, fieldnames=list(rows[0].keys())) w.writeheader() w.writerows(rows) # known vs new kv = [] for r in rows: n = r["n"] if n in KNOWN: lit, src = KNOWN[n] elif n % 24 == 0: lit, src = "12", "Alameda et al. 2018 as reported by Rashidi et al. 2020 Remark 2.4 (second-hand)" else: lit, src = "", "no published exact value found (to our knowledge)" ub = RASHIDI_UB.get(n, 12) kv.append({"n": n, "published_value": lit, "published_source": src, "published_upper_bound": ub, "this_run_Z": r["Z"], "status": r["status"], "classification": ("known" if lit else ("new" if r["status"] == "fully certified" else ("new (solver-supported)" if r["status"] == "solver-supported" else "unresolved"))), "agrees_with_literature": ("" if not lit or r["Z"] == "" else str(int(lit) == r["Z"]))}) with open(os.path.join(R, "known_vs_new.csv"), "w", newline="") as f: w = csv.DictWriter(f, fieldnames=list(kv[0].keys())) w.writeheader() w.writerows(kv) return rows, kv if __name__ == "__main__": rows, kv = main() for r in rows: print(r["n"], r["Z"], r["status"], r["upper_evidence"], "|", r["lower_evidence"])