1"""Exact-value driver (T5/T6). For each n:2 * upper bound: smallest b at which the fort-cover search finds a witness3 quickly (descending from min(12, published bound)); the witness is replayed4 by closure_oracle and stored in results/upper_bound_witnesses.jsonl with the5 full chronology;6 * SAT lower bound: fort-cover UNSAT at b = Z_upper - 1 within the time limit7 (static final CNF re-solved with proof logging, DRAT checked by drat-trim);8 and, independently, the round-based encoding (P4) at s = Z_upper - 1 within9 its own time limit;10 * brute-force lower bound is read from results/brute_force_values.json when11 present.12Every run is recorded in results/solver_runs.jsonl.1314usage: python3 code/run_exact.py N [N ...] (env: FORT_LIMIT, ROUND_LIMIT seconds)15"""16import json17import os18import sys19import time2021import common22from closure_oracle import closure, replay23from graph_constructor import adjacency, edge_list_sha256, edges_formula, label24from sat_or_ilp_solver import fort_cover, round_sat, solve_with_proof2526K = 527FORT_LIMIT = float(os.environ.get("FORT_LIMIT", "900"))28ROUND_LIMIT = float(os.environ.get("ROUND_LIMIT", "600"))293031def record(rec):32 rec["utc"] = common.utcnow()33 rec.update(common.versions())34 common.append_jsonl(os.path.join(common.RESULTS, "solver_runs.jsonl"), rec)35 print(json.dumps(rec)[:300], flush=True)363738def upper_bound_search(n, start):39 """Descend b from start while a witness is found within a short limit."""40 adj = adjacency(n, K)41 best = None42 b = start43 while b >= 1:44 r = fort_cover(n, K, b, time_limit=FORT_LIMIT)45 record({"n": n, "k": K, "method": "fort_cover", "bound": b, "sat": r["sat"], "iterations": r["iterations"],46 "forts": len(r["forts"]), "wall_seconds": r["wall_seconds"], "timeout": r["sat"] is None})47 if r["sat"]:48 S = r["witness"]49 final, chron = closure(adj, S)50 assert len(final) == 2 * n51 ok, fin, bad = replay(adj, S, chron)52 assert ok and len(fin) == 2 * n53 best = {"n": n, "k": K, "size": len(S), "S": [label(w, n) for w in S],54 "chronology": [[label(a, n), label(c, n)] for a, c in chron],55 "graph_sha256": edge_list_sha256(edges_formula(n, K)), "source": "fort_cover", "utc": common.utcnow()}56 common.append_jsonl(os.path.join(common.RESULTS, "upper_bound_witnesses.jsonl"), best)57 b = len(S) - 158 continue59 return best, b, r # r is the UNSAT (or timeout) result at b60 return best, b, None616263def lower_bound_certificate(n, b, r):64 """r: fort_cover result with sat False at bound b. Re-solve the static CNF with proof logging."""65 cert_dir = os.path.join(common.CERTS, "fortcover")66 os.makedirs(cert_dir, exist_ok=True)67 clauses = r["base_clauses"] + r["fort_clauses"]68 cnf_path = os.path.join(cert_dir, "P%d_5_atmost%d.cnf" % (n, b))69 proof_path = os.path.join(cert_dir, "P%d_5_atmost%d.drat" % (n, b))70 forts_path = os.path.join(cert_dir, "P%d_5_atmost%d.forts.json" % (n, b))71 with open(forts_path, "w") as f:72 json.dump({"n": n, "k": K, "bound": b, "svar": r["svar"], "normalised": r["normalised"], "symmetric": r["symmetric"],73 "forts": r["forts"], "forts_labels": [[label(w, n) for w in F] for F in r["forts"]]}, f)74 out = solve_with_proof(clauses, r["nv"], "cadical195", cnf_path, proof_path)75 out.update({"n": n, "k": K, "bound": b, "method": "fort_cover_static_proof", "forts_path": os.path.relpath(forts_path, common.ROOT),76 "forts_sha256": common.sha256_file(forts_path), "num_forts": len(r["forts"])})77 record(out)78 common.append_jsonl(os.path.join(common.RESULTS, "lower_bound_certificates.jsonl"), out)79 return out808182if __name__ == "__main__":83 ns = [int(a) for a in sys.argv[1:]]84 published = {11: 6, 12: 8, 13: 10, 14: 11, 16: 9}85 for n in ns:86 start = min(12, published.get(n, 12))87 t0 = time.time()88 best, b, r = upper_bound_search(n, start)89 Zu = best["size"] if best else start90 lower = None91 if r is not None and r["sat"] is False:92 cert = lower_bound_certificate(n, b, r)93 lower = b + 194 # second path: round-based encoding at s = Zu - 195 # SKIP_ROUND=1 (reproduce.sh default mode) omits the round-based path, whose runs at n >= 18 only time out96 rr = round_sat(n, K, Zu - 1, time_limit=ROUND_LIMIT) if (n <= 30 and os.environ.get("SKIP_ROUND") != "1") else None97 if rr is not None:98 record({"n": n, "k": K, "method": "round_sat", "solver": rr["solver"], "bound": Zu - 1, "sat": rr["sat"], "T": rr["T"],99 "num_vars": rr["num_vars"], "num_clauses": rr["num_clauses"], "wall_seconds": rr["solve_seconds"], "timeout": rr["timeout"]})100 print("n=%d: upper=%d (witness size), fort-cover lower=%s, round_sat(%d)=%s, total %.1fs" % (101 n, Zu, lower, Zu - 1, rr["sat"] if rr else None, time.time() - t0), flush=True)102