1"""Regenerates the DRAT certificate for a stored fort-cover CNF whose proof-logging2re-solve did not complete (used for n = 22: the lazy loop proved UNSAT at bound 103and stored the CNF and the fort list, but the process ended before the DRAT file4was written). Reads the stored DIMACS file verbatim (so its SHA-256 is unchanged),5re-solves it with CaDiCaL under proof logging, writes the DRAT proof, runs6drat-trim and appends the usual record to results/lower_bound_certificates.jsonl7and results/solver_runs.jsonl.89usage: python3 code/regen_fortcover_proof.py N BOUND10"""11import json12import os13import subprocess14import sys15import time1617import common18from pysat.formula import CNF19from pysat.solvers import Solver2021DRAT_TRIM = os.path.join(common.ROOT, "code", "tools", "drat-trim", "drat-trim")222324def main(n, b):25 cert_dir = os.path.join(common.CERTS, "fortcover")26 cnf_path = os.path.join(cert_dir, "P%d_5_atmost%d.cnf" % (n, b))27 proof_path = os.path.join(cert_dir, "P%d_5_atmost%d.drat" % (n, b))28 forts_path = os.path.join(cert_dir, "P%d_5_atmost%d.forts.json" % (n, b))29 cnf = CNF(from_file=cnf_path)30 forts = json.load(open(forts_path))["forts"]31 t0 = time.time()32 with Solver(name="cadical195", bootstrap_with=cnf.clauses, with_proof=True) as s:33 sat = s.solve()34 proof = None if sat else s.get_proof()35 t_solve = time.time() - t036 out = {"sat": sat, "solver": "cadical195", "solve_seconds": round(t_solve, 3),37 "cnf_path": os.path.relpath(cnf_path, common.ROOT), "cnf_sha256": common.sha256_file(cnf_path),38 "num_vars": cnf.nv, "num_clauses": len(cnf.clauses)}39 if sat:40 out["note"] = "stored CNF is satisfiable: no certificate"41 else:42 with open(proof_path, "w") as f:43 f.write("\n".join(proof) + "\n")44 out["proof_path"] = os.path.relpath(proof_path, common.ROOT)45 out["proof_sha256"] = common.sha256_file(proof_path)46 out["proof_lines"] = len(proof)47 t1 = time.time()48 cmd = [DRAT_TRIM, cnf_path, proof_path]49 r = subprocess.run(cmd, capture_output=True, text=True)50 out["checker_cmd"] = " ".join(os.path.relpath(c, common.ROOT) if c.startswith("/") else c for c in cmd)51 out["checker_exit"] = r.returncode52 out["checker_verified"] = ("s VERIFIED" in r.stdout)53 out["checker_seconds"] = round(time.time() - t1, 3)54 out["checker_stdout_tail"] = r.stdout.strip().splitlines()[-3:]55 out.update({"n": n, "k": 5, "bound": b, "method": "fort_cover_static_proof", "regenerated_from_stored_cnf": True,56 "forts_path": os.path.relpath(forts_path, common.ROOT), "forts_sha256": common.sha256_file(forts_path),57 "num_forts": len(forts), "utc": common.utcnow()})58 out.update(common.versions())59 common.append_jsonl(os.path.join(common.RESULTS, "solver_runs.jsonl"), out)60 if not sat:61 common.append_jsonl(os.path.join(common.RESULTS, "lower_bound_certificates.jsonl"), out)62 print(json.dumps(out))636465if __name__ == "__main__":66 main(int(sys.argv[1]), int(sys.argv[2]))67