1"""Uniform solver front-ends: CaDiCaL (pysat Cadical195, in-process), Kissat (subprocess), z3 (bit-vector SMT).23Each runner returns a dict with: status in {sat, unsat, timeout, error}, wall_s, conflicts, decisions, propagations4(when available), solver-reported extras, and `model` = set of true literals (SAT) / dict of word values (z3).5Peak RSS is measured by the caller (one fresh process per cell; see cluster_driver.py).6"""7from __future__ import annotations8import os, re, shutil, subprocess, sys, tempfile, threading, time9from common import S, MASK1011KISSAT_CANDIDATES = [os.environ.get("KISSAT_BIN", ""), os.path.expanduser("~/wp34/bin/kissat"), "/opt/homebrew/bin/kissat"]12CADICAL_CANDIDATES = [os.environ.get("CADICAL_BIN", ""), os.path.expanduser("~/wp34/bin/cadical"), "/opt/homebrew/bin/cadical"]131415def _find(cands, name):16 for c in cands:17 if c and os.path.exists(c):18 return c19 return shutil.which(name)202122def kissat_bin() -> str | None:23 return _find(KISSAT_CANDIDATES, "kissat")242526def cadical_bin() -> str | None:27 return _find(CADICAL_CANDIDATES, "cadical")282930def _write_dimacs(clauses, n_vars):31 with tempfile.NamedTemporaryFile("w", suffix=".cnf", delete=False) as f:32 f.write("p cnf %d %d\n" % (n_vars, len(clauses)))33 for c in clauses:34 f.write(" ".join(map(str, c)) + " 0\n")35 return f.name363738_STAT_RE = re.compile(r"^c (conflicts|decisions|propagations|restarts|maximum-resident-set-size|process-time|maximum resident set size of process|total real time since initialization):\s+([0-9.]+)")39_STAT_KEYS = {"maximum-resident-set-size": "kissat_rss_bytes", "process-time": "solver_process_s",40 "maximum resident set size of process": "cadical_rss_mb", "total real time since initialization": "solver_real_s"}414243def _run_binary(cmd, timeout):44 """Run a DIMACS solver binary; returns (status, model, stats, wall)."""45 t0 = time.time()46 try:47 p = subprocess.run(cmd, capture_output=True, text=True, timeout=timeout + 60)48 txt = p.stdout49 except subprocess.TimeoutExpired as e:50 txt = e.stdout if isinstance(e.stdout, str) else (e.stdout or b"").decode(errors="replace")51 txt += "\ns UNKNOWN\n"52 wall = time.time() - t053 status, model, stats = "timeout", set(), {}54 for line in txt.splitlines():55 if line.startswith("s "):56 status = {"s SATISFIABLE": "sat", "s UNSATISFIABLE": "unsat"}.get(line.strip(), "timeout")57 elif line.startswith("v "):58 model.update(int(x) for x in line[2:].split() if int(x) > 0)59 else:60 m = _STAT_RE.match(line)61 if m:62 key = _STAT_KEYS.get(m.group(1), m.group(1))63 val = float(m.group(2))64 stats[key] = int(val) if val.is_integer() and key not in ("cadical_rss_mb",) else val65 return status, model, stats, wall666768def run_cadical(clauses, timeout: float, n_vars: int | None = None, seed: int = 0) -> dict:69 """CaDiCaL as the standalone binary (`cadical -t <s> --seed=<seed>`): pysat's in-process `interrupt()` does70 not stop CaDiCaL 1.9.5 (tested: a 5 s limit ran for minutes), so wall-clock limits are enforced by the71 binary's real-time limit and a subprocess kill guard."""72 binp = cadical_bin()73 if binp is None:74 return {"status": "error", "error": "cadical binary not found", "wall_s": 0.0}75 if n_vars is None:76 n_vars = max(abs(l) for c in clauses for l in c)77 path = _write_dimacs(clauses, n_vars)78 try:79 status, model, st, wall = _run_binary([binp, "-t", str(int(timeout)), "--seed=%d" % seed, path], timeout)80 finally:81 os.unlink(path)82 # the CaDiCaL binary omits a statistics line when its value is 0 (e.g. an instance solved by propagation)83 dflt = 0 if status in ("sat", "unsat") else None84 out = {"status": status, "wall_s": round(wall, 3), "conflicts": st.get("conflicts", dflt), "decisions": st.get("decisions", dflt),85 "propagations": st.get("propagations", dflt), "restarts": st.get("restarts", dflt), "model": model if status == "sat" else None}86 out.update({k: v for k, v in st.items() if k.startswith("cadical_") or k.startswith("solver_")})87 return out888990def run_cadical_pysat(clauses, timeout: float) -> dict:91 """In-process pysat Cadical195 (used only where the instance is known to be fast; no reliable timeout)."""92 from pysat.solvers import Cadical19593 t0 = time.time()94 with Cadical195(bootstrap_with=clauses) as s:95 timer = threading.Timer(timeout, s.interrupt)96 timer.start()97 try:98 res = s.solve_limited(expect_interrupt=True)99 finally:100 timer.cancel()101 wall = time.time() - t0102 st = s.accum_stats() or {}103 out = {"status": "sat" if res is True else ("unsat" if res is False else "timeout"),104 "wall_s": round(wall, 3), "conflicts": st.get("conflicts"), "decisions": st.get("decisions"),105 "propagations": st.get("propagations"), "restarts": st.get("restarts"), "model": None}106 if res is True:107 out["model"] = {l for l in s.get_model() if l > 0}108 return out109110111def run_kissat(clauses, n_vars: int, timeout: float, seed: int = 0) -> dict:112 binp = kissat_bin()113 if binp is None:114 return {"status": "error", "error": "kissat binary not found", "wall_s": 0.0}115 path = _write_dimacs(clauses, n_vars)116 try:117 status, model, st, wall = _run_binary([binp, "--time=%d" % int(timeout), "--seed=%d" % seed, "-s", path], timeout)118 finally:119 os.unlink(path)120 out = {"status": status, "wall_s": round(wall, 3), "conflicts": st.get("conflicts"), "decisions": st.get("decisions"),121 "propagations": st.get("propagations"), "restarts": st.get("restarts"), "model": model if status == "sat" else None}122 out.update({k: v for k, v in st.items() if k.startswith("kissat_") or k.startswith("solver_")})123 return out124125126# ---------------------------------------------------------------------------------------------------------- z3 ---127def z3_compress(z3, IV, W16, rounds: int, feedforward: bool):128 """Bit-vector model of the reference compression (W16/IV are z3 BitVec(32) or python ints)."""129 def rotr(x, k): return z3.RotateRight(x, k)130 def S0(x): return rotr(x, 2) ^ rotr(x, 13) ^ rotr(x, 22)131 def S1(x): return rotr(x, 6) ^ rotr(x, 11) ^ rotr(x, 25)132 def s0(x): return rotr(x, 7) ^ rotr(x, 18) ^ z3.LShR(x, 3)133 def s1(x): return rotr(x, 17) ^ rotr(x, 19) ^ z3.LShR(x, 10)134 bv = lambda v: z3.BitVecVal(v, 32) if isinstance(v, int) else v135 W = [bv(w) for w in W16]136 for t in range(16, rounds):137 W.append(s1(W[t - 2]) + W[t - 7] + s0(W[t - 15]) + W[t - 16])138 a, b, c, d, e, f, g, h = [bv(x) for x in IV]139 for t in range(rounds):140 T1 = h + S1(e) + ((e & f) ^ (~e & g)) + z3.BitVecVal(S.K[t], 32) + W[t]141 T2 = S0(a) + ((a & b) ^ (a & c) ^ (b & c))142 a, b, c, d, e, f, g, h = T1 + T2, a, b, c, d + T1, e, f, g143 out = [a, b, c, d, e, f, g, h]144 if feedforward:145 out = [x + bv(y) for x, y in zip(out, IV)]146 return out147148149def run_z3(build, timeout: float, seed: int = 0) -> dict:150 """build(z3, solver) -> dict name -> BitVec to read back on SAT."""151 import z3152 z3.set_param("sat.random_seed", seed)153 z3.set_param("smt.random_seed", seed)154 s = z3.Solver()155 s.set("timeout", int(timeout * 1000))156 names = build(z3, s)157 t0 = time.time()158 r = s.check()159 wall = time.time() - t0160 st = {}161 try:162 stats = s.statistics()163 for k in stats.keys():164 try:165 st[k] = stats.get_key_value(k)166 except Exception:167 pass168 except Exception:169 pass170 status = "sat" if r == z3.sat else ("unsat" if r == z3.unsat else "timeout")171 out = {"status": status, "wall_s": round(wall, 3),172 "conflicts": st.get("conflicts", st.get("sat conflicts")), "decisions": st.get("decisions", st.get("sat decisions")),173 "propagations": st.get("propagations", st.get("sat propagations")), "z3_stats": st, "model": None}174 if r == z3.sat:175 m = s.model()176 out["model"] = {k: m.eval(v, model_completion=True).as_long() for k, v in names.items()}177 return out178