1"""Checks a stored fort-cover certificate (CNF + DRAT proof + fort list) with2drat-trim through a plain subprocess and appends the usual record to3results/lower_bound_certificates.jsonl and results/solver_runs.jsonl.45Used for the proofs whose producing process (code/regen_fortcover_proof.py)6ended before drat-trim finished and before the record was appended (n = 237and n = 25, see review/revisions.md, F1). The proof file is read verbatim; its8SHA-256 and the solver that produced it are recorded, but no solve time is9claimed because the producing process did not report one (the DRAT file10modification time is recorded instead).1112usage: python3 code/check_fortcover_proof.py N BOUND [TIMEOUT_SECONDS]13Exit code 0 iff drat-trim printed "s VERIFIED" and exited 0.14"""15import datetime16import json17import os18import subprocess19import sys20import time2122import common2324DRAT_TRIM = os.path.join(common.ROOT, "code", "tools", "drat-trim", "drat-trim")252627def mtime_utc(path):28 return datetime.datetime.fromtimestamp(os.path.getmtime(path), datetime.timezone.utc).isoformat(timespec="seconds")293031def count_lines(path):32 n = 033 with open(path, "rb") as f:34 for chunk in iter(lambda: f.read(1 << 24), b""):35 n += chunk.count(b"\n")36 return n373839def main(n, b, limit):40 cert_dir = os.path.join(common.CERTS, "fortcover")41 cnf_path = os.path.join(cert_dir, "P%d_5_atmost%d.cnf" % (n, b))42 proof_path = os.path.join(cert_dir, "P%d_5_atmost%d.drat" % (n, b))43 forts_path = os.path.join(cert_dir, "P%d_5_atmost%d.forts.json" % (n, b))44 nv = ncl = 045 with open(cnf_path) as f:46 for line in f:47 if line.startswith("p"):48 nv, ncl = int(line.split()[2]), int(line.split()[3])49 break50 forts = json.load(open(forts_path))["forts"]51 out = {"n": n, "k": 5, "bound": b, "method": "fort_cover_static_proof", "sat": False,52 "solver": "cadical195", "solve_seconds": None,53 "proof_origin": "proof-logging re-solve of the stored CNF by code/regen_fortcover_proof.py whose process ended "54 "before drat-trim finished; checked afterwards by code/check_fortcover_proof.py",55 "proof_file_mtime_utc": mtime_utc(proof_path),56 "cnf_path": os.path.relpath(cnf_path, common.ROOT), "cnf_sha256": common.sha256_file(cnf_path),57 "num_vars": nv, "num_clauses": ncl,58 "proof_path": os.path.relpath(proof_path, common.ROOT), "proof_sha256": common.sha256_file(proof_path),59 "proof_lines": count_lines(proof_path), "proof_bytes": os.path.getsize(proof_path),60 "forts_path": os.path.relpath(forts_path, common.ROOT), "forts_sha256": common.sha256_file(forts_path),61 "num_forts": len(forts), "regenerated_from_stored_cnf": True}62 cmd = [DRAT_TRIM, cnf_path, proof_path]63 out["checker_cmd"] = " ".join(os.path.relpath(c, common.ROOT) if c.startswith("/") else c for c in cmd)64 t1 = time.time()65 try:66 r = subprocess.run(cmd, capture_output=True, text=True, timeout=limit)67 out["checker_exit"] = r.returncode68 out["checker_verified"] = ("s VERIFIED" in r.stdout)69 out["checker_stdout_tail"] = r.stdout.strip().splitlines()[-3:]70 out["checker_timeout"] = False71 except subprocess.TimeoutExpired:72 out["checker_exit"] = None73 out["checker_verified"] = False74 out["checker_timeout"] = True75 out["checker_stdout_tail"] = ["timeout after %d s: proof status unknown" % limit]76 out["checker_seconds"] = round(time.time() - t1, 3)77 out["utc"] = common.utcnow()78 out.update(common.versions())79 # CHECK_RECORD_DIR (optional): write the records there instead of results/ (used when the check80 # runs detached and the workspace must not change until the records are merged by hand).81 rec_dir = os.environ.get("CHECK_RECORD_DIR") or common.RESULTS82 common.append_jsonl(os.path.join(rec_dir, "solver_runs.jsonl"), out)83 if out["checker_verified"] and out["checker_exit"] == 0:84 common.append_jsonl(os.path.join(rec_dir, "lower_bound_certificates.jsonl"), out)85 print(json.dumps(out, sort_keys=True))86 sys.exit(0 if (out["checker_verified"] and out["checker_exit"] == 0) else 1)878889if __name__ == "__main__":90 main(int(sys.argv[1]), int(sys.argv[2]), int(sys.argv[3]) if len(sys.argv) > 3 else 6 * 3600)91