"""Holdout test (pre-registered H = {32,35,37,41,44,48}; conjectures registered
2026-10-30T18:00:31Z in plan/conjectures.jsonl). For each holdout n:
  * attempt to find an 11-vertex zero-forcing set with the fort-cover search
    (time-limited); a witness would refute C1/C2;
  * the lower bound Z >= 12 is supplied by the DRAT-certified boundary
    certificate F(n,18) (run_boundary_window.py) and Lemma 3.1;
  * the upper bound 12 by P7 (replayed by verify_upper_bounds.py).
Appends to results/solver_runs.jsonl and results/holdout_results.jsonl.
"""
import json
import os
import sys

import common
from graph_constructor import label
from sat_or_ilp_solver import fort_cover

HOLDOUT = [32, 35, 37, 41, 44, 48]
LIMIT = float(os.environ.get("FORT_LIMIT", "600"))

if __name__ == "__main__":
    ns = [int(a) for a in sys.argv[1:]] or HOLDOUT
    for n in ns:
        r = fort_cover(n, 5, 11, time_limit=LIMIT)
        rec = {"n": n, "k": 5, "method": "fort_cover", "bound": 11, "sat": r["sat"], "iterations": r["iterations"],
               "forts": len(r["forts"]), "wall_seconds": r["wall_seconds"], "timeout": r["sat"] is None,
               "witness": [label(w, n) for w in r["witness"]] if r["witness"] else None, "utc": common.utcnow(), "holdout": True}
        rec.update(common.versions())
        common.append_jsonl(os.path.join(common.RESULTS, "solver_runs.jsonl"), rec)
        common.append_jsonl(os.path.join(common.RESULTS, "holdout_results.jsonl"), rec)
        print(json.dumps(rec), flush=True)