1"""Stage 5: negative controls for the trusted checker (drat-trim).23The proof of Theorem 5.1 trusts drat-trim's 's VERIFIED' on 129 boundary4certificates. A checker that accepted anything would be useless, so:5 C1 the proof for P(26,5), p = 18, b = 11 truncated to its first half must6 be rejected;7 C2 the same proof run against the WEAKER formula F(26,18,b') for the8 smallest b' >= 12 that is satisfiable must be rejected (a satisfiable9 formula has no refutation); as a by-product this determines the exact10 beta_18(26) (searched upward from 12, capped at 20);11 C3 the proof for n = 26 run against the CNF for n = 27 must be rejected;12 C4 (positive) the original pair must still verify.13All drat-trim exit codes and output tails are recorded.14Output: results/robustness/drat_negative_controls.json15"""16import json17import os18import subprocess19import sys20import time2122ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))23os.chdir(ROOT)24sys.path.insert(0, os.path.join(ROOT, ".pydeps"))25sys.path.insert(0, os.path.join(ROOT, "code"))26from pysat.formula import CNF # noqa: E40227from pysat.solvers import Solver # noqa: E40228from sat_or_ilp_solver import boundary_clauses # noqa: E4022930DRAT = "code/tools/drat-trim/drat-trim"31CERT = "code/proofs/certificates/boundary"32TMP = os.path.join(os.environ.get("TMPDIR", "/tmp"), "drat_controls")33os.makedirs(TMP, exist_ok=True)343536def run_drat(cnf, proof):37 t0 = time.time()38 r = subprocess.run([DRAT, cnf, proof], capture_output=True, text=True, timeout=3600)39 tail = [l for l in r.stdout.strip().splitlines()[-4:]]40 return {"cmd": " ".join([DRAT, cnf, proof]), "exit": r.returncode, "verified": "s VERIFIED" in r.stdout,41 "stdout_tail": tail, "seconds": round(time.time() - t0, 1)}424344def main():45 out = {}46 cnf26 = f"{CERT}/P26_5_p18_b11.cnf"47 drat26 = f"{CERT}/P26_5_p18_b11.drat"48 cnf27 = f"{CERT}/P27_5_p18_b11.cnf"49 # C4 positive50 out["C4_positive_original"] = run_drat(cnf26, drat26)51 # C1 truncated proof52 lines = open(drat26).read().splitlines()53 half = os.path.join(TMP, "P26_half.drat")54 with open(half, "w") as f:55 f.write("\n".join(lines[: len(lines) // 2]) + "\n")56 out["C1_truncated_proof"] = run_drat(cnf26, half)57 out["C1_truncated_proof"]["lines_total"] = len(lines)58 out["C1_truncated_proof"]["lines_kept"] = len(lines) // 259 # C3 wrong CNF60 out["C3_proof_against_n27_cnf"] = run_drat(cnf27, drat26)61 # C2 weaker formula62 beta = None63 for b in range(12, 21):64 cl, x, z, nv = boundary_clauses(26, 5, 18, b)65 with Solver(name="cadical195", bootstrap_with=cl) as sv:66 sat = sv.solve()67 model = sv.get_model() if sat else None68 if sat:69 beta = b70 X = [w for w in range(52) if model[x[w] - 1] > 0]71 path = os.path.join(TMP, f"P26_5_p18_b{b}.cnf")72 CNF(from_clauses=cl).to_file(path)73 out["C2_weaker_formula"] = {"b_prime": b, "exact_beta_18_26": b, "model_X": X}74 out["C2_weaker_formula"].update(run_drat(path, drat26))75 break76 out.setdefault("C2_unsat_bounds", []).append(b)77 out["beta_18_26_exact"] = beta78 out["controls_behave"] = (out["C4_positive_original"]["verified"] and not out["C1_truncated_proof"]["verified"]79 and not out["C3_proof_against_n27_cnf"]["verified"]80 and (beta is None or not out["C2_weaker_formula"]["verified"]))81 json.dump(out, open("results/robustness/drat_negative_controls.json", "w"), indent=1)82 print(json.dumps(out, indent=1))838485if __name__ == "__main__":86 main()87