1"""Holdout test (pre-registered H = {32,35,37,41,44,48}; conjectures registered22026-10-30T18:00:31Z in plan/conjectures.jsonl). For each holdout n:3 * attempt to find an 11-vertex zero-forcing set with the fort-cover search4 (time-limited); a witness would refute C1/C2;5 * the lower bound Z >= 12 is supplied by the DRAT-certified boundary6 certificate F(n,18) (run_boundary_window.py) and Lemma 3.1;7 * the upper bound 12 by P7 (replayed by verify_upper_bounds.py).8Appends to results/solver_runs.jsonl and results/holdout_results.jsonl.9"""10import json11import os12import sys1314import common15from graph_constructor import label16from sat_or_ilp_solver import fort_cover1718HOLDOUT = [32, 35, 37, 41, 44, 48]19LIMIT = float(os.environ.get("FORT_LIMIT", "600"))2021if __name__ == "__main__":22 ns = [int(a) for a in sys.argv[1:]] or HOLDOUT23 for n in ns:24 r = fort_cover(n, 5, 11, time_limit=LIMIT)25 rec = {"n": n, "k": 5, "method": "fort_cover", "bound": 11, "sat": r["sat"], "iterations": r["iterations"],26 "forts": len(r["forts"]), "wall_seconds": r["wall_seconds"], "timeout": r["sat"] is None,27 "witness": [label(w, n) for w in r["witness"]] if r["witness"] else None, "utc": common.utcnow(), "holdout": True}28 rec.update(common.versions())29 common.append_jsonl(os.path.join(common.RESULTS, "solver_runs.jsonl"), rec)30 common.append_jsonl(os.path.join(common.RESULTS, "holdout_results.jsonl"), rec)31 print(json.dumps(rec), flush=True)32